Hemal A Lal - Research page

Research Interest:
   - Solving Satisfiability problems, and Satisfiability Solvers.
   - Artifical Intelligence
   - Data Mining and Knowledge Discovery

   Current Projects
   Give It A Thought


Master's Thesis:
    - "Design and Implement a Finite Domain Satisfiability Solver"
       Thesis Proposal [pdf , ps]
       Thesis Report [pdf , ps]
       Advisor : Dr Hudson Turner


Work Done:

1. A SAT Solver.
   current features :
   - Finite/Boolean domain benchmark creator
   - Model verifier
   - Boolean to Finite domain convertor
   - Finite to Boolean domain convertor - Quadratic Encoding
   - Finite to Boolean domain convertor - Linear Encoding
   - Solve SAT problems using Stochastic Local Search
   - Solve SAT problems using Random Backtracking
   - Solve SAT problems using Chronological Backtracking
   - Solve SAT problems using Non-Chronological Backtracking with Conflict Based Learning
2. Generating Benchmark and finding relationship between variables, clauses, and the domains (Phase Transitions)
   current observation :
   - As the ratio of #clause to #variables increases, time required to solve
     also increase.
   - As the domain size increases, time required to solve also increases.

Future Work

1. Try some more heuristics to see the performance change
2. Improve Data Structures
3. Improve Conflict learning mechanism
4. Phase Transition for each domain size

Download

Here it is ... FDSolver.tar.gz...
This software has been tested on Solaris 9/10, RedHat Linux, with gcc version 3.2.2
This software is distributed under GNU OpenSource policy. You can ammend, redevelop, redistribute without the author knowledge
but you should be responsible for anything you do with it. The author does not provide any warranty. Please as a courtesy if
you find a bug or develop a better version do inform the author. Author would like to keep this as an ongoing project as time permits.

Related Papers:

1. Ines Lynce and Joao Marques-Silva. "Building State-of-the-Art SAT Solves."
2. Alan M. Frisch and Timothy J.Peugniez. "Solving Non-Boolean Satisfiability Problems with Stochastic Local Search." University of York, United Kingdom.
3. Mel Tsai. "Multivalued Boolean Satisfiability: MV-SAT." Final Project Report. University of Califonia Berkley. 1999.
4. Shweta Sinha. "A Finite Domain Solver." Thesis Report. University of Minnesota Duluth. 2003.
5. Matthew W. Moshewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. "Chaff: Engineering an Efficient SAT Solver."
6. Evgueni Goldberg, and Yakov Novikov. "BerkMin: a Fast and Robust Sat-Solver."
7. Slawomir Pilarski and Gracia Hu. "SAT with Partial Clauses and Back-Leaps."
8. Ines Lynce, L. Baptista, and Joao Marques-Silva. "Unrestricted Backtracking Algorithms for Satisfiability." Techincal Report. University of Lisbon, Portugal.
9. Ines Lynce, and Joao Marques-Silva. "Efficient Data Structures for Fast SAT Solvers." Techical Report. Cadence European Laboratories.
10. Cong Liu, Andreas Kuelmann, Matthew W.Moskewicz. " CAMA: A Multi Value Satisfiability Solver. " University of California at Berkeley.
11. Cong Liu, Andreas Kuelmann, Matthew W.Moskewicz. " A Search Algorithm for Multi-Valued Satisfiability Solver " University of California at Berkeley.
12. Joao Marques-Silva, Karen A. Sakallah. " GRASP - A New Search Algorithm for Satisfiability ".
13. Joao Marques-Silva, A. Bhalla, Ines Lynce." Heuristic Backtracking Algorithms for SAT " Technical University of Lisbon, Portugal.
14. Dimitris Achlioptas, Arthur Chtcherba, Gabriel Istrate, Cristopher Moore. "The Phase Transition in 1-in-k SAT and NAE 3-SAT".
15. Ke Xu, Wei LI "The SAT Phase Transition" Beijing University of Aeronautics and Astronautics.
16. Ian P. Gent, Toby Walsh. "The SAT Phase Transition" University of Edinburgh.
17. Fahiem Bacchus, Peter van Beek "On the Conversion between Non-Binary and Binary Constraint Satisfaction Problem".
18. Bart Selman, David Mitchell, Hector Levesque. "Generating Hard Satisfiability Problems".
19. Paul Beame, Henry Kautz, Ashish Sabharwal "Understanding the Power of Clause Learning".
20. Lintao Zhang, Conof F.Madigan, Matthew H.Moskewicz, Sharad Malik "Efficient Conflict Driver Learning in a Boolean Satisfiability Solver".


Links:
   - SATLib : The Satisfiability Library
   - SAT Live
   - Satisfiability.org
   - SAT 2004 Conference in Vancouver, Canada
   - zChaff Boolean Solver
   - Alan Frisch's site on solving non-boolean satisfiability problems
   - Joćo Marques Silva's Research Page
   - CiteSeer : Computer Science Papers (Search)

Contact:
    - lalx0004@d.umn.edu
 
 
 
Old Research Homepage