SAT with Global Constraints

  • Author / Creator
    Chowdhury, Md Solimul
  • Propositional satisability (SAT) has been a dominant tool in solving some practical NP-complete problems. However, SAT also has a number of weaknesses, including its inability to compactly represent numerical constraints and its low level, unstructured language of clauses. In contrast, Constraint Programming (CP) has been widely used for scheduling and solving combinatorial search problems. In this thesis, we develop a tight integration of SAT with CP, called SAT(gc), which embeds global constraints, one of the most efficient features of CP, into SAT. We devise a DPLL-based algorithm for a SAT(gc) solver. A prototype system is implemented by integrating the state of the art SAT solver Zchaff and the generic constraint solver named Gecode. Experiments are carried out for benchmarks from puzzle domains and planning domains to reveal insights in compact representation, solving effectiveness, and novel usabilities of the new framework.

  • Subjects / Keywords
  • Graduation date
  • Type of Item
  • Degree
    Master of Science
  • DOI
  • License
    This thesis is made available by the University of Alberta Libraries with permission of the copyright owner solely for non-commercial purposes. This thesis, or any portion thereof, may not otherwise be copied or reproduced without the written consent of the copyright owner, except to the extent permitted by Canadian copyright law.
  • Language
  • Institution
    University of Alberta
  • Degree level
  • Department
    • Department of Computing Science
  • Supervisor / co-supervisor and their department(s)
    • You, Dr. Jia-Huai (Computing Science)
  • Examining committee members and their departments
    • Reformat, Dr. Marek (Electrical and Computer Engineering)
    • Müller, Dr. Martin (Computing Science)