Summary of Research for Fadi Aloul

My research interests are in solving combinatorial problems, e.g. decision and optimization problems, which arise in various Engineering and Computer Science applications. In general, combinatorial problems are hard to solve and have a significantly large search space. Combinatorial algorithms work on effectively reducing the size of the search space and efficiently exploring the remaining space. Many combinatorial problems can be successfully modeled and solved using Boolean Satisfiability (SAT) technology.

My research has mainly focused on:

(1)    SAT Algorithms – Development of powerful Boolean Satisfiability (SAT) solvers.

(2)    SAT Applications – Using advanced SAT technologies to solve challenging Engineering problems.

(3)    Applied Engineering

 

(1) SAT Algorithms

Detecting and analyzing structural properties in SAT instances and using the properties to speed up search

Speeding up SAT search by statically detecting and breaking symmetries in 0/1 Integer Linear Programming (ILP) problems, i.e. SAT problems consisting of CNF and Pseudo Boolean (PB) constraints. This is a pre-processing process, i.e. constraints are added to the instance before SAT search. This work released the tool “ShatterPB”.

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

Speeding up SAT search by statically detecting and breaking symmetries in CNF SAT problems. This is a pre-processing process, i.e. constraints are added to the instance before SAT search. This work released the tool “Shatter”.

1.       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, September 2003.

Efficient construction of Symmetry-Breaking Predicates (SBPs) for SAT problems.

1.       Efficient Symmetry Breaking for Boolean Satisfiability
F. Aloul, K. Sakallah, and I. Markov
IEEE Transactions on Computers, 55(5), pp. 541-558, May 2006.

Using symmetry breaking to speed up local search solvers (i.e. incomplete solvers) in proving unsatisfiability of SAT instances.

1.       Symmetry Breaking in Local Search for Unsatisfiability
F Aloul, I. Lynce, and S. Prestwich
International Workshop on Symmetry and Constraint Satisfaction Problems (SymCon), Providence, RI, September 2007.

Speeding up SAT search by dynamically detecting and breaking symmetries. Constraints are added during the search process.

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

Using logic minimization to simplify symmetry-breaking predicates (SBPs) and speeding up the search process.

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

Speeding up SAT search and BDD construction by detecting sparsity in SAT instances. This is a static or pre-processing process, i.e. variables are re-ordered before SAT search or BDD construction. This work released the tools “MINCE” and “FORCE”.

1.       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, December 2004.

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

Relaxing SAT input format

Relaxing the input format of SAT solvers by allowing them to read CNF and linear inequalities constraints (also known as Pseudo-Boolean (PB) constraints or 0/1 ILP). This extends the application of SAT solvers to handle Boolean decision and optimization problems and allows for new applications to be tackled by SAT solvers. This work has lead to the release of a powerful award-winning 0-1 ILP solver “PBS”. PBS has been shown to compete with some of the best commercial 0-1 ILP solvers, e.g. CPLEX.

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.

Search space estimation in SAT

Estimating the percentage of the search space actually explored by a backtrack SAT solver. This work released the tool “Satometer”.

1.       Satometer: How Much Have We Searched?
F. Aloul, B. Sierawski, and K. Sakallah
IEEE Transactions on Computer Aided Design, 22(8), pp. 995-1004, August 2003.
Nominated for Best Paper Award.

Implicit constraint representation using ZBDDs in SAT

We show how to implicitly represent satisfiability instances using ZBDDs, and perform search using an efficient implementation of unit propagation on the ZBDD structure.

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

Solving optimization problems with SAT

1.       Search Techniques for SAT-Based Boolean Optimization
F. Aloul
Elsevier Journal of the Franklin Institute, vol. 343, Issues 5-6, pp. 436-447, August 2006.

Evaluation of conflict diagnosis and recursive learning in SAT

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

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

 

(2) SAT Applications

The significant advances in SAT solver technology over the last few years have lead to the successful deployment of SAT solvers in a wide range of applications. My research has contributed to the use of SAT solvers in solving challenging combinatorial problems arising in:

Wireless Communications

1.       PN Code Acquisition Using Boolean Satisfiability Techniques
F. Aloul and M. Tarhuni
IEEE Wireless Communications & Networking Conference (WCNC), Budapest, Hungary, April 2009.

FPGA routing

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

Global routing

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.

Power Reduction

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

Power Estimation

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

2.       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, May 2006.

3.       Maximum Power-Up Current Estimation in Combinational CMOS Circuits
A. Sagahyroon and F. Aloul
IEEE Mediterranean Electro-technical conference (MELECON), Malaga, Spain, May 2006.

4.       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, March 2006.

Artificial Intelligence – Graph Coloring

1.       Breaking Instance-Independent Symmetries in Exact Graph Coloring
A. Ramani, I. Markov, K. Sakallah, and F. Aloul
Journal of Artificial Intelligence Research (JAIR), vol. 26, August 2006.

Networking – Routing and Wavelength Assignments

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

Scheduling – University Classroom Assignment & Employee Timetabling

1.       Solving the University Class Scheduling Problem Using Advanced ILP Techniques
A. Wasfy and F. Aloul
IEEE GCC Conference, Bahrain, November 2007.
Best Student Paper Award

2.       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, 2006.

Fault Tolerance – Sensor selection and placement for failure diagnosis in wireless sensor networks.

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.       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, May 2006.

PCI Bus Verification

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

(3) Applied Engineering

Efficient pollution monitoring in urban cities

1.       Pollution Mapper for Urban Gulf Cities
M. AbuJayyab, S. Al-Ahdab, M. Taji, Z. Al-Hamdani, and F. Aloul
Youth and Environment Research, Gulf Research Center, 59-64, December 2006. ISBN 9948-432-67-3

2.       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, 2006.

Efficient stock monitoring using mobile phones

1.       M-Stock: Efficient Stock Monitoring for Mobile Users
F. Aloul, A. Sagahyroon, N. Salem, O. Al-Omar, S. Shehada
IEEE International Conference On Modeling, Simulation, and Applied Optimization (ICMSAO), Sharjah, UAE, January 2009.

Tracking objects using RFID

1.       Mobile RFID Tracking System
A. Al-Ali, F. Aloul, A. Sagahyroon, N. Aji, A. AlZarouni, N. Fakhro
3rd International Conference on Information & Communication Technologies: From Theory to Applications (ICTTA), April 2008.

IT Security

1.       On Detecting Port Scanning using Fuzzy Based Intrusion Detection System
W. Hajj, F. Aloul, and Z. Trabelsi
IEEE International Wireless Communications and Mobile Computing Conference (IWCMC), Greece, August 2008.

2.       Wireless Security in UAE: A Survey Paper
A. Kalbasi, O. Alomar, M. Hajipour, and F. Aloul
4th IEEE GCC Conference, Bahrain, November 2007.

Sensor Networks

1.       A Call Admission Protocol for Cellular Multimedia Networks
M. Aboelaze and F. Aloul
6th World Wireless Congress (WWC), San Francisco, USA, 2005.

2.       Current and Future Trends in Sensor Networks: A Survey
M. Aboelaze and F. Aloul
Second IFIP International Conference on Wireless and Optical Communications Networks (WOCN), Dubai, UAE, 2005.

Microprocessor Verification

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

Distributed Systems

Software-based methods were developed for implementing predictable and low-cost failure diagnosis and recovery in distributed embedded systems, e.g. automotive systems.

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

2.       The Synthesis of Dependable Communication Networks for Automotive Systems
N. Kandasamy and F. Aloul
SAE World Congress, Detroit, Michigan, April 2006.