You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

Locality and Hard SAT-Instances

Issue title: SAT 2005 Competitions and Evaluations

Guest editors: Daniel Le Berre and Laurent Simon

Article type: Research Article

Authors: Markström, Klas

Affiliations: Department of Mathematics, Umeå University, SE-901 87 Umeå, Sweden. E-mail: [email protected]

Keywords: satisfiability, hard instances, resolution, graphs, density

DOI: 10.3233/SAT190024

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 2, no. 1-4, pp. 221-227, 2006

Received 1 October 2005
|
Revision received 1 December 2005
|
Published: 1 March 2006
Get PDF open access

Abstract

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.

Show more