Tseitin's formulas revisited

DOI10.1016/0304-3975(92)90356-KMaRDI QIDQ1193906zbMATH OpenOpenAlexFDO

Authors J.-D. Fouks

Publication date 27 September 1992

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(92)90356-k

zbMATH Keywords

cyclomatic cohesionresolutionTseitin's formulasTseitin's method

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Graph theory (05C99) Graph theory (including graph drawing) in computer science (68R10)

Recommendations

• scientific article; zbMATH DE number 176731
• Hard examples for resolution
• Graph expansion, Tseitin formulas and resolution proofs for CSP
• Characterizing Tseitin-Formulas with Short Regular Resolution Refutations
• Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs

Cites work

• A Computing Procedure for Quantification Theory
• A Machine-Oriented Logic Based on the Resolution Principle
• Hard examples for resolution
• scientific article; zbMATH DE number 3341035 (Why is no real title available?)
• Many hard examples for resolution
• Meta-resolution: An algorithmic formalisation
• On the complexity of regular resolution and the Davis-Putnam procedure
• The intractability of resolution

Cited in

(6)

• scientific article; zbMATH DE number 5993524 (Why is no real title available?)
• scientific article; zbMATH DE number 176731 (Why is no real title available?)
• scientific article; zbMATH DE number 6125146 (Why is no real title available?)
• Graph expansion, Tseitin formulas and resolution proofs for CSP
• Meta-resolution: An algorithmic formalisation
• A formula for Tignol's constant

This page was built for publication: Tseitin's formulas revisited

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