Fadi A. Aloul, Ph.D.

Assistant Professor of Computer Engineering
American University of Sharjah, UAE
Agere/SRC Research Fellow
IEEE UAE GOLD Chair

Email: faloul ‘at’ aus.edu


I completed my Ph.D. in Computer Science and Engineering in 2003 from the University of Michigan – Ann Arbor under the supervision of Prof. Karem Sakallah. My research interests include Design Automation, Optimization, and IT & Network Security. I am also currently interested in studying the general IT security awareness in UAE (see the IEEE GCC'07 paper below).

Resume, Professional Activities, Awards, Teaching, Education, Publications, Tutorials, Patents, Invited Talks, Tools, Benchmarks, News, Links


Curriculum Vitae

[HTML]  [PDF]

Professional Activities

 

  • Invited Speaker at the Hacker Halted Conference (H@cker|Halted’08), Dubai, UAE, October 2008.
  • Invited Speaker at the 4th ICT Security Forum (ICT’08), Damascus, Syria, July 2008.
  • Invited Speaker at the E-Commerce Middle East Summit (E-Commerce’08), Dubai, UAE, May 2008.
  • Invited Speaker at the Middle East IT Security Conference (MEITSEC’07), Sharjah, UAE, November 2007.
  • Invited Speaker at the Pakistan’s Cyber Security Conference (PAKCON’07), Karachi, Pakistan, July 2007.
  • Invited Speaker at Drexel University, Philadelphia, PA, January 2007.
  • Invited Speaker at Intel Corporation, Portland, Oregon, July 2005.
  • Invited Speaker at Tufts University, Boston, Massachusetts, April 2005.
  • Invited Speaker at Microsoft Research, Redmond, Washington, December 2003.
  • Invited Speaker at Microsoft Research, Redmond, Washington, May 2003.
  • Invited Tutorialist at the IEEE International Symmetry Conference (ISC’07), Edinburgh, Scotland, 2007.
  • Invited Tutorialist at the IEEE Innovations in Information Technology (IIT’06), Dubai, UAE, 2006.
  • Invited Tutorialist at the International Conference on Modeling, Simulation, and Applied Optimization (ICMSAO’05), Sharjah, UAE, 2005.
  • Track Chair (Computer Engineering) at the IEEE 3rd International Conference on Modeling, Simulation, and Applied Optimization, (ICMSAO’09), Sharjah, UAE, 2009.
  • Co-Chair of the 8th International Workshop on Symmetry and Constraint Satisfaction Problems, (SymCon'08), Sydney, Australia, 2008.
  • Local Organizer at the 7th International Conference on New Software Methodologies, Tools, and Techniques, (SoMeT’08), Sharjah, UAE, 2008.
  • Local Organizer and Session Chair of the IEEE International Conference on Computer Systems and Applications, (AICCSA’06), Sharjah, UAE, 2006.
  • Technical Program Committee (TPC) member of the 11th ACM/SIGDA PhD Forum at the Design Automation Conference (DAC’08), Anaheim, CA, 2008.
  • TPC member of the IEEE Innovations in Information Technology, (IIT’07), Al-Ain, UAE, 2008.
  • TPC member of the 10th ACM/SIGDA PhD Forum at the Design Automation Conference (DAC’07), San Diego, CA, 2007.
  • TPC member of the IEEE International Design and Test Workshop (IDT’07), Cairo, Egypt, 2007.
  • TPC member of the 7th International Workshop on Symmetry and Constraint Satisfaction Problems (SymCon’07), Providence, RI, 2007.
  • TPC member of the IEEE Innovations in Information Technology, (IIT’07), Dubai, UAE, 2007.
  • TPC member of the IEEE Innovations in Information Technology, (IIT’06), Dubai, UAE, 2006.
  • TPC member of the 9th ACM/SIGDA PhD Forum at the Design Automation Conference (DAC’06), San Francisco, CA, 2006.
  • TPC member of the ACM/IEEE International Workshop on Logic and Synthesis (IWLS’06), Vail, Colorado, 2006.
  • TPC member of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT’05), St. Andrews, Scotland, 2005.
  • TPC member of the 8th ACM/SIGDA PhD Forum at the Design Automation Conference (DAC’05), Anaheim, CA, 2005.
  • TPC member of the International Symposium on Wireless Systems and Networks (ISWSN’05), Bahrain, 2005.
  • TPC member of the ACM/IEEE International Workshop on Logic and Synthesis (IWLS’05), Lake Arrowhead, CA, 2005.
  • TPC member of the 7th ACM/SIGDA PhD Forum at the Design Automation Conference (DAC’04), San Diego, CA, 2004.
  • TPC member of the ACM/IEEE International Workshop on Logic and Synthesis (IWLS’04), San Diego, CA, 2004.
  • TPC member of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT’03), Portofino, Italy, 2003.
  • TPC member of the 5th International Workshop on Soft Constraints (CP03-SOFT), County Cork, Ireland, 2003.
  • TPC member and A/V Chair of the ACM/IEEE International Workshop on Logic and Synthesis (IWLS’03), Anaheim, CA, 2003.

 

