On enumerating short projected models

DOI10.1016/J.DAM.2024.10.021MaRDI QIDQ6657245zbMATH OpenFDO

Authors Sibylle Möhle, Roberto Sebastiani, Armin Biere

Publication date 6 January 2025

Published in Discrete Applied Mathematics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.DAM.2024.10.021

zbMATH Keywords

all-SATmodel enumerationprojectionpropositional logic

Mathematics Subject Classification ID

Classical propositional logic (03B05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Model enumeration via assumption literals
• An isomorph-free SEM-like enumeration of models
• \(\#{\exists}\mathrm{SAT}\): projected model counting
• Tools and Algorithms for the Construction and Analysis of Systems
• Algorithms for Propositional Model Counting

Cites work

• \(\#{\exists}\mathrm{SAT}\): projected model counting
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• A Machine-Oriented Logic Based on the Resolution Principle
• A structure-preserving clause form translation
• A verified SAT solver framework with learn, forget, restart, and incrementality
• Advanced SMT techniques for weighted model integration
• Backing backtracking
• Chronological backtracking
• Compact DSOP and partial DSOP forms
• Formal Methods in Computer-Aided Design
• Formalization of Abstract State Transition Systems for SAT
• Four flavors of entailment
• GRASP: a search algorithm for propositional satisfiability
• scientific article; zbMATH DE number 1670796 (Why is no real title available?)
• scientific article; zbMATH DE number 4012495 (Why is no real title available?)
• scientific article; zbMATH DE number 1315584 (Why is no real title available?)
• scientific article; zbMATH DE number 1946853 (Why is no real title available?)
• scientific article; zbMATH DE number 1852147 (Why is no real title available?)
• scientific article; zbMATH DE number 1903357 (Why is no real title available?)
• scientific article; zbMATH DE number 3325539 (Why is no real title available?)
• Implementing efficient All solutions SAT solvers
• Interpolation and SAT-based model checking.
• Lazy satisfiability modulo theories
• Mathematical Foundations of Computer Science 2003
• Minimizing models for Tseitin-encoded SAT instances
• On converting CNF to DNF
• On probabilistic inference by weighted model counting
• Reusing the assignment trail in CDCL solvers
• Solution Enumeration for Projected Boolean Search Problems
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Solving the incremental satisfiability problem
• Temporal induction by incremental SAT solving
• The language of search
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Weighted model counting on the GPU by exploiting small treewidth

Cited in

(3)

• Submodel enumeration of Kripke structures in modal logic
• Entailment vs. verification for partial-assignment satisfiability and enumeration
• On CNF conversion for SAT and SMT enumeration

This page was built for publication: On enumerating short projected models

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