Fadi A. Aloul, Ph.D.

Agere/SRC Research Fellow,
Electrical Engineering & Computer Science
University of Michigan – Ann Arbor

Email: faloul ‘at’ umich.edu

Resume, Professional Activities, Publications, Patents, Technical Reports, Invited Talks, Tools, Benchmarks , Links


Curriculum Vitae

[HTML]  [PDF]

Professional Activities

 

 


Publications
  Journals:

  1. MINCE: A Static Global Variable-Ordering Heuristic for SAT Search and BDD Manipulation
    F. Aloul, I. Markov, K. Sakallah
    to appear in Journal of Universal Computer Science (JUCS), 2005.
  2. A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints
    G. Nam, F. Aloul, K. Sakallah, and R. Rutenbar
    IEEE Transactions on Computers, 53(6), pp. 688-696, June 2004.
  3. Solving Difficult Instances of Boolean Satisfiability in the Presence of Symmetry
    F. Aloul, A. Ramani, I. Markov, and K. Sakallah
    IEEE Transactions on Computer Aided Design, 22(9), pp. 1117-1137, Sept. 2003.
  4. Satometer: How Much Have We Searched?
    F. Aloul, B. Sierawski, and K. Sakallah
    IEEE Transactions on Computer Aided Design, 22(8), pp. 995-1004, Aug. 2003.

Conferences and Workshops:

1.      Dynamic Symmetry-Breaking for Improved Boolean Optimization
F. Aloul, A. Ramani, I. Markov, and K. Sakallah
Asia South Pacific Design Automation Conference (ASPDAC), Shanghai, China, pp. 445-450, 2005.

2.      On Solving Optimization Problems Using Boolean Satisfiability
F. Aloul
International Conference on Modeling, Simulation, and Applied Optimization, (ICMSAO), Sharjah, UAE, 2005.

3.      Breaking Instance-Independent Symmetries in Exact Graph Coloring
A. Ramani, F. Aloul, I. Markov, and K. Sakallah
Design, Automation and Test in Europe Conference (DATE), Paris, France, pp. 324-329, 2004.

4.      ShatterPB: Symmetry-Breaking for Pseudo-Boolean Formulas
F. Aloul, A. Ramani, I. Markov, and K. Sakallah
Asia South Pacific Design Automation Conference (ASPDAC), Yokohama, Japan, pp. 884-887, 2004.

5.      Efficient Symmetry-Breaking for Boolean Satisfiability
F. Aloul, I. Markov, and K. Sakallah
International Joint Conference on Artificial Intelligence (IJCAI), Acapulco, Mexico, pp. 271-282, 2003.

6.      Shatter: Efficient Symmetry-Breaking for Boolean Satisfiability
F. Aloul, I. Markov, and K. Sakallah
Design Automation Conference (DAC), Anaheim, California, pp. 836-839, 2003.

7.      FORCE: A Fast and Easy-To-Implement Variable-Ordering Heuristic
F. Aloul, I. Markov, and K. Sakallah
Great Lakes Symposium on VLSI (GLSVLSI), Washington D.C., pp. 116-119, 2003.

8.      Symmetry-Breaking for Pseudo-Boolean Formulas
F. Aloul, A. Ramani, I. Markov, and K. Sakallah
International Workshop on Symmetry on Constraint Satisfaction Problems (SymCon), County Cork, Ireland, pp. 1-12, 2003.

9.      Generic ILP versus Specialized 0-1 ILP: an Update
F. Aloul, A. Ramani, I. Markov, and K. Sakallah
International Conference on Computer Aided Design (ICCAD), San Jose, California, pp. 450-457, 2002.

10.  Improving the Efficiency of Circuit-to-BDD Conversion by Gate and Input Ordering
F. Aloul, I. Markov, and K. Sakallah
International Conference on Computer Design (ICCD), Freiburg, Germany, pp. 64-69, 2002.

