Reasoning with propositional logic: from SAT solvers to knowledge compilation

DOI10.1007/978-3-030-06167-8_5MaRDI QIDQ6602252zbMATHFDO

Authors Laurent Simon

Publication date 11 September 2024

Mathematics Subject Classification ID

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

Recommendations

• Introduction to propositional satisfiability
• Propositional SAT solving
• Mechanizing Mathematical Reasoning
• scientific article; zbMATH DE number 1470716
• Handbook of satisfiability. In 2 parts

Cites work

• scientific article; zbMATH DE number 1696808 (Why is no real title available?)
• scientific article; zbMATH DE number 4162321 (Why is no real title available?)
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 1995157 (Why is no real title available?)
• scientific article; zbMATH DE number 1765680 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A Generalized Framework for Conflict Analysis
• A machine program for theorem-proving
• Average time analyses of simplified Davis-Putnam procedures
• Backjumping for quantified Boolean logic satisfiability
• Blocked clause elimination for QBF
• Building decision procedures for modal logics from propositional decision procedures -- the case study of modal K
• Characterizing diagnoses and systems
• Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
• Diagnosing multiple faults
• Graph-Based Algorithms for Boolean Function Manipulation
• Lazy clause exchange policy for parallel SAT solvers
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Many hard examples for resolution
• On compiling CNFs into structured deterministic DNNFs
• On the complexity of regular resolution and the Davis-Putnam procedure
• Planning as quantified Boolean formula
• Principles and Practice of Constraint Programming – CP 2004
• Random formulas have frozen variables
• Relations between average case complexity and approximation complexity
• Resolution for quantified Boolean formulas
• SAT-Based Model Checking without Unrolling
• The asymptotic \(k\)-SAT threshold
• The complexity of theorem-proving procedures
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

Cited in

(1)

• Reasoning and inference for (maximum) satisfiability: new insights

This page was built for publication: Reasoning with propositional logic: from SAT solvers to knowledge compilation

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