Implementing Efficient All Solutions SAT Solvers
From MaRDI portal
Publication:5266602
DOI10.1145/2975585zbMath1365.68400arXiv1510.00523OpenAlexW3123509436MaRDI QIDQ5266602
Publication date: 16 June 2017
Published in: ACM Journal of Experimental Algorithmics (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1510.00523
conflict-directed backjumpingBDDknowledge compilationblocking clausemodel enumerationAllSAT solversCNF to DNF conversionformula caching
Learning and adaptive systems in artificial intelligence (68T05) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items
Exploiting Database Management Systems and Treewidth for Counting, Selfadhesivity in Gaussian conditional independence structures, Solving projected model counting by utilizing treewidth and its limits, SAF: SAT-based attractor finder in asynchronous automata networks, Unnamed Item, Faradžev Read-type enumeration of non-isomorphic CC systems, The geometry of gaussoids, Construction methods for gaussoids
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Mining top-\(k\) motifs with a SAT-based framework
- Dualization of Boolean functions using ternary decision diagrams
- On the power of clause-learning SAT solvers as resolution engines
- Itemset mining: a constraint programming perspective
- Automated technology for verification and analysis. 10th international symposium, ATVA 2012, Thiruvananthapuram, India, October 3--6, 2012. Proceedings
- Computational aspects of monotone dualization: a brief survey
- Decomposition of the flow polynomial
- Backjump-based backtracking for constraint satisfaction problems
- Predicate abstraction of ANSI-C programs using SAT
- On preprocessing techniques and their impact on propositional model counting
- Efficient algorithms for dualizing large-scale hypergraphs
- Discrete Optimization with Decision Diagrams
- Enumerating Prime Implicants of Propositional Formulae in Conjunctive Normal Form
- Formula Caching in DPLL
- The Minimal Hitting Set Generation Problem: Algorithms and Computation
- Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
- Solution Enumeration for Projected Boolean Search Problems
- Graph-Based Algorithms for Boolean Function Manipulation
- Binary Decision Diagrams
- GRASP: a search algorithm for propositional satisfiability
- Decision Diagrams and Dynamic Programming
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- Theory and Applications of Satisfiability Testing
- Decomposable negation normal form
- Tools and Algorithms for the Construction and Analysis of Systems
- Theory and Applications of Satisfiability Testing
- Computer Aided Verification
