Parallelizing SMT solving: lazy decomposition and conciliation
type: Item
instance of: scholarly article
title: Parallelizing SMT solving: lazy decomposition and conciliation
zbMATH Open document ID: 1444.68169
author: Xianqiang Yang
published in: Artificial Intelligence
publication date: 2018-05-16T00:00:00Z
Mathematics Subject Classification ID: 68T20
Mathematics Subject Classification ID: 68W10
zbMATH DE Number: 6869125
zbMATH Keywords: satisfiability modulo theories
zbMATH Keywords: parallelization
zbMATH Keywords: lazy decomposition
zbMATH Keywords: conciliation
zbMATH Keywords: theory of equality with uninterpreted functions
describes a project that uses: Yices
describes a project that uses: z3
describes a project that uses: CVC4
describes a project that uses: MathSAT5
describes a project that uses: FOCI
describes a project that uses: Treengeling
describes a project that uses: PSATO
describes a project that uses: UCLID
describes a project that uses: Boolector
describes a project that uses: ManySAT
describes a project that uses: Princess
describes a project that uses: Chaff
describes a project that uses: Plingeling
describes a project that uses: MiniSat
describes a project that uses: SATO
describes a project that uses: Skeptik
describes a project that uses: Lingeling
describes a project that uses: STP
MaRDI profile type: Publication
full work available at URL: j.artint.2018.01.001
OpenAlex ID: W2791364807
cites work: Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
cites work: Q4138187
cites work: Theory and Applications of Satisfiability Testing
cites work: Computer Aided Verification
cites work: A Decision Procedure for Bit-Vectors and Arrays
cites work: Q1008939
cites work: Q2479551
cites work: The MathSAT5 SMT Solver
cites work: Logic in Computer Science
cites work: Fast Decision Procedures Based on Congruence Closure
cites work: Linear reasoning. A new form of the Herbrand-Gentzen theorem
cites work: Interpolation and Symbol Elimination
cites work: An interpolating theorem prover
cites work: Ground interpolation for the theory of equality
cites work: An interpolating sequent calculus for quantifier-free Presburger arithmetic
cites work: Rewriting-based Quantifier-free Interpolation for a Theory of Arrays.
cites work: Efficient generation of craig interpolants in satisfiability modulo theories
cites work: Constraint solving for interpolation
cites work: Automated Deduction – CADE-20
cites work: Quantifier-free interpolation in combinations of equality interpolating theories
cites work: Computer aided verification. 21st international conference, CAV 2009, Grenoble, France, June 26--July 2, 2009. Proceedings
cites work: Generating minimum transitivity constraints in P-time for deciding equality logic
cites work: Automated reasoning and exhaustive search: Quasigroup existence problems
cites work: Solvable cases of the decision problem
cites work: Exploiting Symmetry in SMT Problems
cites work: Q3639756
cites work: PSATO: A distributed propositional prover and its application to quasigroup problems
cites work: Counterexample-guided abstraction refinement for symbolic model checking
cites work: Lazy abstraction
cites work: Lazy Abstraction with Interpolants
cites work: Compression of Propositional Resolution Proofs by Lowering Subproofs
cites work: Two Techniques for Minimizing Resolution Proofs
DOI: 10.1016/J.ARTINT.2018.01.001
Recommended article: Search-Space Partitioning for Parallelizing SMT Solvers
Recommended article: Fast and parallel decomposition of constraint satisfaction problems
Recommended article: An Expressive Model for Instance Decomposition Based Parallel SAT Solvers
Recommended article: Parallel SAT Solving in Bounded Model Checking
Recommended article: Lazy Clause Exchange Policy for Parallel SAT Solvers
Recommended article: Reproducible efficient parallel SAT solving
Recommended article: Q4251078
Recommended article: Q4859227