Satisfiability, branch-width and Tseitin tautologies
DOI10.1007/S00037-011-0033-1zbMATH Open1243.68182OpenAlexW3158535383MaRDI QIDQ430830FDOQ430830
Authors: Michael Alekhnovich, Alexander 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
Recommendations
Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20)
Cites Work
- Graph minors. X: Obstructions to tree-decomposition
- Applications of a Planar Separator Theorem
- Graph minors. XIII: The disjoint paths problem
- Title not available (Why is that?)
- Intersection Theorems for Systems of Sets
- A Separator Theorem for Planar Graphs
- The monotone circuit complexity of Boolean functions
- Title not available (Why is that?)
- Title not available (Why is that?)
- Pseudorandom Generators in Propositional Proof Complexity
- On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic
- Short proofs are narrow—resolution made simple
- Resolution Is Not Automatizable Unless W[P] Is Tractable
- On Interpolation and Automatization for Frege Systems
- Title not available (Why is that?)
- On the automatizability of resolution and related propositional proof systems
- Mutilated chessboard problem is exponentially hard for resolution
- An exponential separation between the parity principle and the pigeonhole principle
- Solving satisfiability using decomposition and the most constrained subproblem
- Title not available (Why is that?)
- Width-parametrized SAT: time-space tradeoffs
Cited In (30)
- Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs
- Reflections on Proof Complexity and Counting Principles
- Characterizing Tseitin-formulas with short regular resolution refutations
- Backdoors to q-Horn
- Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints
- On Tseitin formulas, read-once branching programs and treewidth
- On the hierarchical community structure of practical Boolean formulas
- Complexity and approximability of parameterized MAX-CSPs
- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
- Size-treewidth tradeoffs for circuits computing the element distinctness function
- Time-space trade-offs in resolution: superpolynomial lower bounds for superlinear space
- Title not available (Why is that?)
- Special issue in memory of Misha Alekhnovich. Foreword
- Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
- A SAT approach to branchwidth
- An upper bound for resolution size: characterization of tractable SAT instances
- Computing branchwidth via efficient triangulations and blocks
- Tangle bases: Revisited
- On treewidth, separators and Yao's garbling
- Expansion-based QBF solving versus Q-resolution
- Counting truth assignments of formulas of bounded tree-width or clique-width
- Theory and Applications of Satisfiability Testing
- Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs
- Characterizing Tseitin-Formulas with Short Regular Resolution Refutations
- Logics in Artificial Intelligence
- On the satisfiability of quantum circuits of small treewidth
- On the satisfiability of quantum circuits of small treewidth
- Complexity and Algorithms for Well-Structured k-SAT Instances
- Variants and satisfiability in the infinitary unification wonderland
- Bounded-depth Frege complexity of Tseitin formulas for all graphs
This page was built for publication: Satisfiability, branch-width and Tseitin tautologies
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q430830)