11.  Robust SAT-Based Search Algorithm for Leakage Power Reduction
F. Aloul, S. Hassoun, K. Sakallah, and D. Blaauw
International Workshop on Power and Timing Modeling, Optimization and Simulation (PATMOS), Sevilla, Spain, pp. 167-177, 2002.

12.  Satometer: How Much Have We Searched?
F. Aloul, B. Sierawski, and K. Sakallah
Design Automation Conference (DAC), New Orleans, Louisiana, pp. 737-742, 2002.

13.  Solving Difficult SAT Instances in the Presence of Symmetry
F. Aloul, A. Ramani, I. Markov, and K. Sakallah
Design Automation Conference (DAC), New Orleans, Louisiana, pp. 731-736, 2002.

14.  Search-Based SAT Using Zero-Suppressed BDDs
F. Aloul, M. Mneimneh, and K. Sakallah
Design, Automation, and Test in Europe Conference (DATE), Paris, France, pp. 1082, 2002.

15.  Symmetry-Breaking for Boolean Satisfiability: The Mysteries of Logic Minimization
F. Aloul, I. Markov, and K. Sakallah
International Workshop on Symmetry on Constraint Satisfaction Problems (SymCon), Ithaca, New York, pp. 37-46, 2002.

16.  ZBDD-Based Backtrack Search SAT Solver
F. Aloul, M. Mneimneh, and K. Sakallah
International Workshop on Logic Synthesis (IWLS), New Orleans, Louisiana, pp. 131-136, 2002.

17.  Efficient Gate and Input Ordering for Circuit-to-BDD Conversion
F. Aloul, I. Markov, and K. Sakallah
International Workshop on Logic Synthesis (IWLS), New Orleans, Louisiana, pp. 137-142, 2002.

18.  PBS: A Backtrack Search Pseudo-Boolean Solver
F. Aloul, A. Ramani, I. Markov, and K. Sakallah
Symposium on the Theory and Applications of Satisfiability Testing (SAT), Cincinnati, Ohio, pp. 346-353, 2002. [Slides]

19.  A Tool for Measuring Progress of Backtrack Search Solvers
F. Aloul, B. Sierawski, and K. Sakallah
Symposium on the Theory and Applications of Satisfiability Testing (SAT), Cincinnati, Ohio, pp. 98-105, 2002.

20.  Solving Difficult SAT Instances in the Presence of Symmetry
F. Aloul, A. Ramani, I. Markov, and K. Sakallah
Symposium on the Theory and Applications of Satisfiability Testing (SAT), Cincinnati, Ohio, pp. 338-345, 2002. [Slides]

21.  Faster SAT and Smaller BDDs via Common Function Structure
F. Aloul, I. Markov, and K. Sakallah
International Conference on Computer Aided Design (ICCAD), San Jose, California, pp. 443-448, 2001.

22.  Scalable Hybrid Verification of Complex Microprocessors
M. Mneimneh, F. Aloul, C. Weaver, S. Chatterjee, K. Sakallah, and T. Austin
Design Automation Conference (DAC), Las Vegas, Nevada, pp. 41-46, 2001.

23.  A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints
G. Nam, F. Aloul, K. Sakallah, and R. Rutenbar
International Symposium on Physical Design (ISPD), Sonoma Wine County, California, pp. 222-227, 2001.

24.  Backtrack Search Using ZBDDs
F. Aloul, M. Mneimneh, and K. Sakallah
International Workshop on Logic Synthesis (IWLS), Lake Tahoe, California, pp. 293-297, 2001.

25.  MINCE: A Static Global Variable-Ordering for SAT and BDD
F. Aloul, I. Markov, and K. Sakallah
International Workshop on Logic Synthesis (IWLS), Lake Tahoe, California, pp. 281-286, 2001. [Slides]

26.  An Experimental Study of Satisfiability Search Heuristics
F. Aloul, J. Silva, and K. Sakallah
Design, Automation, and Test in Europe Conference (DATE), Paris, France, pp. 745, 2000.

27.  An Experimental Evaluation of Conflict Diagnosis and Recursive Learning in Boolean Satisfiability
F. Aloul and K. Sakallah
International Workshop on Logic Synthesis (IWLS), Dana Point, California, pp. 117-122, 2000.

