טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
Ph.D Thesis
Ph.D StudentVeksler Michael
SubjectConstraint Solving with a Learning Mechanism based on
General Constraints
DepartmentDepartment of Industrial Engineering and Management
Supervisor Professor Ofer Strichman
Full Thesis textFull thesis text - English Version


Abstract

The Constraint Satisfaction Problem (CSP) is a known NP-hard problem in the field of Artificial Intelligence. As part of this thesis, I developed a new CSP solver called HCSP, which has several novel capabilities and a reasoning engine that is highly competitive and on many benchmarks the fastest available. It is the first CSP solver capable of generating machine-checkable proofs in case the formula is unsatisfiable (based on an inference system called signed resolution), and also the first CSP solver that is able to generate a Craig interpolant. Both of these capabilities were so far only available in SAT solvers, and the main challenge in adapting them to CSP is the need to bridge between the general constraints comprising the input problem, and an inference system that provides the building blocks of a proof.


HCSP uses novel algorithms that work directly on CSP (i.e., not via translation to CNF SAT like some other CSP solvers) and are able to learn stronger constraints than a SAT solver. During conflict analysis, it is able to learn new non-clausal constraints. For example, from x <= y and y<= z    it may infer that x <= z, although x <= z is not an existing predicate in the formula (in contrast to theory propagation in SMT solvers).

This capability is based on a new general inference rule, Combine, which can be seen as a generalization of CNF resolution.


The thesis is comprised of a collection of new algorithms and of known algorithms adapted from other domains (mostly SAT) to the realm of CSP.