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
- 1st place in Microsoft
Imagine Cup Gulf Competition, UAE, 2008.
- 1st place in National Mobile Phone Application
Contest (NMAC), UAE, 2008.
- Best Student Paper Award at the IEEE GCC
Conference, Bahrain, 2007.
- 3rd place in the Made-In-Arab
World Competition (MIA), Egypt, 2007.
- 2nd place in National Mobile Phone Application Contest (NMAC), UAE, 2007.
- Short-listed among 4 top participants in
the Microsoft Imagine Cup Gulf Competition, UAE, 2007.
- 1st place in Green Gulf Youth
Conference Competition, Sharjah, UAE, 2006.
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 -

Journals:
- 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.
- 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.
- 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.
- 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.
- 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
- 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.
- 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.
- Search Techniques
for SAT-based Boolean Optimization
F. Aloul
Elsevier Journal of the Franklin
Institute, Volume 343, Issues 5-6, pp. 436-447, 2006.
- 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.
- 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.
- 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.
- 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:
- 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.
- 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
- 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:
- 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.
- 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.
- 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.
- 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.
- 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.
- Wireless Security
in UAE: A Survey Paper
A. Kalbasi, O. Alomar, M. Hajipour, and F. Aloul
4th IEEE GCC Conference, Bahrain, November 2007.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- On Solving
Optimization Problems Using Boolean Satisfiability
F. Aloul
International Conference on
Modeling, Simulation, and Applied Optimization, (ICMSAO), Sharjah,
UAE, 2005.
- A Call Admission
Protocol for Cellular Multimedia Networks
M. Aboelaze and F. Aloul
6th World Wireless
Congress (WWC), San Francisco,
USA, 2005.
- 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.
- 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.
- 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.
- 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.
- Shatter: Efficient
Symmetry-Breaking for Boolean Satisfiability
F. Aloul, I. Markov, and K. Sakallah
Design Automation Conference (DAC), Anaheim, California,
pp. 836-839, 2003.
- 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.
- 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.
- 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.
- 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.
- Satometer: How
Much Have We Searched?
F. Aloul, B. Sierawski, and K. Sakallah
Design Automation Conference (DAC), New Orleans, Louisiana, pp.
737-742, 2002.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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]
- 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.
- 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]
- 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.
- 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.
- 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.
- Backtrack Search
Using ZBDDs
F. Aloul, M. Mneimneh, and K. Sakallah
International Workshop on Logic Synthesis (IWLS), Lake Tahoe, California,
pp. 293-297, 2001.
- 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]
- 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.
- 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.
- 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:
- 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.
- 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.
- Satometer: How Much
Have We Searched?
F. Aloul, B. Sierawski, and K. Sakallah
Technical Report CSE-TR-457-02, University of Michigan,
June 2002.
- 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
- Invited Tutorial: Symmetry
Detection and Breaking for Boolean Satisfiability
F. Aloul
International Symmetry Conference, Edinburgh, UK,
January 2007.
- Information Security: From Theory to
Practice
F. Aloul and A. Khatib
IEEE Innovations in Information Technology Conference (IIT), Dubai, UAE, 2006.
- Boolean Satisfiability: Theory and
Applications
F. Aloul
First International Conference on
Modeling, Simulation, and Applied Optimization (ICMSAO), Sharjah, UAE,
2005.
Patents
- 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
- Symmetry-Detection and Breaking for
Boolean Satisfiability
F. Aloul
Drexel University, Philadelphia,
PA, January 2007.
- Symmetry-Detection and Breaking for
Boolean Satisfiability
F. Aloul
Intel Corporation, Portland,
Oregon, July 2005.
- Symmetry-Detection and Breaking for Boolean
Satisfiability
F. Aloul
Tufts University, Boston,
Massachusetts, April 2005.
- Symmetry Breaking for Pseudo-Boolean
Formulas
F. Aloul
Microsoft Research, Redmond,
Washington, December 2003.
- Scalable Algorithms for Boolean
Satisfiability Enabled by Problem Structure
F. Aloul
Microsoft Research, Redmond,
Washington, May 2003.
- 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.
- Generic ILP vs. Specialized 0-1 ILP:
An Update
F. Aloul
IPoCSE Symposium, University
of Michigan,
2002.
- Faster SAT and Smaller BDDs Through
Efficient Problem Partitioning
F. Aloul
GFP Annual Conference, Semiconductor Research Corporation (SRC), Dallas, Texas,
September 2002.
- 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.
- SATIRE – An Incremental SAT Solver
F. Aloul, M. Mneimneh, and K. Sakallah
University Booth, Design Automation Conference (DAC), Las Vegas, Nevada,
June 2001.
- An Experimental Exploration of SAT
Problem Hardness
F. Aloul
IPoCSE Symposium, University of Michigan,
2000.
- 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.
- GRASP – SAT Solver
F. Aloul, V. Kravets, and K. Sakallah
University Booth, Design
Automation Conference (DAC), Los
Angeles, California,
June 2000.
- An Experimental Study of
Satisfiability Search Heuristics
F. Aloul
IPoCSE Symposium, University of Michigan,
1999.
Tools
- 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.
- PBS
Incremental pseudo-Boolean backtrack search SAT solver and optimizer
(handles CNF and 0/1 inequality forms)
- SHATTER
Identifies symmetry-breaking clauses in CNF instances (preprocessing tool)
- SATOMETER
Measures progress of backtrack-search SAT solvers
- ZBDDLIB
New ZBDD operations added to the CUDD package
- GRASP
Backtrack-search SAT solver
- MINCE
Static global variable ordering for SAT & BDDs (preprocessing tool)
- SATIRE
Incremental SAT solver
Benchmarks
Newspaper
Clips