The INI has a new website!

This is a legacy webpage. Please visit the new site to ensure you are seeing up to date information.

Skip to content



A class of SAT-instances which are hard for resolution based SAT-solvers

Markstrom, K (Umea)
Friday 17 February 2006, 11:00-12:00

Seminar Room 1, Newton Institute


In this talk we will construct a class of SAT-formulae based on Eulerian graphs. The satisfiablility of these formulae depend on the number of edges in the Eulerian graph and it is easy to construct extremely similar formulae which differ in satisfiabillity. The structure of the graph can also be used to tune the formulae to be resitant to several modern enhancements of the basic DPLL-algorithm. Some possible connections to the hardness of random K-SAT formulae will also be mentioned.

Back to top ∧