Awards

Supervised Student Awards

 

Awards

  • Agere/SRC (Semiconductor Research Corporation) Research Fellowship, 2001-2003
  • GANN Fellowship, 2000
  • Graduate Student Research Assistantship, 1999-2001
  • University of Michigan EECS Summer Fellowship, 1998
  • Graduate Student Teaching Assistantship, 1997-1998
  • Ranked 1st among 930 graduating students at Lawrence Technological University (LTU), 1997
  • Lawrence Technological University (LTU) Engineering Excellence Award, 1997
  • Lawrence Technological University (LTU) Presidential Scholarship, 1995-1997
  • Ranked 1st in graduation from highschool, 1993


Teaching

Courses taught at the American University of Sharjah (AUS):

  • NGN110 - Introduction to Engineering & Computing (~700 students/year - Course Coordinator).
  • COE210 - Programming I (C++).
  • COE221 - Digital Systems.
  • COE381 - Operating Systems.
  • COE444 - Computer Security.


Education

  • Post-Doc 2003 - Computer Science & Engineering - University of Michigan, Ann Arbor
  • Ph.D. 2003 - Computer Science & Engineering - University of Michigan, Ann Arbor
  • M.S. 1999 - Computer Science & Engineering - University of Michigan, Ann Arbor (GPA 3.82/4.0)
  • B.S. 1997 - Electrical Engineering - Lawrence Technological University, Southfield (GPA 4.0/4.0 - Summa Cum Laude)


Publications - gs                dblp             cite
Journals:

  1. Solution and Optimization of Systems of Pseudo-Boolean Constraints
    F. Aloul, A. Ramani, I. Markov, and K. Sakallah
    IEEE Transactions on Computers (TC), 56(10), 1415-1424, October 2007.
  2. Symmetry-Breaking for Pseudo-Boolean Formulas
    F. Aloul, A. Ramani, I. Markov, and K. Sakallah
    ACM Journal of Experimental Algorithmics (JEA), vol. 12, article 1.3, 2007.
  3. Using SAT-Based Techniques in Power Estimation
    A. Sagahyroon and F. Aloul
    Elsevier Microelectronics Journal (MEJ), vol. 38, issues 6-7, 706-715, June-July 2007.
  4. Routing in Optical and Non-Optical Networks using Boolean Satisfiability
    F. Aloul, B. Al-Rawi, and M. Aboelaze
    Journal of Communications (JCM), Academy Publishers, 2(4), 49-56, June 2007.
  5. The Synthesis of Dependable Communication Networks for Automotive Systems
    N. Kandasamy and F. Aloul
    SAE Transactions Journal of Passenger Cars – Electronic and Electrical Systems, 2006-01-1333, V115-7, 667-674, March 2007.
    ISBN Number: 978-0-7680-1839-4
  6. Breaking Instance-Independent Symmetries in Exact Graph Coloring
    A. Ramani, F. Aloul, I. Markov, and K. Sakallah
    Journal of Artificial Intelligence Research (JAIR), Volume 26, pp. 289-322, August 2006.
  7. Efficient Symmetry Breaking for Boolean Satisfiability
    F. Aloul, K. Sakallah, and I. Markov
    IEEE Transactions on Computers (TC), 55(5), pp. 549-558, May 2006.
  8. Search Techniques for SAT-based Boolean Optimization
    F. Aloul
    Elsevier Journal of the Franklin Institute, Volume 343, Issues 5-6, pp. 436-447, 2006.
  9. MINCE: A Static Global Variable-Ordering Heuristic for SAT Search and BDD Manipulation
    F. Aloul, I. Markov, and K. Sakallah
    Journal of Universal Computer Science (JUCS), 10(12), pp. 1562-1596, Dec. 2004.
  10. 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 (TC), 53(6), pp. 688-696, June 2004.
  11. 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 (TCAD), 22(9), pp. 1117-1137, Sept. 2003.
  12. Satometer: How Much Have We Searched?
    F. Aloul, B. Sierawski, and K. Sakallah
    IEEE Transactions on Computer Aided Design (TCAD), 22(8), pp. 995-1004, Aug. 2003.

