SATO: An efficient propositional prover
From MaRDI portal
Publication:5234711
DOI10.1007/3-540-63104-6_28zbMath1430.68427OpenAlexW1511155470MaRDI QIDQ5234711
Publication date: 1 October 2019
Published in: Automated Deduction—CADE-14 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-63104-6_28
Related Items
On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers ⋮ An experiment with satisfiability modulo SAT ⋮ What we can learn from conflicts in propositional satisfiability ⋮ Propositional SAT Solving ⋮ The state of SAT ⋮ BerkMin: A fast and robust SAT-solver ⋮ Random backtracking in backtrack search algorithms for satisfiability ⋮ Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL ⋮ A Decision-Making Procedure for Resolution-Based SAT-Solvers ⋮ 3-Valued Circuit SAT for STE with Automatic Refinement ⋮ Equivalent literal propagation in the DLL procedure ⋮ A satisfiability procedure for quantified Boolean formulae ⋮ SAT problems with chains of dependent variables ⋮ Towards Robust CNF Encodings of Cardinality Constraints ⋮ Hierarchical Hardness Models for SAT ⋮ Formal verification based on Boolean expression diagrams ⋮ Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. ⋮ Another look at graph coloring via propositional satisfiability ⋮ Combining enumeration and deductive techniques in order to increase the class of constructible infinite models ⋮ A heuristic block coordinate descent approach for controlled tabular adjustment ⋮ The Mechanical Verification of a DPLL-Based Satisfiability Solver ⋮ On SAT instance classes and a method for reliable performance experiments with SAT solvers ⋮ Efficient data structures for backtrack search SAT solvers ⋮ Toward leaner binary-clause reasoning in a satisfiability solver ⋮ On deciding subsumption problems ⋮ Learning action models from plan examples using weighted MAX-SAT ⋮ Equivalency reasoning to solve a class of hard SAT problems. ⋮ Complexity results for structure-based causality. ⋮ Extending and implementing the stable model semantics ⋮ A logic programming approach to knowledge-state planning. II: The DLV\(^\mathcal K\) system ⋮ SAT-based planning in complex domains: Concurrency, constraints and nondeterminism
Uses Software
Cites Work
