Computing Short SAT Implicants via Ising/QUBO Encodings

TL;DR

This paper introduces a novel Ising/QUBO encoding that captures 'don't-care' variables, enabling extraction of short partial solutions for SAT problems, and demonstrates its effectiveness through empirical evaluation.

Contribution

It presents a new dual-polarity Ising/QUBO formulation that supports short implicant retrieval and partial assignment, improving upon traditional total assignment encodings.

Findings

Leaves about one-third of variables unassigned on random 3-SAT formulas

Supports implicant shrinking and projection through minor modifications

Achieves minimality and minimum-cardinality with high probability

Abstract

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.