Search-space partitioning for parallelizing SMT solvers

DOI10.1007/978-3-319-24318-4_27MaRDI QIDQ3453241zbMATH OpenOpenAlexFDO

Authors Antti E. J. Hyvärinen, Matteo Marescotti, Natasha Sharygina

Publication date 20 November 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-24318-4_27

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Parallel algorithms in computer science (68W10)

Recommendations

• Partitioning SAT instances for distributed solving
• Parallelizing SMT solving: lazy decomposition and conciliation
• OpenSMT2: an SMT solver for multi-core and cloud computing
• Partitioning search spaces of a randomized search
• SMTS: Distributed, Visualized Constraint Solving

Cites work

• A fast parallel SAT-solver -- efficient workload balancing
• An overview of parallel SAT solving
• Exploiting symmetry in SMT problems
• Incorporating clause learning in grid-based randomized SAT solving
• MCMT: a model checker modulo theories
• On SAT Modulo Theories and Optimization Problems
• Optimization in SMT with \(\mathcal{LA}(\mathbb Q)\) cost functions
• Partitioning search spaces of a randomized search
• PSATO: A distributed propositional prover and its application to quasigroup problems
• Simplify: a theorem prover for program checking
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Symbolic optimization with SMT solvers
• Term Rewriting and Applications
• The MathSAT5 SMT solver
• Theory and Applications of Satisfiability Testing

Cited in

(6)

• Parallelizing SMT solving: lazy decomposition and conciliation
• OpenSMT2: an SMT solver for multi-core and cloud computing
• Partitioning search spaces of a randomized search
• PARSSSE: AN ADAPTIVE PARALLEL STATE SPACE SEARCH ENGINE
• Partitioning methods for satisfiability testing on large formulas
• Partitioning SAT instances for distributed solving

Describes a project that uses

Uses Software

• MiniSat
• Yices
• z3
• SIMPLIFY
• CVC4
• MathSAT5
• SAFARI
• PSATO
• Chaff
• SYMBA
• OpenSMT
• SATO
• Mcmt
• vZ

This page was built for publication: Search-space partitioning for parallelizing SMT solvers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3453241)