Book Chapters:

  1. Sensor Deployment for Failure Diagnosis in Networked Aerial Robots: A Satisfiability-Based Approach
    F. Aloul and N. Kandasamy
    Lecture Notes on Computer Science (LNCS), SAT 2007, vol. 4501, Springer, 369-376, May 2007.
    ISBN: 978-3-540-72787-3.
  2. Pollution Mapper for Urban Gulf Cities
    M. AbuJayyab, S. Al-Ahdab, M. Taji, Z. Al-Hamdani, F. Aloul
    Youth and Environment Research, Gulf Research Center, 59-64, December 2006.
    ISBN 9948-432-67-3
  3. Robust SAT-Based Search Algorithm for Leakage Power Reduction
    F. Aloul, S. Hassoun, K. Sakallah, and D. Blaauw
    Lecture Notes on Computer Science (LNCS), PATMOS 2002, vol. 2451, Springer, 167-177, 2002.
    ISBN 3-540-44143-3

Conferences and Workshops:

  1. M-Stock: Efficient Stock Monitoring for Mobile Users
    F. Aloul, A. Sagahyroon, N. Salem, O. Al-Omar, and S. Shehada
    3rd IEEE International Conference on Modeling, Simulation, and Applied Optimization, (ICMSAO), Sharjah, UAE, January 2009.
  2. On Detecting Port Scanning using Fuzzy Based Intrusion Detection Systems
    W. Hajj, F. Aloul, and Z. Trabelsi
    IEEE International Wireless Communications and Mobile Computing Conference (IWCMC), Crete Island, Greece, August 2008.
  3. Mobile RFID Tracking System
    A. Al-Ali, F. Aloul, N. Aji, A. AlZarouni, and N. Fakhro
    3rd IEEE International Conference on Information & Communication Technologies: From Theory to Applications (ICTTA), Damascus, Syria, April 2008.
  4. Routing and Wavelength Assignment in Optical Networks using Boolean Satisfiability
    F. Aloul, B. Al-Rawi, M. Aboelaze
    5th Annual IEEE Consumer Communications and Networking Conference (CCNC), Las Vegas, NV, January 2008.
  5. Symmetry Breaking in Local Search for Unsatisfiability
    F. Aloul, Ines Lynce, and Steven Prestwich
    7th International Workshop on Symmetry and Constraint Satisfaction Problems (SymCon), Providence, RI, September 2007.
  6. Wireless Security in UAE: A Survey Paper
    A. Kalbasi, O. Alomar, M. Hajipour, and F. Aloul
    4th IEEE GCC Conference, Bahrain, November 2007.
  7. Solving the University Class Scheduling Problem Using Advanced ILP Techniques
    A.Wasfy and F. Aloul
    4th IEEE GCC Conference, Bahrain, November 2007.
    Won the Best Student Paper Award.
  8. Solving Employee Timetabling Problems Using Boolean Satisfiability
    F. Aloul, B. Al-Rawi, A. Al-Farra, and B. Al-Roh
    IEEE Innovations in Information Technology Conference (IIT), Dubai, UAE, November 2006.
  9. PolluMap: A Pollution Mapper for Cities
    M. AbuJayyab, S. Al Ahdab, M. Taji, Z. Al Hamdani, and F. Aloul
    IEEE Innovations in Information Technology Conference (IIT), Dubai, UAE, November 2006.
    Won the first place in the Gulf Research Center (GRC) Environmental Competition, 2006.
  10. Identifying the Shortest Path in Large Networks Using Boolean Satisfiability
    F. Aloul, B. Al-Rawi, and M. Aboelaze
    IEEE International Conference on Electrical and Electronics Engineering (ICEEE), Mexico, September 2006.
  11. Sensor Selection and Placement for Failure Diagnosis in Wireless Sensor Networks: Application to Unmanned Aerial Vehicle Networks
    N. Kandasamy, F. Aloul, and J. Koo
    IEEE International Conference on Robotics and Automation (ICRA), Orlando, Florida, pp.2182-2187, May 2006.
  12. Estimation of the Weighted Maximum Switching Activity in Combinational CMOS Circuits
    F. Aloul and A. Sagahyroon
    IEEE International Symposium on Circuits and Systems (ISCAS), Kos, Greece, pp. 2929-2932, May 2006.
  13. Maximum Power-Up Current Estimation in Combinational CMOS Circuits
    A. Sagahyroon and F. Aloul
    IEEE Mediterranean Electro-technical conference (MELECON), Malaga, Spain, pp. 70-73, May 2006.
  14. The Synthesis of Dependable Communication Networks for Automotive Systems
    N. Kandasamy and F. Aloul
    SAE World Congress (SAE), Detroit, Michigan, Paper No. 2006-01-1333, April 2006.
  15. Exciting Stuck-Open faults in CMOS Circuits Using ILP Techniques
    F. Aloul, A. Sagahyroon, and B. Al-Rawi
    IEEE International Conference on Computer Systems and Applications (AICCSA), Sharjah, UAE, pp. 409-414, March 2006.
  16. 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, January 2005.
  17. On Solving Optimization Problems Using Boolean Satisfiability
    F. Aloul
    International Conference on Modeling, Simulation, and Applied Optimization, (ICMSAO), Sharjah, UAE, 2005.
  18. A Call Admission Protocol for Cellular Multimedia Networks
    M. Aboelaze and F. Aloul
    6th World Wireless Congress (WWC), San Francisco, USA, 2005.
  19. Current and Future Trends in Sensor Networks: A Survey
    M. Aboelaze and F. Aloul
    IEEE International Conference on Wireless and Optical Communications Networks (WOCN), Dubai, UAE, pp. 551-555, March 2005.
  20. 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.
  21. 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.
  22. 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.
  23. Shatter: Efficient Symmetry-Breaking for Boolean Satisfiability
    F. Aloul, I. Markov, and K. Sakallah
    Design Automation Conference (DAC), Anaheim, California, pp. 836-839, 2003.
  24. 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.
  25. 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.
  26. 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.
  27. 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.

  28. Satometer: How Much Have We Searched?
    F. Aloul, B. Sierawski, and K. Sakallah
    Design Automation Conference (DAC), New Orleans, Louisiana, pp. 737-742, 2002.
  29. 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.

  30. 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.

  31. 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.

  32. 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.

  33. 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.

  34. 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]

  35. 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.

  36. 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]

  37. 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.

  38. 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.

  39. 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.

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

  41. 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]

  42. 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.

  43. 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.

  44. 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.

 

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.

