Organizing Committee |
| Yael Ben-Haim, IBM Research yaelbh@il.ibm.com |
| Yehuda Naveh, IBM Research naveh@il.ibm.com |
|
Program Committee |
| Fahiem Bacchus, U. Toronto, Canada |
| Yael Ben-Haim, IBM Research, Israel |
| Lucas Bordeaux, Microsoft Research, UK |
| Alan Frisch, U. York, UK |
| Enrico Giunchiglia, U. Genova, Italy |
| Youssef Hamadi, Microsoft Research, UK |
| Ian Miguel, U. St. Andrews, UK |
| Yehuda Naveh, IBM Research, Israel |
| Steven Prestwich, U. College Cork, Ireland |
| Meinolf Sellmann, IBM Research, USA |
| Ofer Strichman, Technion, Israel |
| Toby Walsh, NICTA, Australia |
| |
|
|
CSPSAT 2011 Workshop
First International Workshop on the Cross-Fertilization Between CSP and SAT in conjunction with SAT 2011
Ann Arbor, Michigan, USA
June 18, 2011
PCS: a proof-producing CSP solver
Ofer Strichman
PCS is a CSP solver that can produce a machine-checkable deductive proof in case it decides that the input problem is unsatisfiable. The roots of the proof may be nonclausal constraints, whereas the rest of the proof is based on resolution of signed clauses, ending with the empty clause. PCS uses parameterized, constraint-specific inference rules in order to bridge between the nonclausal and the clausal parts of the proof. The consequent of each such rule is a signed clause that is 1) logically implied by the nonclausal premise, and 2) strong enough to be the premise of the consecutive proof steps. The resolution process itself is integrated in the learning mechanism, and can be seen as a generalization to CSP of a similar solution that is adopted by competitive SAT solvers.
| |
|
|