2 papers
cs.LO2024
Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses
Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
All-Solution Satisfiability (AllSAT) and its extension, All-Solution Satisfiability Modulo Theories (AllSMT), have become more relevant in recent years, mainly in formal verificati…
cs.AI2024
Dynamic Blocked Clause Elimination for Projected Model Counting
Jean-Marie Lagniez, Pierre Marquis, Armin Biere
In this paper, we explore the application of blocked clause elimination for projected model counting. This is the problem of determining the number of models ||\exists X.Σ|| of a p…