Hiding Satisfying Assignments: Two are Better than One
Dimitris Achlioptas, Haixia Jia, Cristopher Moore

TL;DR
This paper introduces a symmetrized model for generating hard satisfiable instances of random k-SAT by ensuring both a hidden assignment and its complement are satisfying, significantly increasing problem difficulty.
Contribution
The paper proposes a novel symmetrization technique for generating hard satisfiable instances, balancing attractors to challenge algorithms more effectively.
Findings
Symmetrized instances are significantly harder for algorithms to solve.
Theoretical analysis supports increased hardness due to symmetrization.
Experimental results confirm the difficulty of the new model.
Abstract
The evaluation of incomplete satisfiability solvers depends critically on the availability of hard satisfiable instances. A plausible source of such instances consists of random k-SAT formulas whose clauses are chosen uniformly from among all clauses satisfying some randomly chosen truth assignment A. Unfortunately, instances generated in this manner tend to be relatively easy and can be solved efficiently by practical heuristics. Roughly speaking, as the formula's density increases, for a number of different algorithms, A acts as a stronger and stronger attractor. Motivated by recent results on the geometry of the space of satisfying truth assignments of random k-SAT and NAE-k-SAT formulas, we introduce a simple twist on this basic model, which appears to dramatically increase its hardness. Namely, in addition to forbidding the clauses violated by the hidden assignment A, we also…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsConstraint Satisfaction and Optimization · Logic, Reasoning, and Knowledge · Advanced Graph Theory Research
