Automated Reencoding Meets Graph Theory

TL;DR

This paper characterizes the capabilities and limitations of Bounded Variable Addition (BVA) in reencoding 2-CNF formulas, providing theoretical bounds and a more efficient implementation based on graph theory insights.

Contribution

It offers a graph-theoretic characterization of BVA, establishes new bounds on reencoding efficiency, and improves BVA implementation for random formulas.

Findings

Idealized BVA can reencode any 2-CNF with about 0.396 times n^2/ log n clauses.

Without preprocessing, the constant factor increases to 1, and cannot go below 0.25.

BVA cannot produce the product encoding for at-most-one constraints, which uses 2n+o(n) clauses.

Abstract

Bounded Variable Addition (BVA) is a central preprocessing method in modern state-of-the-art SAT solvers. We provide a graph-theoretic characterization of which 2-CNF encodings can be constructed by an idealized BVA algorithm. Based on this insight, we prove new results about the behavior and limitations of BVA and its interaction with other preprocessing techniques. We show that idealized BVA, plus some minor additional preprocessing (e.g., equivalent literal substitution), can reencode any 2-CNF formula with $n$ variables into an equivalent 2-CNF formula with $(\tfrac{\lg(3)}{4}+o(1))\,\tfrac{n^2}{\lg n}$ clauses. Furthermore, we show that without the additional preprocessing the constant factor worsens from $\tfrac{\lg(3)}{4} \approx 0.396$ to $1$, and that no reencoding method can achieve a constant below $0.25$. On the other hand, for the at-most-one constraint on $n$ variables, we prove that idealized BVA cannot reencode this constraint using fewer than $3n-6$ clauses, a bound that we prove is achieved by actual implementations. In particular, this shows that the product encoding for at-most-one, which uses $2n+o(n)$ clauses, cannot be constructed by BVA regardless of the heuristics used. Finally, our graph-theoretic characterization of BVA allows us to leverage recent work in algorithmic graph theory to develop a drastically more efficient implementation of BVA that achieves a comparable clause reduction on random monotone 2-CNF formulas.