Characterizing Tseitin-formulas with short regular resolution refutations

DOI10.1007/978-3-030-80223-3_9MaRDI QIDQ2118291zbMATH OpenOpenAlexFDO

Authors Alexis de Colnet, Stefan Mengel

Publication date 22 March 2022

Full work available at URL https://arxiv.org/abs/2103.09609

zbMATH Keywords

DNNFproof complexityregular resolutiontreewidth

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational aspects of satisfiability (68R07) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Characterizing Tseitin-Formulas with Short Regular Resolution Refutations
• Parameterized and Exact Computation
• On finding short resolution refutations and small unsatisfiable subsets
• Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs
• Decomposition of tautologies into regular formulas and strong completeness of connection-graph resolution
• Satisfiability, branch-width and Tseitin tautologies
• A Resolution Calculus for Shortening Proofs
• Lower Bounds of Static Lovász-Schrijver Calculus Proofs for Tseitin Tautologies
• scientific article; zbMATH DE number 5161489
• \(T\)-resolution: Refinements and model elimination

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
• Cops-robber games and the resolution of Tseitin formulas
• Decomposable negation normal form
• Graph expansion, Tseitin formulas and resolution proofs for CSP
• 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 3313427 (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
• Search Problems in the Decision Tree Model
• 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

(2)

• 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

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 Q2118291)