Tutorials

  1. Invited Tutorial: Symmetry Detection and Breaking for Boolean Satisfiability
    F. Aloul
    International Symmetry Conference, Edinburgh, UK, January 2007.
  2. Information Security: From Theory to Practice
    F. Aloul and A. Khatib
    IEEE Innovations in Information Technology Conference (IIT), Dubai, UAE, 2006.
  3. Boolean Satisfiability: Theory and Applications
    F. Aloul
    First International Conference on Modeling, Simulation, and Applied Optimization (ICMSAO), Sharjah, UAE, 2005.

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
    United States Patent 20040078674, Billions of Operations Per Second Inc. (BOPS), Mountain View, California, 2004.

Invited Talks / Demos

  1. Symmetry-Detection and Breaking for Boolean Satisfiability
    F. Aloul
    Drexel University, Philadelphia, PA, January 2007.

  2. Symmetry-Detection and Breaking for Boolean Satisfiability
    F. Aloul
    Intel Corporation, Portland, Oregon, July 2005.

  3. Symmetry-Detection and Breaking for Boolean Satisfiability
    F. Aloul
    Tufts University, Boston, Massachusetts, April 2005.

  4. Symmetry Breaking for Pseudo-Boolean Formulas
    F. Aloul
    Microsoft Research, Redmond, Washington, December 2003.

  5. Scalable Algorithms for Boolean Satisfiability Enabled by Problem Structure
    F. Aloul
    Microsoft Research, Redmond, Washington, May 2003.

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

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

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

  9. Search-Based SAT Using Zero-Suppressed BDDs
    F. Aloul, M. Mneimneh, and K. Sakallah
    University Booth, Design Automation Conference (DAC), New Orleans, Louisiana, June 2002.
  10. SATIRE – An Incremental SAT Solver
    F. Aloul, M. Mneimneh, and K. Sakallah
    University Booth, Design Automation Conference (DAC), Las Vegas, Nevada, June 2001.
  11. An Experimental Exploration of SAT Problem Hardness
    F. Aloul
    IPoCSE Symposium, University of Michigan, 2000.
  12. An Exploration of Boolean Satisfiability Solvers and their Application in Hardware Verification
    F. Aloul
    3rd Ph.D. Forum, Design Automation Conference (DAC), Los Angeles, California, 2000.
  13. GRASP – SAT Solver
    F. Aloul, V. Kravets, and K. Sakallah
    University Booth, Design Automation Conference (DAC), Los Angeles, California, June 2000.
  14. 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

Newspaper Clips