Satisfiability, branch-width and Tseitin tautologies
From MaRDI portal
Publication:430830
DOI10.1007/s00037-011-0033-1zbMath1243.68182OpenAlexW3158535383MaRDI QIDQ430830
Michael Alekhnovich, Alexander A. Razborov
Publication date: 26 June 2012
Published in: Computational Complexity (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00037-011-0033-1
Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20)
Related Items
Characterizing Tseitin-Formulas with Short Regular Resolution Refutations ⋮ On the Satisfiability of Quantum Circuits of Small Treewidth ⋮ Complexity and approximability of parameterized MAX-CSPs ⋮ On the satisfiability of quantum circuits of small treewidth ⋮ Complexity and Algorithms for Well-Structured k-SAT Instances ⋮ Tangle bases: Revisited ⋮ Special issue in memory of Misha Alekhnovich. Foreword ⋮ Size-treewidth tradeoffs for circuits computing the element distinctness function ⋮ On treewidth, separators and Yao's garbling ⋮ An Upper Bound for Resolution Size: Characterization of Tractable SAT Instances ⋮ Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs ⋮ Counting truth assignments of formulas of bounded tree-width or clique-width ⋮ Computing branchwidth via efficient triangulations and blocks ⋮ Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable ⋮ On tseitin formulas, read-once branching programs and treewidth ⋮ Time-Space Trade-offs in Resolution: Superpolynomial Lower Bounds for Superlinear Space ⋮ A SAT Approach to Branchwidth ⋮ Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution ⋮ Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs ⋮ Bounded-depth Frege complexity of Tseitin formulas for all graphs ⋮ Expansion-based QBF solving versus Q-resolution ⋮ Reflections on Proof Complexity and Counting Principles ⋮ Backdoors to q-Horn ⋮ Characterizing Tseitin-formulas with short regular resolution refutations ⋮ On the hierarchical community structure of practical Boolean formulas
Cites Work
- The monotone circuit complexity of Boolean functions
- Graph minors. X: Obstructions to tree-decomposition
- On the automatizability of resolution and related propositional proof systems
- Mutilated chessboard problem is exponentially hard for resolution
- Graph minors. XIII: The disjoint paths problem
- An exponential separation between the parity principle and the pigeonhole principle
- Intersection Theorems for Systems of Sets
- Resolution Is Not Automatizable Unless W[P Is Tractable]
- A Separator Theorem for Planar Graphs
- Applications of a Planar Separator Theorem
- Short proofs are narrow—resolution made simple
- On Interpolation and Automatization for Frege Systems
- Pseudorandom Generators in Propositional Proof Complexity
- On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
