Reasoning with propositional logic: from SAT solvers to knowledge compilation

DOI10.1007/978-3-030-06167-8_5MaRDI QIDQ6602252zbMATH OpenFDO

Authors Laurent Simon

Publication date 11 September 2024

Full work available at URL https://doi.org/10.1007/978-3-030-06167-8_5

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

• 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
• 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?)
• 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)