Locality and hard SAT-instances
2006 (English)In: Journal on Satisfiability, Boolean Modeling and Computation, Vol. 2Article in journal (Refereed) Published
In this note we construct a family of SAT-instance based on Eulerian graphs which are aimed at being hard for resolution based SAT-solvers. We discuss some experiments made with instances of this type and how a solver can try to avoid at least some of the pitfalls presented by these instances. Finally we look at how the density of subformulae can influence the hardness of SAT instances.
Place, publisher, year, edition, pages
2006. Vol. 2
IdentifiersURN: urn:nbn:se:umu:diva-7601OAI: oai:DiVA.org:umu-7601DiVA: diva2:147272