Characterizing Tseitin-formulas with short regular resolution refutations
type: Item
instance of: scholarly article
title: Characterizing Tseitin-formulas with short regular resolution refutations
DOI: 10.1007/978-3-030-80223-3_9
author: Alexis de Colnet
author: Stefan Mengel
publication date: 2022-03-22T00:00:00Z
full work available at URL: https://arxiv.org/abs/2103.09609
Mathematics Subject Classification ID: 68Q25
Mathematics Subject Classification ID: 68R07
Mathematics Subject Classification ID: 68T20
zbMATH DE Number: 7495569
zbMATH Keywords: proof complexity
zbMATH Keywords: regular resolution
zbMATH Keywords: DNNF
zbMATH Keywords: treewidth
MaRDI profile type: Publication
OpenAlex ID: W3184595420
cites work: Q3002781
cites work: Satisfiability, branch-width and Tseitin tautologies
cites work: Clique is hard on average for regular resolution
cites work: Time-space tradeoffs in resolution
cites work: Strong ETH holds for regular resolution
cites work: Hard examples for the bounded depth Frege proof system
cites work: Safe separators for treewidth
cites work: Decomposable negation normal form
cites work: Q4411139
cites work: A machine program for theorem-proving
cites work: A Computing Procedure for Quantification Theory
cites work: Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs
cites work: Cops-robber games and the resolution of Tseitin formulas
cites work: Satisfiable Tseitin Formulas Are Hard for Nondeterministic Read-Once Branching Programs.
cites work: Regular Resolution Versus Unrestricted Resolution
cites work: Parameters Tied to Treewidth
cites work: Graph Expansion, Tseitin Formulas and Resolution Proofs for CSP
cites work: Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs
cites work: Search Problems in the Decision Tree Model
cites work: On the read-once property of branching programs and CNFs of bounded treewidth
cites work: Q5593816
cites work: Hard examples for resolution
cites work: A Near-Optimal Separation of Regular and General Resolution
cites work: Simplified and improved separations between regular and general resolution by lifting
Recommended article: Characterizing Tseitin-Formulas with Short Regular Resolution Refutations
Recommended article: Parameterized and Exact Computation
Recommended article: On finding short resolution refutations and small unsatisfiable subsets
Recommended article: Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs
Recommended article: Decomposition of tautologies into regular formulas and strong completeness of connection-graph resolution
Recommended article: Satisfiability, branch-width and Tseitin tautologies
Recommended article: A Resolution Calculus for Shortening Proofs
Recommended article: Lower Bounds of Static Lovász-Schrijver Calculus Proofs for Tseitin Tautologies
Recommended article: Q3444802
Recommended article: \(T\)-resolution: Refinements and model elimination
description: scientific article; zbMATH DE number 7495569