Dynamic blocked clause elimination for projected model counting

DOI10.4230/LIPICS.SAT.2024.21MaRDI QIDQ6864420zbMATH OpenFDO

Authors Jean-Marie Lagniez, Pierre Marquis, Armin Biere

Publication date 3 February 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.SAT.2024.21

zbMATH Keywords

blocked clause eliminationprojected model countingpropositional logic

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational aspects of satisfiability (68R07) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Cites work

• \(\#{\exists}\mathrm{SAT}\): projected model counting
• A new exact solver for (Weighted) Max\#SAT
• Blocked clause elimination
• Blocked clauses in first-order logic
• Boosting definability bipartition computation using SAT witnesses
• Clause elimination for SAT and QSAT
• Covered clauses are not propagation redundant
• Definability for model counting
• scientific article; zbMATH DE number 1946872 (Why is no real title available?)
• scientific article; zbMATH DE number 839556 (Why is no real title available?)
• Inprocessing rules
• On a generalization of extended resolution
• On preprocessing techniques and their impact on propositional model counting
• Preprocessing for DQBF
• Quantitative evaluation of systems. 10th international conference, QEST 2013, Buenos Aires, Argentina, August 27--30, 2013. Proceedings
• Simulating circuit-level simplifications on CNF
• Solving projected model counting by utilizing treewidth and its limits
• Strong extension-free proof systems
• Taming high treewidth with abstraction, nested dynamic programming, and database technology

This page was built for publication: Dynamic blocked clause elimination for projected model counting

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