An Abstract CNF-to-d-DNNF Compiler Based on Chronological CDCL

DOI10.1007/978-3-031-43369-6_11MaRDI QIDQ6496630zbMATH OpenFDO

Authors Sibylle Möhle

Publication date 3 May 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-43369-6_11

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Recommendations

• On compiling CNFs into structured deterministic DNNFs
• Decomposable negation normal form
• Tableaux, path dissolution, and decomposable negation normal form for knowledge compilation
• Parameterized compilation lower bounds for restricted CNF-formulas
• CV-width: a new complexity parameter for CNFs

Cites work

• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Backing backtracking
• Cache conscious data structures for Boolean satisfiability solvers
• Chronological backtracking
• Compact DSOP and partial DSOP forms
• Compiling CP subproblems to MDDs and d-DNNFs
• Compiling relational Bayesian networks for exact inference
• Decomposable negation normal form
• Decomposing SAT problems into connected components
• Four flavors of entailment
• GRASP: a search algorithm for propositional satisfiability
• scientific article; zbMATH DE number 1946853 (Why is no real title available?)
• Laissez-faire caching for parallel \#SAT solving
• On compiling CNFs into structured deterministic DNNFs
• On limitations of structured (deterministic) DNNFs
• On the relation between structured \(d\)-DNNFs and SDDs
• On the Tractable Counting of Theory Models and its Application to Truth Maintenance and Belief Revision
• The language of search
• Theory and Applications of Satisfiability Testing

Cited in

(1)

• Verifying the conversion into CNF in dafny

This page was built for publication: An Abstract CNF-to-d-DNNF Compiler Based on Chronological CDCL

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