Exact efficient algorithms for max 2-sat on dense and structured formulas
Accumulating Pruning Constraints: New Exact Polynomial-Space Algorithms for Max 2-SAT
Data Structures and AlgorithmsArtificial Intelligence
Summary
Max 2-SAT is a problem where you try to make the most true statements out of many pairs of variables, which is usually very slow to solve exactly. The authors found a way to speed this up for some special types of problems, even when there are many pairs to consider. They do this by cleverly throwing away many impossible options while searching for the best solution, using what they call pruning constraints. This method works well on certain structured problems and random-looking formulas, and it might help solve similar problems faster in practice.
What this means in practice
- •For optimization software developers: Create faster exact Max 2-SAT solvers for dense and structured input formulas using pruning constraints that reduce search space efficiently.
- •For graph algorithm engineers: Improve exact Max-Cut computations on regular expander and stochastic block model graphs by integrating new pruning constraints into branching algorithms.
Authors
Konstantin Kutzkov
Abstract
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.