DOI:
Abstract:
The evaluation of incomplete satisfiability solvers depends critically on the availability of hard satisfiable instances. A plausible source of such instances are k-CNF formulas whose clauses are chosen uniformly at random among all clauses satisfying some randomly chosen truth assignment A. Unfortunately, instances generated in this manner are relatively easy and can be solved efficiently by practical heuristics. Roughly speaking, as the number of clauses is increased, A acts as a stronger and stronger attractor. Motivated by recent results on the geometry of the space of solutions for random k-SAT and NAE-k-SAT instances, we propose a very simple twist on this model that greatly increases the hardness of the resulting formulas. Namely, in addition to forbidding the clauses violated by the hidden assignment A, we also forbid the clauses violated by its complement, so that both A and the complement of A are satisfying. It appears that under this "symmetrization" the effects of the two attractors largely cancel out, making it much harder for an algorithm to "feel" (and find) either one. We give theoretical and experimental evidence supporting this assertion.