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

DOI10.1007/s10472-005-0420-xzbMath1099.68099OpenAlexW2480672842MaRDI QIDQ1777393

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

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

Uses Software

• Chaff

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the complexity of cutting-plane proofs
• Short proofs for tricky formulas
• The intractability of resolution
• The symmetry rule in propositional logic
• Many hard examples for resolution
• A machine program for theorem-proving