← All papers
First page of Accumulating Pruning Constraints: New Exact Polynomial-Space Algorithms for Max 2-SAT

Accumulating Pruning Constraints: New Exact Polynomial-Space Algorithms for Max 2-SAT

Konstantin Kutzkov

cs.DS Oct 29, 2026 · v1 cs.AI
A Lean 4 artifact verifies the correctness of the Max 2-SAT algorithms and their search-node bounds, with two random-matrix estimates taken as explicit hypotheses.
We present deterministic polynomial-space algorithms that solve Max 2-SAT on $n$ variables exactly in time $\Ostar(2^{(1-γ)n})$, for a fixed $γ>0$, on several classes of instances whose clause density may grow with $n$. Our main tool extends the classic DPLL branching algorithm. When the search gives a variable its less promising value, comparing the two values of the variable yields a pruning constraint that is satisfied by some optimal assignment. Accumulating these constraints along each branch prunes all but an exponentially small fraction of the assignments. The classes are formulas with many biased variables, semirandom 2-CNF formulas, and Max-Cut on regular expander graphs and on graphs generated by a stochastic block model. In a semirandom formula, the pairs of variables that may share a clause are arbitrary, and the clauses on these pairs are random. For semirandom formulas and block-model graphs, the algorithms are still exact on every input, and the time bound holds with high probability over the input. To our knowledge, these are the first polynomial-space algorithms with such a running time for nontrivial classes of dense Max 2-SAT instances. Beyond these classes, the pruning constraints can be added to any branching algorithm for Max 2-SAT, and we expect them to be of practical relevance for general formulas, in particular for sparse ones, where each constraint involves only a few variables.

No known polynomial-space algorithm solves Max 2-SAT exactly in time O*(2^{(1-γ)n}) on all instances. Known improvements over 2^n require exponential space or apply only to sparse formulas.

DPLL branching is extended with pruning constraints. When a variable is given its less promising value, comparing its two values yields a constraint satisfied by some optimal assignment. These constraints accumulate along each branch and prune all but an exponentially small fraction of assignments. The method is analyzed on formulas with many biased variables, semirandom 2-CNF formulas, Max-Cut on regular expanders, and Max-Cut on stochastic block model graphs. A Lean 4 artifact formalizes correctness and the search-node bounds.

The algorithms run in deterministic polynomial space and time O*(2^{(1-γ)n}) on these dense instance classes, with high probability for the random classes, and are exact on every input. Lean checks optimality for all four classes and the main node-count theorems; arithmetic and space bounds and one spectral-gap corollary are not formalized.

InstancesDensityTime bound holdsResult
Many biased variablesanyfor every instanceThm. 3.2, Cor. 3.5
Semirandom 2-CNFanyin expectation and w.h.p.Thm. 4.2
Max-Cut, regular expandersd ≤ (1-ε)nfor every instanceCor. 5.3
Max-Cut, block modelnπ_ab(1-π_ab) ≥ C log nw.h.p. over the graphThm. 6.2
Instance classes and results