Testing satisfiability of CNF formulas by computing a stable set of points

DOI10.1007/S10472-005-0420-XMaRDI QIDQ1777393zbMATH OpenOpenAlexFDO

Authors Eugene Goldberg

Publication date 13 May 2005

Published in Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10472-005-0420-x

zbMATH Keywords

conjunctive normal form

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Logic in artificial intelligence (68T27)

Recommendations

• scientific article; zbMATH DE number 2090298
• Partitioning methods for satisfiability testing on large formulas
• Why almost all satisfiable k-CNF formulas are easy
• A threshold for unsatisfiability
• Partitioning methods for satisfiability testing on large formulas

Cites work

• A machine program for theorem-proving
• Generating effective symmetry-breaking predicates for search problems
• scientific article; zbMATH DE number 956863 (Why is no real title available?)
• Many hard examples for resolution
• On the complexity of cutting-plane proofs
• Proving unsatisfiability of CNFs locally
• Short proofs for tricky formulas
• The intractability of resolution
• The symmetry rule in propositional logic

Cited in

(4)

• Proving unsatisfiability of CNFs locally
• Proving unsatisfiability of CNFs locally
• scientific article; zbMATH DE number 1241716 (Why is no real title available?)
• scientific article; zbMATH DE number 2090298 (Why is no real title available?)

Describes a project that uses

Uses Software

• Chaff

This page was built for publication: Testing satisfiability of CNF formulas by computing a stable set of points

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