Exploring a Two-Solver Architecture for Clause Learning CSP Solvers

摘要

Many real world problems can be encoded as Constraint Satisfaction Problems (CSPs). Constraint satisfaction problems contain variables over finite domains, as well as constraints over these variables. There exists many solvers that can solve these problems efficiently. Once these problems are solved, their solutions correspond to solutions of the real world problem the CSP encodes.;Similarly, many problems can be encoded as instances of the Satisfiability Problem (SAT). In SAT all the variables are binary propositions, and the only kind of constraint they allow is the disjunction of a set of variables. SAT and CSP are closely related, and they both are NP-complete.;These two approaches have their own advantages and disadvantages. SAT solvers perform clause learning, which prevents them from visiting similar subtrees in the search tree. The advantage of CSP solvers is that the CSP instances contain higher level constraints, which allows better reasoning. Recently, methods combining the advantages of SAT and CSP solvers have emerged. In such methods, solvers maintain a propositional representation of the CSP problem, and perform clause learning over this representation. Such solvers are called "clause learning CSP solvers".;However, the question of how to handle constraints in such solvers is unresolved. For each constraint, a solver must choose whether to encode the constraint entirely in SAT or use a special purpose propagator, and this choice also determines the propagation strength and efficiency. Different choices perform better in different scenarios, hence hybrid methods which can be adaptive are promising.;In this thesis, we propose an alternative architecture for clause learning CSP solvers, which incorporates two solvers of different strength. One of the solvers directs the search using fast and weak propagators. Once it gets into a dead end, it produces a conflict clause, and asks the other solver to enhance it using stronger but slower propagators. In this way, the slower propagators are run only whenever they are likely to be needed, instead of each node in the search tree. We instantiate this architecture in different ways, and perform experiments to demonstrate the trade-offs between these instantiations.