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

Konstantin Kutzkov

cs.DSOct 29, 2026

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

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.

Figures & tables

Instances	Density	Time bound holds	Result
Many biased variables	any	for every instance	Thm. 3.2 , Cor. 3.5
Semirandom 2-CNF	any	in expectation and w.h.p.	Thm. 4.2
Max-Cut, regular expanders	$d\leq(1-\varepsilon)n$	for every instance	Cor. 5.3
Max-Cut, block model	$n\pi_{ab}(1-\pi_{ab})\geq C\log n$	w.h.p. over the graph	Thm. 6.2

Table 1: The four classes on which our algorithms run in polynomial space and time

O^{*}(2^{(1-\gamma)n})

Panel of Figure 1 — Figure 1: Branching on a vertex $v$ of degree $7$ in Max-Cut. The neighbors $a,b,c$ of $v$ are already placed, and $u_{1},\ldots,u_{4}$ are not. Thick edges are cut, dashed edges are not, and dotted edges are still open. (a) On side 1, $v$ cuts two of its three placed edges. This is its preferred side, and the branch keeps all placements of $u_{1},\ldots,u_{4}$ . (b) Placing $v$ on side 0 pays off only if at least four of its seven neighbors end on side 1. Otherwise, moving $v$ to side 1 cuts more edges, and that cut is examined in branch (a). Since $a$ and $b$ are on side 0, at most one of $u_{1},\ldots,u_{4}$ may join them there, and only $5$ of the $16$ placements of $u_{1},\ldots,u_{4}$ remain.

Maximum Satisfiability

Maximum Satisfiability (MaxSAT) finds truth assignments that satisfy as many, or as much-weighted, Boolean clauses as possible.

See all 11 papers

Jul 26, 2026

Maximum Satisfiability of Simple Temporal Problems

The Simple Temporal Problem (STP) is a core framework for quantitative temporal constraints. As STP data can be inconsistent, we study MAXSTP: compute a maximum-cardinality consistent subset of constraints. This extension is NP-hard, and we analyze its parameterized complexity under measures that capture practically relevant instance features: the number of variables

n

(instance scale), the maximum coefficient magnitude

k

(numeric range), and structural parameters of the constraint graph such as treewidth

tw

(decomposability) and vertex cover size

vc

(density). We show that MAXSTP is W[1]-hard parameterized by

n

, implying that

n

and parameters that depend on

n

(including

tw

and

vc

) are insufficient for fixed-parameter tractability. For combined parameters, we give an

O^*(k^n)

-time algorithm, yielding single-exponential solvability for fixed

k

. While

k+tw

remains W[1]-hard, MAXSTP is in XP via an

O^*((n\cdot k)^{tw})

algorithm. Our results suggest that MAXSTP is often computationally harder than optimizing qualitative CSPs. We verify that many such problems (including RCC-8 and Allen's algebra) are FPT when parameterized by

n

tw

. However, we also demonstrate that FPT algorithms for MAXSTP are indeed possible but with other parameters such as

k + vc

Johannes K. Fichte, Johanna Groven, Peter Jonsson +2

Department of Computer and Information Science (IDA) Linköping University

Temporal Reasoning Parameterized Complexity Constraint Satisfaction Maximum Satisfiability

Ask PDF

May 8, 2026

Solving Max-Cut to Global Optimality via Feasibility-Preserving Graph Neural Networks

Exact solution of hard combinatorial optimization problems often relies on strong convex relaxations, but solving these relaxations repeatedly inside a branch-and-bound algorithm can be prohibitively expensive. Hence, we consider this challenge for Max-Cut, where branch and bound commonly uses semidefinite programming (SDP) relaxations to bound subproblems. We propose a Max-Cut-specific graph neural network that serves as a principled, lightweight neural proxy for these SDP solvers and can be plugged directly into an exact branch-and-bound framework. The proposed architecture has update steps of complexity

\mathcal{O}(n^2 + ne)

, and predicts both primal- and dual-feasible SDP solutions. The primal SDP solutions yield feasible Max-Cut solutions via the Goemans--Williamson algorithm. In addition, it is trained in a self-supervised fashion without requiring solved SDP relaxations as labels. Empirically, we show that our architecture can substantially reduce the cost of bounding in exact Max-Cut solving by up to

10.6 \times

compared with using the state-of-the-art SDP solver Mosek. Our work highlights the potential of learned, validity-preserving surrogates for accelerating exact optimization over structured convex relaxations.

Hao Chen, Chendi Qian, Christopher Morris +2

1Davidson School of Chemical Engineering, Purdue University · Faculty of Computer Science, RWTH Aachen University · 3Jacobs Technion-Cornell Institute, Cornell Tech

Max-Cut Semidefinite Programming Graph Neural Networks Branch and Bound Combinatorial Optimization Global Optimization+2

Ask PDF

Jun 23, 2026

Cost-Optimal Decision Diagrams for Stochastic Boolean Function Evaluation

In many decision-making scenarios, acquiring information incurs different costs. We consider the problem of constructing a deterministic evaluation strategy that minimizes the expected cost of evaluating a propositional formula under variable costs and a probability distribution over truth assignments. We present a branch-and-bound algorithm with variable-selection heuristics, pruning, and caching. To the best of our knowledge, it is the first practical exact algorithm for this level of generality. Experiments on random instances demonstrate scalability and quantify the efficiency-quality trade-off of a greedy beam-search variant. We additionally evaluate a structured heart-disease diagnosis instance. Finally, we prove that the problem is

\#P

-hard and contained in

\mathrm{PSPACE}

Xia Zong, Tuomo Lehtonen, Jussi Rintanen

Department of Computer Science, Aalto University

Branch and Bound Cost-Aware Inference Combinatorial Optimization

Ask PDF

Abstract

Maximum Satisfiability

Explore similar work

Maximum Satisfiability of Simple Temporal Problems

Solving Max-Cut to Global Optimality via Feasibility-Preserving Graph Neural Networks

Cost-Optimal Decision Diagrams for Stochastic Boolean Function Evaluation