Propositional SAT solving
From MaRDI portal
Recommendations
Cites work
- A Computing Procedure for Quantification Theory
- A linear-time transformation of linear inequalities into conjunctive normal form
- A machine program for theorem-proving
- A Machine-Oriented Logic Based on the Resolution Principle
- A New Look at BDDs for Pseudo-Boolean Constraints
- A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
- A structure-preserving clause form translation
- Algorithms for computing minimal unsatisfiable subsets of constraints
- BerkMin: A fast and robust SAT-solver
- Cardinality networks: a theoretical and empirical study
- Compact translations of non-disjunctive answer set programs to propositional clauses
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- Efficient data structures for backtrack search SAT solvers
- Extended clause learning
- Extending clause learning DPLL with parity reasoning
- Finding Dominators in Directed Graphs
- Forward checking and intelligent backtracking
- Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis
- Graph-Based Algorithms for Boolean Function Manipulation
- GRASP: a search algorithm for propositional satisfiability
- scientific article; zbMATH DE number 5798406 (Why is no real title available?)
- scientific article; zbMATH DE number 5139161 (Why is no real title available?)
- scientific article; zbMATH DE number 5510691 (Why is no real title available?)
- scientific article; zbMATH DE number 2080328 (Why is no real title available?)
- scientific article; zbMATH DE number 2080337 (Why is no real title available?)
- scientific article; zbMATH DE number 1470716 (Why is no real title available?)
- scientific article; zbMATH DE number 2085252 (Why is no real title available?)
- scientific article; zbMATH DE number 1903357 (Why is no real title available?)
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- scientific article; zbMATH DE number 3313427 (Why is no real title available?)
- scientific article; zbMATH DE number 956858 (Why is no real title available?)
- scientific article; zbMATH DE number 956863 (Why is no real title available?)
- scientific article; zbMATH DE number 956865 (Why is no real title available?)
- Implementing the Davis-Putnam method
- Inprocessing rules
- Interpolation and SAT-based model checking.
- Iterative and core-guided maxsat solving: a survey and assessment
- Locating Minimal Infeasible Constraint Sets in Linear Programs
- ManySAT: a parallel SAT solver
- Minimaxsat: an efficient weighted Max-SAT solver
- New Encodings of Pseudo-Boolean Constraints into CNF
- On computing backbones of propositional theories
- On computing minimal models
- Practical algorithms for unsatisfiability proof and core generation in SAT solvers
- Principles and practice of constraint programming - CP 2000. 6th international conference, Singapore, September 18--21, 2000. Proceedings
- Property-directed incremental invariant generation
- Reasoning with minimal models: efficient algorithms and applications
- SAT-based MaxSAT algorithms
- SAT-Based Model Checking without Unrolling
- Satisfiability-based algorithms for Boolean optimization
- SATO: An efficient propositional prover
- SATzilla: portfolio-based algorithm selection for SAT
- Simulating circuit-level simplifications on CNF
- Solving QBF with counterexample guided refinement
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- The Complexity of Propositional Proofs
- The complexity of theorem-proving procedures
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Theory and applications of satisfiability testing -- SAT 2009. 12th international conference, SAT 2009, Swansea, UK, June 30--July 3, 2009. Proceedings
- 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
- Towards efficient MUS extraction
- Variable Dependency in Local Search: Prevention Is Better Than Cure
Cited in
(36)- A BDD SAT solver for satisfiability testing: An industrial case study
- Computing with SAT oracles: past, present and future
- On tackling the limits of resolution in SAT solving
- Separating signs in the propositional satisfiability problem
- A modal view on resource-bounded propositional logics
- CrystalBall: gazing in the black box of SAT solving
- Propositional proof systems based on maximum satisfiability
- Simulating parity reasoning
- SAT and SMT are still resolution: questions and challenges
- Inprocessing rules
- Empirical study of the anatomy of modern SAT solvers
- Binary decision diagrams
- Combining Model Checking and Deduction
- Model Checking Security Protocols
- DPLL: the core of modern satisfiability solvers
- Using Boolean Constraint Propagation for Sub-clauses Deduction
- Model checking with Boolean Satisfiability
- A Pearl on SAT Solving in Prolog
- Boolean satisfiability and EDA applications
- Learning from conflicts in propositional satisfiability
- scientific article; zbMATH DE number 1113999 (Why is no real title available?)
- scientific article; zbMATH DE number 6874827 (Why is no real title available?)
- Anatomy and empirical evaluation of modern SAT solvers
- On the Unreasonable Effectiveness of SAT Solvers
- scientific article; zbMATH DE number 7559496 (Why is no real title available?)
- Building strategies into QBF proofs
- Handbook of satisfiability. In 2 parts
- Theory and Applications of Satisfiability Testing
- Introduction to propositional satisfiability
- Present and Future of Practical SAT Solving
- RegSTAB: A SAT Solver for Propositional Schemata
- Solving String Theories Involving Regular Membership Predicates Using SAT
- Reasoning with propositional logic: from SAT solvers to knowledge compilation
- SAT modulo symmetries for graph generation and enumeration
- Proof complexity of modal resolution
- SAT-solving in practice, with a tutorial example from supervisory control
Describes a project that uses
Uses Software
This page was built for publication: Propositional SAT solving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3176367)
