×

zbMATH — the first resource for mathematics

Locality and hard SAT-instances. (English) Zbl 1113.68483
Summary: We construct a family of SAT-instances 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.

MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68R10 Graph theory (including graph drawing) in computer science
Keywords:
satisfiability
Software:
UnitWalk
PDF BibTeX XML Cite