Solving SAT and SAT Modulo Theories
From MaRDI portal
Publication:3455223
DOI10.1145/1217856.1217859zbMath1326.68164OpenAlexW2022846948MaRDI QIDQ3455223
Cesare Tinelli, Albert Oliveras, Robert Nieuwenhuis
Publication date: 4 December 2015
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1217856.1217859
Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items
Abstract interpretation as automated deduction ⋮ Multi-agent pathfinding with continuous time ⋮ Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Automating Induction with an SMT Solver ⋮ On abstract modular inference systems and solvers ⋮ Interpolation systems for ground proofs in automated deduction: a survey ⋮ Semantically-guided goal-sensitive reasoning: model representation ⋮ An experiment with satisfiability modulo SAT ⋮ Adding decision procedures to SMT solvers using axioms with triggers ⋮ A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ Deciding unifiability and computing local unifiers in the description logic \(\mathcal{EL}\) without top constructor ⋮ A unified framework for DPLL(T) + certificates ⋮ Protocol analysis with time ⋮ Rewriting modulo SMT and open system analysis ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Solving linear optimization over arithmetic constraint formula ⋮ Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL ⋮ Metalevel transformation of strategies ⋮ Three-valued semantics for hybrid MKNF knowledge bases revisited ⋮ On First-Order Model-Based Reasoning ⋮ A progression semantics for first-order logic programs ⋮ Optimization Modulo Theories with Linear Rational Costs ⋮ An Equation-Based Classical Logic ⋮ The ins and outs of first-order runtime verification ⋮ Twenty years of rewriting logic ⋮ raSAT: an SMT solver for polynomial constraints ⋮ Cardinality constraints for arrays (decidability results and applications) ⋮ Better answers to real questions ⋮ Ordered completion for first-order logic programs on finite structures ⋮ What is answer set programming to propositional satisfiability ⋮ First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation ⋮ Axiomatic Constraint Systems for Proof Search Modulo Theories ⋮ A pearl on SAT and SMT solving in Prolog ⋮ Superposition as a decision procedure for timed automata ⋮ Superposition decides the first-order logic fragment over ground theories ⋮ Complete Boolean satisfiability solving algorithms based on local search ⋮ SMT proof checking using a logical framework ⋮ Satisfiability in composition-nominative logics ⋮ Curriculum-based course timetabling with SAT and MaxSAT ⋮ Solving constraint satisfaction problems with SAT modulo theories ⋮ Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories ⋮ Relating constraint answer set programming languages and algorithms ⋮ Improved algorithms for the general exact satisfiability problem ⋮ Syntax-guided quantifier instantiation ⋮ Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories ⋮ Incremental search for conflict and unit instances of quantified formulas with E-matching ⋮ Reducing Chaos in SAT-Like Search: Finding Solutions Close to a Given One ⋮ On Interpolation in Decision Procedures ⋮ I-RiSC: An SMT-Compliant Solver for the Existential Fragment of Real Algebra ⋮ SMT-based model checking for recursive programs ⋮ An efficient SMT solver for string constraints ⋮ Producing and verifying extremely large propositional refutations ⋮ Conflict-driven answer set solving: from theory to practice ⋮ Synthesis of quantifier-free DNF sentences from inconsistent samples of strings with EF games and SAT ⋮ Cardinality networks: a theoretical and empirical study ⋮ Engineering constraint solvers for automatic analysis of probabilistic hybrid automata ⋮ A formal methods approach to predicting new features of the eukaryotic vesicle traffic system ⋮ IPL: an integration property language for multi-model cyber-physical systems ⋮ Hard problems in max-algebra, control theory, hypergraphs and other areas ⋮ Refutation-based synthesis in SMT ⋮ Efficiently and effectively recognizing toricity of steady state varieties ⋮ Access Nets: Modeling Access to Physical Spaces ⋮ The SAT+CAS method for combinatorial search with applications to best matrices ⋮ On solving quantified bit-vector constraints using invertibility conditions ⋮ Range and Set Abstraction using SAT ⋮ Algorithmic reduction of biological networks with multiple time scales ⋮ A conflict-driven solving procedure for poly-power constraints ⋮ \textsc{OptiMathSAT}: a tool for optimization modulo theories ⋮ Conflict-driven satisfiability for theory combination: transition system and completeness ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ⋮ A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT ⋮ Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers ⋮ Deciding Bit-Vector Formulas with mcSAT ⋮ Predicate Elimination for Preprocessing in First-Order Theorem Proving ⋮ Transition systems for model generators—A unifying approach ⋮ Efficient SAT-based proof search in intuitionistic propositional logic ⋮ A unifying splitting framework ⋮ Superposition with first-class booleans and inprocessing clausification ⋮ SPASS-SATT. A CDCL(LA) solver ⋮ SCL clause learning from simple models ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic ⋮ From simplification to a partial theory solver for non-linear real polynomial constraints ⋮ A complete and terminating approach to linear integer solving ⋮ Opposition Frameworks ⋮ Wombit: a portfolio bit-vector solver using word-level propagation ⋮ Theory decision by decomposition ⋮ Solving bitvectors with MCSAT: explanations from bits and pieces ⋮ A decision procedure for string to code point conversion ⋮ Model-based Theory Combination ⋮ Encoding First Order Proofs in SMT ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column ⋮ Flexible proof production in an industrial-strength SMT solver ⋮ SAT-based proof search in intermediate propositional logics ⋮ Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description) ⋮ Reasoning about vectors using an SMT theory of sequences ⋮ Estimating the volume of solution space for satisfiability modulo linear real arithmetic ⋮ Iterative and core-guided maxsat solving: a survey and assessment ⋮ Cutting to the chase. ⋮ On interpolation in automated theorem proving ⋮ Belief Merging by Examples ⋮ Verifying Procedural Programs via Constrained Rewriting Induction ⋮ A proof system for graph (non)-isomorphism verification ⋮ Automated Reasoning Building Blocks ⋮ Congruence Closure of Compressed Terms in Polynomial Time ⋮ Search-Space Partitioning for Parallelizing SMT Solvers ⋮ Propositional SAT Solving ⋮ SAT-Based Model Checking ⋮ Satisfiability Modulo Theories ⋮ Modal Tableau Systems with Blocking and Congruence Closure ⋮ Shared aggregate sets in answer set programming ⋮ On CDCL-Based Proof Systems with the Ordered Decision Strategy ⋮ Reasoning about vectors: satisfiability modulo a theory of sequences ⋮ Verification Modulo theories ⋮ Well-founded operators for normal hybrid MKNF knowledge bases ⋮ SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions ⋮ Predicate logic as a modeling language: modeling and solving some machine learning and data mining problems withIDP3 ⋮ Disjunctive answer set solvers via templates ⋮ Constraint answer set solver EZCSP and why integration schemas matter ⋮ Constraint solving for finite model finding in SMT solvers ⋮ Local Search For Satisfiability Modulo Integer Arithmetic Theories ⋮ Unifying splitting ⋮ Reluplex: a calculus for reasoning about deep neural networks ⋮ Abstract Solvers for Computing Cautious Consequences of ASP programs ⋮ Decoding Output Sequences for Discrete-Time Linear Hybrid Systems. ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver ⋮ Synthesising programs with non-trivial constants ⋮ Railway scheduling using Boolean satisfiability modulo simulations ⋮ Stepwise debugging of answer-set programs ⋮ Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems ⋮ Constraint CNF: SAT and CSP Language Under One Roof. ⋮ Probabilistic logic over equations and domain restrictions ⋮ Towards SMT Model Checking of Array-Based Systems ⋮ Deciding Effectively Propositional Logic Using DPLL and Substitution Sets ⋮ Engineering DPLL(T) + Saturation ⋮ The CADE-27 Automated theorem proving System Competition – CASC-27 ⋮ Disjunctive logic programs with existential quantification in rule heads ⋮ DPLL: The Core of Modern Satisfiability Solvers ⋮ ASP modulo CSP: The clingcon system ⋮ SMCHR: Satisfiability modulo constraint handling rules ⋮ Constraint Answer Set Solving ⋮ The Strategy Challenge in SMT Solving ⋮ Superposition for Bounded Domains ⋮ A translational approach to constraint answer set solving ⋮ A Slice-Based Decision Procedure for Type-Based Partial Orders ⋮ Linear Quantifier Elimination as an Abstract Decision Procedure ⋮ Unnamed Item ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ Volume Computation for Boolean Combination of Linear Arithmetic Constraints ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ Multi-shot ASP solving with clingo ⋮ Unification in the Description Logic $\mathcal{EL}$ without the Top Concept ⋮ Model Evolution with Equality Modulo Built-in Theories ⋮ Cutting to the Chase Solving Linear Integer Arithmetic ⋮ Solving Systems of Linear Inequalities by Bound Propagation ⋮ The External Interface for Extending WASP ⋮ Boosting Answer Set Optimization with Weighted Comparator Networks ⋮ Preface ⋮ Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates ⋮ Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution ⋮ A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses ⋮ Unsatisfiable Core Analysis and Aggregates for Optimum Stable Model Search ⋮ Abstract Answer Set Solvers ⋮ Modal Satisfiability via SMT Solving
