ABSTRACT. The effective use of satisfiability solvers requires problem encodings that make good use of the reasoning techniques employed in such solvers, such as unit propagation and clause learning. Propagation completeness has been proposed as a useful property for constraint encodings as it maximizes the utility of unit propagation. Experimental results on using encodings with this property in the context of SMT solving have however remained inconclusive, as such encodings are typically very large, which increases the bookkeeping effort of solvers.

In this paper, we introduce approximate propagation completeness and approximate conflict propagation as novel notions that balance the size of an encoding and its properties for efficient SAT-based reasoning. While approximate propagation completeness is a generalization of classical propagation completeness, (approximate) conflict propagation is a new concept for reasoning about how early conflicts can be detected by a SAT solver. Both notions together span a hierarchy of encoding quality choices, with classical propagation completeness as a special case. We show how to compute approximately propagation complete and conflict propagating constraint encodings with a minimal number of clauses using a reduction to MaxSAT. To evaluate the effect of such encodings, we give results on applying them in a case study.