Summary of Research
My research interests involve 4 areas (click on each area for list of papers):
  1. SAT Algorithms & SAT Applications - Development of powerful Boolean Satisfiability (SAT) solvers & Using advanced SAT technologies to solve challenging Engineering problems.
  2. IT Security - Phishing Attacks, Security Awareness, Wireless Security, RFID Security, Multi-Factor Authentication, Intrusion Detection Systems (IDS).
  3. Applied Engineering - Health Monitoring, Pollution Monitoring, Stock Monitoring, Mobile Applications, RFID/WiFi Tracking and Sensor Networks.
  4. Engineering Education - Multidisciplinary Engineering Education.

(1.A) SAT Algorithms

Combinatorial problems, e.g. decision and optimization problems, 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 work involve:

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, June 2008.

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. Symmetry in Boolean Satisfiability
    F. Aloul
    Symmetry, 2(2), 1121-1134, June 2010.

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

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 (TC), 55(5), pp. 549-558, May 2006.

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

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

  1. Dynamic Symmetry-Breaking for Boolean Satisfiability
    F. Aloul, A. Ramani, I. Markov, and K. Sakallah
    Annals of Mathematics and Artificial Intelligence (AMAI), Springer, 57(1), 59-73, 2010.

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, Dec. 2004.

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

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.

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

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 (TCAD), 22(8), pp. 995-1004, Aug. 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
    Design, Automation, and Test in Europe Conference (DATE), Paris, France, pp. 1082, 2002.

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

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

Solving optimization problems with SAT

  1. Search Techniques for SAT-based Boolean Optimization
     F. Aloul
    Elsevier Journal of the Franklin Institute, Volume 343, Issues 5-6, pp. 436-447, 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
    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
    International Workshop on Logic Synthesis (IWLS), Dana Point, California, pp. 117-122, 2000.

(1.B) 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. Multipath Detection Using Boolean Satisfiability Techniques
    F. Aloul and M. El Tarhuni
    Journal of Computer Networks and Communications (JCNC), vol. 2011, Article ID 365107, 2011.

  2. A Multipath Detection Scheme Using SAT
     M. Tarhuni and F. Aloul
    IEEE International Conference on Communications (ICC), Cape Town, South Africa, pp. 1-5, May 2010.

  3. PN Code Acquisition Using Boolean Satisfiability Techniques
     F. Aloul and M. Tarhuni
    IEEE Wireless Communications & Networking Conference (WCNC), Budapest, Hungary, pp. 1-6, 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 (TC), 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.

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

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 & Test Vector Generation

  1. Using SAT-Based Techniques in Low Power State Assignment
    A. Sagahyroon, F. Aloul, and A. Sudnitson
    Journal of Circuits, Systems, and Computers (JCSC), 20(8), 1605-1618, 2011.

  2. Using SAT-Based Techniques in Test Vectors Generation
    F. Aloul and A. Sagahyroon
    Journal of Advances in Information Technology (JAIT), Academy Publishers, 1(4), 153-162, November 2010.

  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.

Artificial Intelligence – Graph Coloring

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

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.
    Won the 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, pp. 1-5, November 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, Florida, pp. 2182-2187, May 2006.

PCI Bus Verification

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

(2) IT Security

Presents the results of several security awareness studies that were conducted in UAE in 2010. The studies evaluated the awareness of residents to 1) Phishing attacks, 2) Wireless attacks, and 3) RFID attacks. The paper shows the need for effective security awareness programs and presents several key factors that are necessary to develop a successful information security awareness program.

  1. The Need for Effective Information Security Awareness
    F. Aloul
    to appear in Journal of Advances in Information Technology (JAIT), 2012.

Presents a novel approach, based on fuzzy logic, to detect port scanning attacks using Snort. Experiments are carried out in both wired and wireless networks. The results show that applying fuzzy logic adds to the accuracy of determining bad traffic.

  1. Updating Snort with a Customized Controller to Thwart Port Scanning
    W. Hajj, H. Hajj, Z. Trabelso, and F. Aloul
    Security and Communication Networks (SCN), Wiley InterScience, 4(8), 807-814, August 2011.

Proposes a One Time Password (OTP) generation algorithm for mobile phones. An SMS-based algorithm for mobile phones is also proposed. Both algorithms are implemented and tested.

  1. Multi Factor Authentication Using Mobile Phones
    F. Aloul, S. Zahidi, and W. El-Hajj
    International Journal of Mathematics and Computer Science (IJMCS), 4(2), 65-80, 2009.

Evaluates the wireless security awareness in UAE. 3890 access points were identified, of which 46% were encrypted only.

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

(3) Applied Engineering

Efficient Pollution Monitoring in Urban Cities

  1. Mobile GPRS-Sensors Array for Air Pollution Monitoring
    A. Al-Ali, I. Zualkernan, and F. Aloul
    IEEE Sensors Journal, 10(10), 1666-1671, October 2010.

  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. 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, pp. 1-5, November 2006.
    Won the first place in the Gulf Research Center (GRC) Environmental Competition, 2006.

Efficient Patient's Health Monitoring

  1. Monitoring Patients' Signs Wirelessly
    A. Sagahyroon, F. Aloul, A. Al-Ali, M. Bahrololoum, F. Makhsoos, and N. Hussein
    Journal of Medical Imaging and Health Informatics (JMIHI), 1(3), 252-255, September 2011.

Efficient Stock Monitoring using Mobile Phones

  1. Efficient Stock Monitoring for Mobile Users
    F. Aloul, A. Sagahyroon, N. Salem, O. Al-Omar, S. Shehada, B. Al-Rawi
    Elsevier Journal of the Franklin Institute, 348(7), 1298-1311, September 2011.

Tracking Objects using RFID and WiFi

  1. Using Mobiles for On Campus Location Tracking
     F. Aloul, A. Sagahyroon, A. Al-Shami, I. Al-Midfa, and R. Moutassem
    7th ACM International Conference on Advances in Mobile Computing & Multimedia (MoMM), Kuala Lumpur, Malaysia, December 2009.

  2. Mobile RFID Tracking System
     A. Al-Ali, F. Aloul, N. Aji, A. AlZarouni, and N. Fakhro
    IEEE International Conference on Information & Communication Technologies: From Theory to Applications (ICTTA), Damascus, Syria, pp. 1-4, April 2008.

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
    IEEE International Conference on Wireless and Optical Communications Networks (WOCN), Dubai, UAE, pp. 551-555, March 2005.

Microprocessor Verification

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

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

Ad hoc Networks

  1. Transmission Coordination for Ad hoc Networks
    A. Kiniy, S. Webery, F. Aloul, and N. Kandasamy
    44th Conference on Information Sciences and Systems (CISS), Princeton, New Jersey, pp. 1-6, March 2010.

(4) Engineering Education

Describes improvements made to the "English for Engineers" course at AUS, which include the introduction of a design project to multidisciplinary engineering teams.

  1. Engineering Communication Interface: An Engineering Multidisciplinary Project
    D. Prescott T. El-Sakran, L. Albasha, F. Aloul, and Y. Al-Assaf
    to appear in Journal of US-China Education Review, 2011.

For more information, please contact Dr. Fadi Aloul (faloul@aus.edu).

Return to main page