Boosting definability bipartition computation using SAT witnesses

DOI10.1007/978-3-031-43619-2_47MaRDI QIDQ6545575zbMATH OpenFDO

Authors Jean-Marie Lagniez, Pierre Marquis

Publication date 29 May 2024

Full work available at URL https://doi.org/10.1007/978-3-031-43619-2_47

zbMATH Keywords

automated reasoning including satisfiability checking and its extensionsdefinabilitypropositional logic

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27)

Recommendations

• Definability for model counting
• Minimal sets on propositional formulae. Problems and reductions
• Partitioning methods for satisfiability testing on large formulas
• Mining definitions in Kissat with Kittens
• On the query complexity of selecting minimal sets for monotone predicates

Cites work

• Definability for model counting
• Efficient Knowledge Compilation Beyond Weighted Model Counting
• scientific article; zbMATH DE number 1946872 (Why is no real title available?)
• scientific article; zbMATH DE number 3085803 (Why is no real title available?)
• Improving Glucose for incremental SAT solving with assumptions: application to MUS extraction
• On computing minimal independent support and its applications to sampling and counting
• On preprocessing techniques and their impact on propositional model counting
• On propositional definability
• Theory and Applications of Satisfiability Testing

Cited in

(2)

• Dynamic blocked clause elimination for projected model counting
• Enhancing query efficiency for D-DNNF representations through preprocessing

This page was built for publication: Boosting definability bipartition computation using SAT witnesses

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