Characterizing Tseitin-formulas with short regular resolution refutations
From MaRDI portal
Publication:2118291
DOI10.1007/978-3-030-80223-3_9OpenAlexW3184595420MaRDI QIDQ2118291
Alexis de Colnet, Stefan Mengel
Publication date: 22 March 2022
Full work available at URL: https://arxiv.org/abs/2103.09609
Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Computational aspects of satisfiability (68R07)
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On the read-once property of branching programs and CNFs of bounded treewidth
- Satisfiability, branch-width and Tseitin tautologies
- Safe separators for treewidth
- Hard examples for the bounded depth Frege proof system
- Cops-robber games and the resolution of Tseitin formulas
- Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs
- Simplified and improved separations between regular and general resolution by lifting
- Parameters Tied to Treewidth
- A Near-Optimal Separation of Regular and General Resolution
- Regular Resolution Versus Unrestricted Resolution
- Hard examples for resolution
- Search Problems in the Decision Tree Model
- Graph Expansion, Tseitin Formulas and Resolution Proofs for CSP
- Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs
- Satisfiable Tseitin Formulas Are Hard for Nondeterministic Read-Once Branching Programs.
- Clique is hard on average for regular resolution
- Time-space tradeoffs in resolution
- Decomposable negation normal form
- Strong ETH holds for regular resolution
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
This page was built for publication: Characterizing Tseitin-formulas with short regular resolution refutations
