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

Introduction

Max 2-SAT is a classic problem in theoretical computer science: given a 2-CNF formula, find an assignment that satisfies the maximum number of clauses simultaneously. It has wide applications in circuit design, machine learning, and other fields. However, exactly solving Max 2-SAT typically requires exponential time and often consumes large amounts of memory. Recently, a paper titled "Accumulating Pruning Constraints: New Exact Polynomial-Space Algorithms for Max 2-SAT" proposed a class of deterministic polynomial-space algorithms that achieve strict exponential speedups on several classes of instances.

The core idea of the algorithm is to reduce the search space by accumulating pruning constraints on top of the classic DPLL branching algorithm. Specifically, when the search assigns a variable its "less promising" value, comparing the two values of that variable yields a pruning constraint, and some optimal assignment must satisfy this constraint. By accumulating these constraints along each branch, all but an exponentially small fraction of assignments can be pruned.

Algorithm Mechanism: From DPLL to Accumulating Pruning

The classic DPLL algorithm solves SAT problems through branching and propagation. For Max 2-SAT, a natural extension is to try both values when branching and solve recursively. But this produces a full binary search tree, requiring in the worst case examination of 2^n assignments.

The key improvement of the new algorithm is: when a branch chooses a "worse" value, the algorithm does not immediately abandon that branch but records a constraint—this constraint is generated by comparing the two values and guarantees that at least one optimal assignment satisfies it. As the search deepens, these constraints are accumulated and used for subsequent pruning.

The authors prove that for certain classes of instances, the number of accumulated constraints is large enough that only an exponentially small fraction of assignments need to be considered on each branch. Therefore, the total running time is reduced to O*(2^{(1-γ)n}), where γ>0 is a fixed constant. Since the algorithm uses only polynomial space, it avoids the need to store large amounts of intermediate results and is better suited to memory-constrained environments.

The DPLL (Davis-Putnam-Logemann-Loveland) algorithm is a classic backtracking algorithm for solving SAT problems, whose core operations are branching and unit propagation. During branching, the algorithm selects an unassigned variable, tries assigning it true or false, and solves recursively. Unit propagation forces a literal to be true to simplify the formula when some clause has only one unassigned literal left. For Max 2-SAT, the DPLL extension typically explores both values when branching and records the number of currently satisfied clauses, ultimately returning the optimal solution. However, this naive extension traverses the full binary search tree and in the worst case must examine 2^n assignments, so its time complexity is exponential. The new algorithm introduces the accumulation of pruning constraints into the DPLL framework; these constraints arise from comparing the two values during branching and guarantee that at least one optimal assignment satisfies them, thereby pruning during the search a large number of branches that cannot contain an optimal solution.

Applicable Instance Classes

The paper proves speedups primarily for three classes of instances:

1. Formulas with Many Biased Variables

In such formulas, many variables frequently appear with the same polarity in clauses (i.e., they are biased). By comparing the two values of these variables, the algorithm can generate strong pruning constraints, thereby rapidly shrinking the search space.

2. Semi-Random 2-CNF Formulas

In semi-random formulas, the relationship of clause sharing between pairs of variables may be arbitrary, but the clauses themselves are randomly generated. This model is closer to practical applications than purely random formulas, because the structure of real problems is often not completely random. For such formulas, the algorithm remains exact, and the time complexity holds with high probability.

Semi-random 2-CNF formulas are an important model in SAT theory, situated between purely random formulas and fully structured formulas. In purely random 2-CNF formulas, each clause is chosen uniformly at random from all possible pairs of literals; the semi-random model allows the relationship of clause sharing between pairs of variables to be arbitrary (i.e., the underlying graph structure of clauses can be non-random), but the clauses themselves are still randomly generated. This model is closer to practical applications, because real problems often have non-random structure (such as community structure, geographic constraints, etc.), but local interactions may exhibit randomness. For semi-random formulas, the time complexity analysis of the algorithm usually needs to hold with high probability, because randomness affects the generation and accumulation of pruning constraints. The paper proves that for such formulas, the new algorithm remains exact and completes in O*(2^{(1-γ)n}) time with high probability, which provides theoretical guarantees for handling Max 2-SAT instances with practical backgrounds.

3. Max-Cut on Regular Expander Graphs and Stochastic Block Model Graphs