28.  Efficient Verification of the PCI Local Bus Using Boolean Satisfiability
F. Aloul and K. Sakallah
International Workshop on Logic Synthesis (IWLS), Dana Point, California, pp. 131-136, 2000.

Patents

  1. Methods and Apparatus for Generating Functional Test Programs by Traversing a Finite State Model of an Instruction Set Architecture
    F. Aloul and R. Raimi
    filed for US patent, Billions of Operations Per Second Inc. (BOPS), Mountain View, California.

Technical Reports

  1. Solving Difficult Instances of Boolean Satisfiability in the Presence of Symmetry
    F. Aloul, A. Ramani, I. Markov, and K. Sakallah
    Technical Report CSE-TR-463-02, University of Michigan, September 2002.

  2. Generic ILP versus Specialized 0-1 ILP: An Update
    F. Aloul, I Markov, and K. Sakallah
    Technical Report CSE-TR-461-02, University of Michigan, August 2002.
  3. Satometer: How Much Have We Searched?
    F. Aloul, B. Sierawski, and K. Sakallah
    Technical Report CSE-TR-457-02, University of Michigan, June 2002.
  4. Faster SAT and Smaller BDDs via Common Function Structure
    F. Aloul, I. Markov, and K. Sakallah
    Technical Report CSE-TR-445-01, University of Michigan, 2001.

Invited Talks / Demos

  1. Symmetry-Detection and Breaking for Boolean Satisfiability
    F. Aloul
    Tufts University, 2005.

  2. Scalable Algorithms for Boolean Satisfiability Enabled by Problem Structure
    F. Aloul
    Microsoft Research Lab, 2003.

  3. PBS: A Backtrack-Search Pseudo-Boolean Solver and Optimizer
    F. Aloul, M. Mneimneh, and K. Sakallah
    University Booth, Design Automation Conference (DAC), 2003.

  4. Generic ILP vs. Specialized 0-1 ILP: An Update
    F. Aloul
    IPoCSE Symposium, University of Michigan, 2002.

  5. Faster SAT and Smaller BDDs Through Efficient Problem Partitioning
    F. Aloul
    GFP Annual Conference, Semiconductor Research Corporation (SRC), 2002.

  6. Search-Based SAT Using Zero-Suppressed BDDs
    F. Aloul, M. Mneimneh, and K. Sakallah
    University Booth, Design Automation Conference (DAC), 2002.
  7. SATIRE – An Incremental SAT Solver
    F. Aloul, M. Mneimneh, and K. Sakallah
    University Booth, Design Automation Conference (DAC), 2001.
  8. An Experimental Exploration of SAT Problem Hardness
    F. Aloul
    IPoCSE Symposium, University of Michigan, 2000.
  9. GRASP – SAT Solver
    F. Aloul, V. Kravets, and K. Sakallah
    University Booth, Design Automation Conference (DAC), 2000.
  10. An Experimental Study of Satisfiability Search Heuristics
    F. Aloul
    IPoCSE Symposium, University of Michigan, 1999.

Tools

  1. FORCE
    Static global variable ordering for SAT & BDDs (preprocessing tool).
    Much faster than MINCE.
    Doesn’t use external tools and consists of less than 500 lines of C code.
  2. PBS
    Incremental pseudo-Boolean backtrack search SAT solver and optimizer (handles CNF and 0/1 inequality forms)
  3. SHATTER
    Identifies symmetry-breaking clauses in CNF instances (preprocessing tool)
  4. SATOMETER
    Measures progress of backtrack-search SAT solvers
  5. ZBDDLIB
    New ZBDD operations added to the CUDD package

  6. GRASP
    Backtrack-search SAT solver

  7. MINCE
    Static global variable ordering for SAT & BDDs (preprocessing tool)

  8. SATIRE
    Incremental SAT solver

Benchmarks

Links

Last Updated: January 20, 2005.
By Fadi A. Aloul