Parallelizing SMT solving: lazy decomposition and conciliation
From MaRDI portal
Recommendations
- Search-space partitioning for parallelizing SMT solvers
- Fast and parallel decomposition of constraint satisfaction problems
- An expressive model for instance decomposition based parallel SAT solvers
- Parallel SAT solving in bounded model checking
- Lazy clause exchange policy for parallel SAT solvers
- Reproducible efficient parallel SAT solving
- scientific article; zbMATH DE number 1304346
- scientific article; zbMATH DE number 828719
Cites work
- scientific article; zbMATH DE number 3566230 (Why is no real title available?)
- A Decision Procedure for Bit-Vectors and Arrays
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- An interpolating theorem prover
- Automated Deduction – CADE-20
- Automated reasoning and exhaustive search: Quasigroup existence problems
- Compression of propositional resolution proofs by lowering subproofs
- Computer Aided Verification
- Computer Aided Verification
- Computer aided verification. 21st international conference, CAV 2009, Grenoble, France, June 26--July 2, 2009. Proceedings
- Constraint solving for interpolation
- Counterexample-guided abstraction refinement for symbolic model checking
- Efficient generation of Craig interpolants in satisfiability modulo theories
- Exploiting symmetry in SMT problems
- Fast Decision Procedures Based on Congruence Closure
- Generating minimum transitivity constraints in P-time for deciding equality logic
- Ground interpolation for the theory of equality
- Interpolation and SAT-based model checking.
- Interpolation and Symbol Elimination
- Lazy Abstraction with Interpolants
- Lazy abstraction
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Logic in Computer Science
- ManySAT: a parallel SAT solver
- PSATO: A distributed propositional prover and its application to quasigroup problems
- Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
- Quantifier-free interpolation in combinations of equality interpolating theories
- Rewriting-based quantifier-free interpolation for a theory of arrays
- Solvable cases of the decision problem
- The MathSAT5 SMT solver
- Theory and Applications of Satisfiability Testing
- Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Proceedings
- Tools and algorithms for the construction and analysis of systems. 15th international conference, TACAS 2009, held as part of the joint European conferences on theory and practice of software, ETAPS 2009, York, UK, March 22--29, 2009. Proceedings
- Two techniques for minimizing resolution proofs
Cited in
(6)- scientific article; zbMATH DE number 7301731 (Why is no real title available?)
- Search-space partitioning for parallelizing SMT solvers
- Towards better heuristics for solving bounded model checking problems
- SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME
- SMTS: Distributed, Visualized Constraint Solving
- OpenSMT2: an SMT solver for multi-core and cloud computing
Describes a project that uses
Uses Software
This page was built for publication: Parallelizing SMT solving: lazy decomposition and conciliation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1749390)
