ORA Thesis: "On the bridge between constraint satisfaction and Boolean satisfiability" - uuid:53bf6d0e-74eb-4c50-a1a2-c8da6773beae

45 views

Thesis

Links & Downloads

Local copy not available for download in ORA



http://ora.ox.ac.uk/objects/ora:6542

Reference: Justyna Petke, (2012). On the bridge between constraint satisfaction and Boolean satisfiability. DPhil. University of Oxford.

Citable link to this page: http://ora.ox.ac.uk/objects/uuid:53bf6d0e-74eb-4c50-a1a2-c8da6773beae
 
Title: On the bridge between constraint satisfaction and Boolean satisfiability

Abstract:

A wide range of problems can be formalized as a set of constraints that need to be satisfied. In fact, such a model is called a constraint satisfaction problem (CSP). Another way to represent a problem is to express it as a formula in propositional logic, or, in other words, a Boolean satisfiability problem (SAT). In the quest to find efficient algorithms for solving instances of CSP and SAT specialised software has been developed. It is, however, not clear when should we choose a SAT-solver over a constraint solver (and vice versa). CSP-solvers are known for their domain-specific reasoning, whereas SAT-solvers are considered to be remarkably fast on Boolean instances. In this thesis we tackle these issues by investigating the connections between CSP and SAT.

In order to answer the question why SAT-solvers are so efficient on certain classes of CSP instances, we first present the various ways one can encode a CSP instance into SAT. Next, we show that with some encodings SAT-solvers simulate the effects of enforcing a form of local consistency, called k-consistency, in expected polynomial-time. Thus SAT-solvers are able to solve CSP instances of bounded-width structure efficiently in contrast to conventional constraint solvers. By considering the various ways one can encode CSP domains into SAT, we give theoretical reasons for choosing a particular SAT encoding for several important classes of CSP instances. In particular, we show that with this encoding many problem instances that can be solved in polynomial-time will still be easily solvable once they are translated into SAT. Furthermore, we show that this is not true for several other encodings.

Finally, we compare the various ways one can use a SAT-solver to solve the classical problem of the pigeonhole principle. We perform both theoretical and empirical comparison of the various encodings. We conclude that none of the known encodings for the classical representation of the problem will result in an efficiently-solvable SAT instance. Thus in this case constraint solvers are a much better choice.


Digital Origin:Born digital
Type of Award:DPhil
Level of Award:Doctoral
Awarding Institution: University of Oxford
Notes:This thesis is not currently available via ORA.
About The Authors
institutionUniversity of Oxford
facultyMathematical,Physical & Life Sciences Division - Computer Science,Department of
oxfordCollegeSt John's College
 
Contributors
Prof Peter Jeavons More by this contributor
RoleSupervisor
 
Bibliographic Details
Issue Date: 2012
Copyright Date: 2012
Identifiers
Urn: uuid:53bf6d0e-74eb-4c50-a1a2-c8da6773beae
Item Description
Type: thesis;
Language: en
Keywords:
Subjects:
Relationships
Member of collection : ora:thesis
Alternate metadata formats
Rights
Copyright Holder: Justyna Petke
Terms of Use: Click here for our Terms of Use