Computer Science Colloquium
Thursday, October 31st, 4:15pm, room 9204/05
Tractable Classes and Practical Solving of CSPs.
Modern SAT (and CSP) solvers have achieved in recent years tremendous progress.
Although these problems are NP-complete, modern solvers now can deal with real instances of very large size, up to several millions of clauses and variables. However, they are sometimes ineffective on small instances. One natural way to improve their practical efficiency could be a better understanding of their good practical behavior. Unfortunately, we do not have to date, any analytical explanation of their efficiency. One approach would be to consider tractable classes (that are subsets of polynomial time solvable instances) that could be exploited by solvers. But today, there is a real gap between the state of the art on tractable classes, and the one of the implementation of efficient solvers.
In this talk, we present recent results on tractable classes of CSP, and try to suggest approaches which could give answers to a better understanding of the effectiveness of solvers.