Generating hard SAT/CSP instances using expander graphs
MetadataShow full item record
In this paper we provide a new method to generate hard k-SAT instances. We incrementally construct a high girth bipartite incidence graph of the k-SAT instance. Having high girth assures high expansion for the graph, and high expansion implies high resolution width. We have extended this approach to generate hard n-ary CSP instances and we have also adapted this idea to increase the expansion of the system of linear equations used to generate XORSAT instances, being able to produce harder satisfiable instances than former generators.
Is part ofProceedings of the twenty-third National Conference on Artificial Intelligence, 2008, p. 1442-1443
European research projects
Showing items related by title, author, creator and subject.
Ansótegui Gil, Carlos José; Béjar Torres, Ramón; Fernàndez Camon, César; Mateu Piñol, Carles (Springer Verlag, 2008)In this paper we provide a new method to generate hard k-SAT instances. Basically, we construct the bipartite incidence graph of a k-SAT instance where the left side represents the clauses and the right side represents ...
Ansótegui Gil, Carlos José; Béjar Torres, Ramón; Fernàndez Camon, César; Gomes, Carla; Mateu Piñol, Carles (Springer, 2011)Sudoku problems are some of the most known and enjoyed pastimes, with a never diminishing popularity, but, for the last few years those problems have gone from an entertainment to an interesting research area, a twofold ...
Ansótegui Gil, Carlos José; Béjar Torres, Ramón; Fernàndez Camon, César; Mateu Piñol, Carles (Association for the Advancement of Artificial Intelligence, 2007)Tractable cases of the binary CSP are mainly divided in two classes: constraint language restrictions and constraint graph restrictions. To better understand and identify the hardest binary CSPs, in this work we propose ...