| Organizing Committee |
 | Yael Ben-Haim, IBM Research
yaelbh@il.ibm.com |
| Valentin Mayer-Eichberger
vale1410@gmail.com |
| Yehuda Naveh, IBM Research
naveh@il.ibm.com |
| |
| Program Committee |
| Yael Ben-Haim, IBM Research, Israel |
| Alan Frisch, University of York, UK |
| Enrico Giunchiglia, University of Genova, Italy |
| George Katsirelos, INRA, France |
| Valentin Mayer-Eichberger, NICTA and University of New South Wales, Australia |
| Ian Miguel, University of St Andrews, UK |
| Nina Narodytska, Carnegie Mellon University, USA |
| Yehuda Naveh, IBM Research, Israel |
| Steve Prestwich, University College Dublin, Ireland |
| Bart Selman, Cornell University, USA |
| Ofer Strichman, Technion, Israel |
| Toby Walsh, NICTA and University of New South Wales, Australia |
 | |
|
|
CSPSAT 2015 Workshop
|
Fifth International Workshop on the Cross-Fertilization Between CSP and SAT
In conjunction with CP 2015
Cork, Ireland
August 31, 2015
There are no CNF problems
Peter Stuckey, University of Melbourne and NICTA
Abstract: SAT technology has improved rapidly in recent years, to the point now where it can solve CNF problems of immense size. But solving CNF problems ignores one important fact: there are NO problems that are originally CNF. All the CNF that SAT solvers tackle is the result of modelling some real world problem, and mapping the high-level constraints and decisions modelling the problem into clauses on binary variables. But by throwing away the high level view of the problem SAT solving may have lost a lot of important insight into how the problem is best solved. In this talk I will hope to persuade you that by keeping the original high level model of the problem one can realise immense benefits in solving hard real world problems, even if finally the underlying solving technology is basically SAT.
| |
|
|
