Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Automated Reencoding Meets Graph Theory

Benjamin Przybocki, Bernardo Subercaseaux, Marijn J. H. Heule

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.

Automated Reencoding Meets Graph Theory

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 variables into an equivalent 2-CNF formula with clauses. Furthermore, we show that without the additional preprocessing the constant factor worsens from to , and that no reencoding method can achieve a constant below . On the other hand, for the at-most-one constraint on variables, we prove that idealized BVA cannot reencode this constraint using fewer than 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 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.

Paper Structure

This paper contains 17 sections, 39 theorems, 34 equations, 7 figures, 4 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Notation and Terminology
  4. CNF Encodings and BVA
  5. BVA in Terms of Strict Polarized Rectifier Networks
  6. Encodings for General 2-CNF Formulas
  7. Upper Bound for BVA With Simplification
  8. Lower Bound for BVA With Simplification
  9. Monotone Formulas
  10. Encodings for AtMostOne
  11. Discussion and Experimental Results
  12. Future directions.
  13. Proofs from \ref{['sec-bva-characterization']}
  14. Proofs from \ref{['sec-2cnf-general']}
  15. Proofs from \ref{['sec-amo']}
  16. ...and 2 more sections

Key Result

Theorem 1

Idealized BVA can reencode every 2-CNF formula with $n$ variables to one with at most $(1+o(1)) \frac{n^2}{\lg n}$ clauses.

Figures (7)

  • Figure 1: Illustration of \ref{['example:BVA-1']}
  • Figure 2: Illustration of a diagram and a polarized diagram for a simple 2-CNF. Edges with positive polarity (i.e., $p(u, v) = +$) are colored green, whereas negative polarity edges are colored red.
  • Figure 3: Illustration of the BVA steps in \ref{['ex-bva']}
  • Figure 4: SPRN realizing $K_n$ with $3n-6$ edges
  • Figure 5: Illustration for the proof of \ref{['thm:amo-formal']}
  • ...and 2 more figures

Theorems & Definitions (84)

  • Theorem 1: Informal
  • Theorem 2: Informal
  • Theorem 3: Informal
  • Theorem 4: Informal
  • Definition 1
  • Example 1
  • Definition 2: BVA Step
  • Lemma 1: mantheyAutomatedReencodingBoolean2012
  • Definition 3: Simple 2-CNF
  • Proposition 1
  • ...and 74 more