arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · cs/0209032

Complexity Results on DPLL and Resolution

Paolo Liberatore
View original source ↗Read source document ↗Export metadata ↓

Abstract

DPLL and resolution are two popular methods for solving the problem of propositional satisfiability. Rather than algorithms, they are families of algorithms, as their behavior depend on some choices they face during execution: DPLL depends on the choice of the literal to branch on; resolution depends on the choice of the pair of clauses to resolve at each step. The complexity of making the optimal choice is analyzed in this paper. Extending previous results, we prove that choosing the optimal literal to branch on in DPLL is Delta[log]^2-hard, and becomes NP^PP-hard if branching is only allowed on a subset of variables. Optimal choice in regular resolution is both NP-hard and CoNP-hard. The problem of determining the size of the optimal proofs is also analyzed: it is CoNP-hard for DPLL, and Delta[log]^2-hard if a conjecture we make is true. This problem is CoNP-hard for regular resolution.

Explore related subjects

cs.LOcs.CC

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Paolo Liberatore. 2004-03-31. Complexity Results on DPLL and Resolution. https://doi.org/10.1145/1119439.1119442

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Terminal Coalgebras in Countably Many Steps

We present a collection of results that imply that an endofunctor on a category has a terminal coalgebra obtainable as a countable limit of its terminal-coalgebra chain. This holds for finitary endofunctors on locally finitely presentable categories under conditions on both the functor and the category. We adapt finiteness arguments that were originally advanced by Worrell concerning terminal coalgebras for finitary set functors. Examples include the categories of sets, posets, vector spaces, graphs, nominal sets, and presheaves on finite sets. Worrell also described, without proof, the terminal-coalgebra chain of the finite power-set functor. We provide a detailed proof following his ideas. We then turn to polynomial endofunctors on the categories of Hausdorff topological spaces and metric spaces. The Vietoris space of compact subsets yields an endofunctor $\mathscr{V}$ on the category of Hausdorff spaces. Vietoris polynomial endofunctors are built from $ \mathscr{V}$, the identity and constant functors by forming products, coproducts and compositions. Their terminal coalgebras are obtained in $ω$ steps. We then turn to the class of Hausdorff polynomial functors on the category of metric spaces, which is analogous but uses in lieu of $\mathscr{V}$ the Hausdorff functor $\mathcal{H}$. We prove they have terminal coalgebras obtained in $ω+ ω$ steps. Finally, we show that every finitary endofunctor on the category of vector spaces over a fixed field again has a terminal coalgebra obtained in $ω+ω$ steps.

cs.LO↗
arXiv2026

Tactix: Towards a Programmable Strategy Interface for Flexible SAT Solving

Modern SAT solvers combine a rich repertoire of proof rules with sophisticated strategies that determine when and how to apply them. Often, the internal implementations are tightly coupled to particular strategies, making it inconvenient to define new strategies without changing solver internals. We present Tactix, a proof-producing sequential CDCL solver that incorporates a wide range of techniques in state-of-the-art solvers with a clean separation of proof rules from solving strategies. This separation enables a public interface through which users can invoke particular techniques, observe their effects, and program a wide range of solving strategies. The default strategy of Tactix is programmable over this interface and outperforms state-of-the-art solvers on benchmarks from the 2024--2026 SAT Competitions. We also use the interface to develop novel strategies tailored to challenging benchmarks from two application domains, which led to performance gains over strong baselines. We intend Tactix to serve as an infrastructure for designing and evaluating novel solving strategies. Finally, we also present a self-study of the AI-assisted development process behind Tactix.

cs.LO↗
arXiv2026

The Lattice of Coalition Logics between MCL and CL: Coatoms and Compact Meets

For a fixed finite set $N$ of at least two agents, we investigate the lattice $L_N$ of coalition logics between minimal coalition logic (MCL) and classical coalition logic (CL), with extensions required to be structural. This lattice is order-dual to an interval in the subvariety lattice of Boolean coalition algebras. The eight basic extensions obtained by imposing seriality, independence of agents, and determinism form a Boolean cube under inclusion, but not a sublattice of $L_N$. Our main results concern coatoms and compact meets. First, finite critical coalition algebras, realized as complex algebras of finite general concurrent games, yield three infinite families of pairwise distinct coatoms containing seriality, distinguished by failures of independence, determinism, or both. An explicit splitting characterizes the unique coatom omitting seriality. Second, the meet of two basic extensions is compact if and only if the extensions are comparable. For incomparable pairs, no axiomatization of the meet can use formulas of uniformly bounded modal depth, even with infinitely many axioms. Consequently, $L_N$ and three natural principal intervals are non-coherent algebraic lattices. These results reveal lattice-theoretic phenomena beyond the inclusion order of the eight basic extensions.

cs.LO↗