Finding hardness reductions automatically using SAT solvers
Helena Bergold, Manfred Scheucher, Felix Schröder
TL;DR
This work tackles the completion problem for partial sign mappings, proving $NP$-hardness in a wide range of combinatorial settings via an automated, SAT-based gadget construction framework. By encoding variables as domain triples and designing Clause-Gadgets and Propagator-Gadgets, the authors assemble reductions from $3$SAT through a general Combination Lemma, enabling systematic hardness proofs across thousands of structures, including generalized signotopes and interior triple systems. They report extensive empirical results across rank $r=3$ and rank $r=4$, identifying numerous hard settings and an infinite family for even ranks, while also highlighting polynomial-time solvable instances via greedy completions. The framework blends human insight with computational search, offering a scalable approach to hardness reductions and potentially enabling automation for additional combinatorial structures and complexity classes.
Abstract
In this article, we show that the completion problem, i.e. the decision problem whether a partial structure can be completed to a full structure, is NP-complete for many combinatorial structures. While the gadgets for most reductions in literature are found by hand, we present an algorithm to construct gadgets in a fully automated way. Using our framework which is based on SAT, we present the first thorough study of the completion problem on sign mappings with forbidden substructures by classifying thousands of structures for which the completion problem is NP-complete. Our list in particular includes interior triple systems, which were introduced by Knuth towards an axiomatization of planar point configurations. Last but not least, we give an infinite family of structures generalizing interior triple system to higher dimensions for which the completion problem is NP-complete.