SAT backdoors: depth beats size
From MaRDI portal
Publication:6152185
Abstract: For several decades, much effort has been put into identifying classes of CNF formulas whose satisfiability can be decided in polynomial time. Classic results are the linear-time tractability of Horn formulas (Aspvall, Plass, and Tarjan, 1979) and Krom (i.e., 2CNF) formulas (Dowling and Gallier, 1984). Backdoors, introduced by Williams Gomes and Selman (2003), gradually extend such a tractable class to all formulas of bounded distance to the class. Backdoor size provides a natural but rather crude distance measure between a formula and a tractable class. Backdoor depth, introduced by M"{a}hlmann, Siebertz, and Vigny (2021), is a more refined distance measure, which admits the utilization of different backdoor variables in parallel. Bounded backdoor size implies bounded backdoor depth, but there are formulas of constant backdoor depth and arbitrarily large backdoor size. We propose FPT approximation algorithms to compute backdoor depth into the classes Horn and Krom. This leads to a linear-time algorithm for deciding the satisfiability of formulas of bounded backdoor depth into these classes. We base our FPT approximation algorithm on a sophisticated notion of obstructions, extending M"{a}hlmann et al.'s obstruction trees in various ways, including the addition of separator obstructions. We develop the algorithm through a new game-theoretic framework that simplifies the reasoning about backdoors. Finally, we show that bounded backdoor depth captures tractable classes of CNF formulas not captured by any known method.
Cites work
- A linear-time algorithm for testing the truth of certain quantified Boolean formulas
- Algorithms for propositional model counting
- Backdoor treewidth for SAT
- Backdoors into heterogeneous classes of SAT and CSP
- Backdoors to q-Horn
- Combining treewidth and backdoors for CSP
- Constraint satisfaction with bounded treewidth revisited
- Discovering archipelagos of tractability for constraint satisfaction and counting
- Graph isomorphism parameterized by elimination distance to bounded degree
- Handbook of knowledge representation.
- scientific article; zbMATH DE number 7595810 (Why is no real title available?)
- Linear-time algorithms for testing the satisfiability of propositional horn formulae
- Linear-Time Parameterized Algorithms via Skew-Symmetric Multicuts
- On the Unreasonable Effectiveness of SAT Solvers
- Polynomial-time inference of all valid implications for Horn and related formulae
- Recognition of q-Horn formulae in linear time
- Sparsity. Graphs, structures, and algorithms
- The complexity of satisfiability problems
- The complexity of theorem-proving procedures
- Theory and Applications of Satisfiability Testing
- Tree-depth, subgraph coloring and homomorphism bounds
Cited in
(3)
This page was built for publication: SAT backdoors: depth beats size
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6152185)
