Search-space partitioning for parallelizing SMT solvers

DOI10.1007/978-3-319-24318-4_27zbMATH Open1471.68244OpenAlexW2281633864MaRDI QIDQ3453241FDOQ3453241

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

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

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)

Cites Work

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

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

Uses Software

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

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)