Implementing efficient All solutions SAT solvers
From MaRDI portal
Abstract: All solutions SAT (AllSAT for short) is a variant of propositional satisfiability problem. Despite its significance, AllSAT has been relatively unexplored compared to other variants. We thus survey and discuss major techniques of AllSAT solvers. We faithfully implement them and conduct comprehensive experiments using a large number of instances and various types of solvers including one of the few public softwares. The experiments reveal solver's characteristics. Our implemented solvers are made publicly available so that other researchers can easily develop their solver by modifying our codes and compare it with existing methods.
Recommendations
Cites work
- A symbolic approach to predicate abstraction.
- An incremental algorithm to check satisfiability for bounded model checking
- Automated technology for verification and analysis. 10th international symposium, ATVA 2012, Thiruvananthapuram, India, October 3--6, 2012. Proceedings
- Backjump-based backtracking for constraint satisfaction problems
- Binary Decision Diagrams
- Computational aspects of monotone dualization: a brief survey
- Computer Aided Verification
- Computing the Tutte polynomial of a graph of moderate size
- Conflict-directed backjumping revisited
- Decision diagrams and dynamic programming
- Decomposable negation normal form
- Decomposition of the flow polynomial
- Discrete optimization with decision diagrams
- Dualization of Boolean functions using ternary decision diagrams
- Efficient algorithms for dualizing large-scale hypergraphs
- Enumerating prime implicants of propositional formulae in conjunctive normal form
- Formula Caching in DPLL
- Graph-Based Algorithms for Boolean Function Manipulation
- GRASP: a search algorithm for propositional satisfiability
- Handbook of knowledge representation.
- scientific article; zbMATH DE number 5852793 (Why is no real title available?)
- scientific article; zbMATH DE number 5510691 (Why is no real title available?)
- scientific article; zbMATH DE number 1568060 (Why is no real title available?)
- scientific article; zbMATH DE number 2102695 (Why is no real title available?)
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- scientific article; zbMATH DE number 3353170 (Why is no real title available?)
- Itemset mining: a constraint programming perspective
- Mining top-\(k\) motifs with a SAT-based framework
- On preprocessing techniques and their impact on propositional model counting
- On the power of clause-learning SAT solvers as resolution engines
- Predicate abstraction of ANSI-C programs using SAT
- SATLIB: An online resource for research on SAT
- Solution Enumeration for Projected Boolean Search Problems
- TG-Pro: A SAT-based ATPG system
- The art of computer programming. Volume 4A. Combinatorial algorithms. Part 1.
- The language of search
- The minimal hitting set generation problem: algorithms and computation
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
Cited in
(19)- Faradžev Read-type enumeration of non-isomorphic CC systems
- The geometry of gaussoids
- Solving projected model counting by utilizing treewidth and its limits
- Optimizing S-Box Implementations for Several Criteria Using SAT Solvers
- Weighted model counting on the GPU by exploiting small treewidth
- Theory and Applications of Satisfiability Testing
- Formal Methods in Computer-Aided Design
- Theory and Applications of Satisfiability Testing
- Construction methods for gaussoids.
- Exploiting Database Management Systems and Treewidth for Counting
- Selfadhesivity in Gaussian conditional independence structures
- SAF: SAT-based attractor finder in asynchronous automata networks
- On the benefits of knowledge compilation for feature-model analyses
- Self-adhesivity in lattices of abstract conditional independence models
- On enumerating short projected models
- Sign patterns of principal minors of real symmetric matrices
- Exploiting partial-assignment enumeration in optimization modulo theories
- Entailing generalization boosts enumeration
- On CNF conversion for SAT and SMT enumeration
This page was built for publication: Implementing efficient All solutions SAT solvers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5266602)
