Computing Short SAT Implicants via Ising/QUBO Encodings
This work provides a novel method for computing short implicants in SAT using Ising/QUBO models, which is important for reasoning tasks requiring partial assignments, but the results are demonstrated only on random benchmarks and may be incremental relative to existing SAT-to-Ising approaches.
The paper introduces an Ising/QUBO framework with don't-care semantics to compute short implicants for SAT problems, achieving about one-third of variables unassigned on random 3-SAT formulas while preserving satisfiability, and showing that consecutive polarity-freezing rounds achieve minimality with high probability.
Many reasoning tasks require short partial satisfying assignments (implicants), sometimes focusing on a set of important variables. SAT-to-Ising-QUBO formulations are implicitly designed so that ground states correspond to total assignments, since the Ising/QUBO model assigns a value to every spin and has no native representation of unassigned variables. We introduce an Ising/QUBO framework that incorporates "don't-care" semantics into the quadratic model via a dual-polarity representation, enabling the retrieval of short implicants. The encoding supports implicant shrinking and projection through minor objective modifications. We provide parameter regimes under which ground states correspond to short partial satisfying assignments, achieving minimality and, when the quadratic penalty function permits, minimum-cardinality. We empirically evaluate the encoding with simulated annealing on random 3-SAT enumeration benchmarks and non-CNF formulas, showing that it leaves about one-third of variables unassigned on random 3-SAT formulas while preserving satisfiability, and that consecutive polarity-freezing rounds achieve minimality (and minimum-cardinality) with high probability.