Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

An Exponential Separation between Deterministic CDCL and DPLL Solvers

Sahil Samar, Marc Vinyals, Vijay Ganesh

Abstract

We prove that there exists a deterministic configuration of Conflict Driven Clause Learning (CDCL) SAT solvers using a variant of the VSIDS branching heuristic that solves instances of the Ordering Principle (OP) CNF formulas in time polynomial in n, where n is the number of variables in such formulas. Since tree-like resolution is known to have an exponential lower bound for proof size for OP formulas, it follows that CDCL under this configuration has an exponential separation with any solver that is polynomially equivalent to tree-like resolution and therefore any configuration of DPLL SAT solvers.

An Exponential Separation between Deterministic CDCL and DPLL Solvers

Abstract

We prove that there exists a deterministic configuration of Conflict Driven Clause Learning (CDCL) SAT solvers using a variant of the VSIDS branching heuristic that solves instances of the Ordering Principle (OP) CNF formulas in time polynomial in n, where n is the number of variables in such formulas. Since tree-like resolution is known to have an exponential lower bound for proof size for OP formulas, it follows that CDCL under this configuration has an exponential separation with any solver that is polynomially equivalent to tree-like resolution and therefore any configuration of DPLL SAT solvers.
Paper Structure (15 sections, 4 theorems, 5 equations, 1 figure)

This paper contains 15 sections, 4 theorems, 5 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Ordering Principle
  4. VSIDS
  5. CDCL Configuration
  6. Main Result
  7. Conclusions
  8. Appendix
  9. First Head Clause Completeness
  10. Second Head Clause Completeness
  11. First Descending Cascade Clause Completeness
  12. Cascade Lemma Completeness
  13. Descending Lemma Completeness
  14. Pivot Lemma Completeness
  15. Tail Lemma Completeness

Key Result

Lemma 1

Assume that the solver has learned at least one clause. Consider the set $S$ of variables in the most recent learned clause. During a run, when the solver has to branch, it must branch on an unassigned variable in $S$ and assign it to false, before it can branch on any other variables.

Figures (1)

  • Figure 10: Descending Lemma Implication Graph

Theorems & Definitions (7)

  • Lemma 1: Focus Lemma
  • Definition 2: Ordered Literal Sequence
  • Definition 3: Prefix Clause
  • Theorem 4
  • Theorem 10
  • Corollary 11
  • Definition 12: Completeness