Characterizing Tseitin-Formulas with Short Regular Resolution Refutations

DOI10.1613/JAIR.1.13521MaRDI QIDQ5881799zbMATH OpenOpenAlexFDO

Authors Alexis de Colnet, Stefan Mengel

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

zbMATH Keywords

knowledge representationsatisfiability

Mathematics Subject Classification ID

Complexity of proofs (03F20) Computational aspects of satisfiability (68R07) Graph theory (including graph drawing) in computer science (68R10) Knowledge representation (68T30)

Recommendations

• Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs
• Efficient arbitrary and resolution proofs of unsatisfiability for restricted tree-width
• Bounded-depth Frege complexity of Tseitin formulas for all graphs
• On Tseitin formulas, read-once branching programs and treewidth
• scientific article; zbMATH DE number 176731

Cites work

• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• A near-optimal separation of regular and general resolution
• Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs
• Clique is hard on average for regular resolution
• Connecting knowledge compilation classes and width parameters
• Cops-robber games and the resolution of Tseitin formulas
• Decomposable negation normal form
• Graph expansion, Tseitin formulas and resolution proofs for CSP
• Handbook of satisfiability. In 2 parts
• Hard examples for resolution
• Hard examples for the bounded depth Frege proof system
• scientific article; zbMATH DE number 5899257 (Why is no real title available?)
• scientific article; zbMATH DE number 1946853 (Why is no real title available?)
• scientific article; zbMATH DE number 4121438 (Why is no real title available?)
• scientific article; zbMATH DE number 819737 (Why is no real title available?)
• scientific article; zbMATH DE number 3325539 (Why is no real title available?)
• Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs
• On the read-once property of branching programs and CNFs of bounded treewidth
• Parameters tied to treewidth
• Regular Resolution Versus Unrestricted Resolution
• Safe separators for treewidth
• Satisfiability, branch-width and Tseitin tautologies
• Satisfiable Tseitin formulas are hard for nondeterministic read-once branching programs
• Simplified and improved separations between regular and general resolution by lifting
• Strong ETH holds for regular resolution
• Time-space tradeoffs in resolution, superpolynomial lower bounds for superlinear space

Cited in

(9)

• Tseitin's formulas revisited
• Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs
• Bounded-depth Frege complexity of Tseitin formulas for all graphs
• Characterizing Tseitin-formulas with short regular resolution refutations
• scientific article; zbMATH DE number 176731 (Why is no real title available?)
• 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
• Separation between Walksat and DPLL

This page was built for publication: Characterizing Tseitin-Formulas with Short Regular Resolution Refutations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5881799)