Characterizing Tseitin-Formulas with Short Regular Resolution Refutations
From MaRDI portal
Publication:5881799
DOI10.1613/jair.1.13521zbMath1506.68062MaRDI QIDQ5881799
Stefan Mengel, Alexis de Colnet
Publication date: 13 March 2023
Published in: Journal of Artificial Intelligence Research (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1613/jair.1.13521
68R10: Graph theory (including graph drawing) in computer science
68T30: Knowledge representation
03F20: Complexity of proofs
68R07: Computational aspects of satisfiability
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- 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
- Connecting knowledge compilation classes and width parameters
- Safe separators for treewidth
- Hard examples for the bounded depth Frege proof system
- 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
- Graph Expansion, Tseitin Formulas and Resolution Proofs for CSP
- Cops-Robber Games and the Resolution of Tseitin Formulas
- 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
