Proving unsatisfiability of CNFs locally

DOI10.1023/A:1015803927637MaRDI QIDQ1610678zbMATH OpenOpenAlexFDO

Authors Eugene Goldberg

Publication date 20 August 2002

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1015803927637

zbMATH Keywords

conjunctive normal formsatisfiability

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Proving unsatisfiability of CNFs locally
• Local Search for Unsatisfiability
• Trivial, tractable, hard. A not so sudden complexity jump in neighborhood restricted CNF formulas
• Testing satisfiability of CNF formulas by computing a stable set of points
• On Local Versus Global Satisfiability

Cites work

• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• A Machine-Oriented Logic Based on the Resolution Principle
• GRASP: a search algorithm for propositional satisfiability
• Hard examples for resolution
• scientific article; zbMATH DE number 1149402 (Why is no real title available?)
• Short proofs are narrow—resolution made simple
• The intractability of resolution

Cited in

(2)

• Proving unsatisfiability of CNFs locally
• Boundary Points and Resolution

This page was built for publication: Proving unsatisfiability of CNFs locally

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