Max 2-SAT is closely related to Max-Cut. The paper applies the algorithm to the Max-Cut problem on regular expander graphs and graphs generated by the stochastic block model, again obtaining exponential speedups. These graph classes are common in both theoretical analysis and practical network models.

Interestingly, for semi-random formulas and block model graphs, the algorithm is exact on every input, while the time bound holds with high probability over the input. To the authors' knowledge, this is the first polynomial-space algorithm for a nontrivial dense class of Max 2-SAT instances with such a running time.

Regular expander graphs are a class of sparse graphs with strong connectivity properties, in which every vertex has the same degree and the graph has good edge expansion (i.e., the neighborhood of any small set is large). The stochastic block model (SBM) is a model for generating random graphs with community structure, in which vertices are partitioned into several communities and edges within and between communities are randomly generated with different probabilities. The Max-Cut problem is to find a partition of the vertices in a graph that maximizes the number of edges crossing the two parts. Max 2-SAT is closely related to Max-Cut: each Max-Cut instance on a graph can be naturally transformed into a Max 2-SAT instance, where each edge corresponds to a clause requiring its two endpoints to belong to different parts. The paper applies the accumulating pruning constraints algorithm to the Max-Cut problem on these two graph classes and proves exponential speedups. These graph classes are common in theoretical computer science and network analysis, so the result has broad theoretical significance.

Beyond Specific Classes: Generality and Practical Significance

Although the paper mainly analyzes the above three classes of instances, the idea of pruning constraints can be added to any branching algorithm for Max 2-SAT. The authors expect that these constraints will also be practically relevant for general formulas, especially sparse formulas—in sparse formulas, each constraint involves only a few variables, so the cost of representing and checking constraints is low.

For sparse Max 2-SAT, each clause contains only two literals, and the accumulated constraints may be very localized, thereby efficiently pruning during branching the regions that cannot contain an optimal solution. This offers the possibility of integrating the technique into practical solvers.

Sparse Max 2-SAT refers to instances in which each variable appears in a small number of clauses; such instances are common in practical applications, for example, formulas arising from circuit design or constraint satisfaction problems. In sparse formulas, the accumulated pruning constraints usually involve only a few variables, so the cost of representing and checking constraints is low. Specifically, each pruning constraint can be represented as a short clause or a local restriction on variable assignments, and the algorithm can efficiently maintain these constraints during branching and quickly determine whether the current branch may contain an optimal solution. This locality makes the idea of pruning constraints particularly suitable for integration into practical Max 2-SAT solvers, especially in memory-constrained environments, because the polynomial-space requirement goes hand in hand with the local structure of sparse formulas. The authors expect that even for general formulas, these constraints may bring practical speedups, especially when the formula has some structure (such as biased variables or community structure).

Conclusion

This research provides a new theoretical tool for exactly solving Max 2-SAT. By accumulating pruning constraints, the algorithm achieves exponential speedups on several important classes of instances while maintaining polynomial space. Although the current results are mainly theoretical, its core idea—using comparison information during branching to generate constraints—is general and may inspire the design of more practical Max 2-SAT solvers. For readers interested in combinatorial optimization, SAT solving, and algorithm design, this paper is worth reading in depth.

One-line Summary

The new algorithm accumulates pruning constraints in DPLL branching to achieve exponential speedups in polynomial space for several classes of Max 2-SAT instances.

Paragraph Summary

The paper proposes a class of deterministic polynomial-space algorithms for exactly solving the Max 2-SAT problem. Building on the classic DPLL branching algorithm, the algorithm reduces the search space by accumulating pruning constraints generated during branching. When a variable is assigned its "worse" value, comparing the two values generates a constraint, and at least one optimal assignment satisfies this constraint. By accumulating these constraints along branches, all but an exponentially small fraction of assignments can be pruned, thereby achieving O*(2^{(1-γ)n}) time complexity on several classes of instances. The paper proves speedups for formulas with many biased variables, semi-random 2-CNF formulas, and Max-Cut on regular expander graphs and stochastic block model graphs. The algorithm is exact on every input for semi-random formulas and block model graphs, with the time bound holding with high probability. The idea of pruning constraints is general and can be added to any Max 2-SAT branching algorithm, with practical potential for sparse formulas.