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) Parallel algorithms in computer science (68W10) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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
• PSATO: A distributed propositional prover and its application to quasigroup problems
• Partitioning search spaces of a randomized search
• 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)

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

Describes a project that uses

Uses Software

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

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)