Clause Sharing and Partitioning for Cloud-Based SMT Solving
| Autor: | Matteo Marescotti, Antti E. J. Hyvärinen, Natasha Sharygina |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Theoretical computer science
Computer science business.industry Programming language Scale (chemistry) Cloud computing 0102 computer and information sciences 02 engineering and technology Solver computer.software_genre 01 natural sciences Satisfiability Constraint (information theory) 010201 computation theory & mathematics Computer Science::Logic in Computer Science Factor (programming language) Problem domain Satisfiability modulo theories 0202 electrical engineering electronic engineering information engineering Computer Science::Programming Languages 020201 artificial intelligence & image processing business computer computer.programming_language |
| Zdroj: | Automated Technology for Verification and Analysis ISBN: 9783319465197 ATVA |
| Popis: | Satisfiability modulo theories (SMT) allows the modeling and solving of constraint problems arising from practical domains by combining well-engineered and powerful solvers for propositional satisfiability with expressive, domain-specific background theories in a natural way. The increasing popularity of SMT as a modelling approach means that the SMT solvers need to handle increasingly complex problem instances. This paper studies how SMT solvers can use cloud computing to scale to challenging problems through sharing of learned information in the form of clauses with approaches based on both divide-and-conquer and algorithm portfolios. Our initial experiments, executed on the OpenSMT2 solver, show that parallelization with clause sharing speeds up the solving of instances, on average, by a factor of four or five depending on the problem domain. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|