Clause Sharing and Partitioning for Cloud-Based SMT Solving
Clause Sharing and Partitioning for Cloud-Based SMT Solving
复制标题
基于云的 SMT 求解的子句共享和分区
DOI：
10.1007/978-3-319-46520-3_27
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
N. Sharygina
中科院分区：
文献类型：
--
作者：
Matteo Marescotti;A. Hyvärinen;N. Sharygina
可满足性模理论（SMT）允许建模和解决约束问题所产生的实际领域相结合的工程和强大的解决方案，命题可满足性与表达，领域特定的背景理论，以自然的方式。SMT作为一种建模方法的日益普及意味着SMT求解器需要处理越来越复杂的问题实例。本文研究了SMT求解器如何使用云计算来扩展到具有挑战性的问题，通过共享学习到的信息，以子句的形式与基于分治和算法组合的方法。我们的初步实验，在OpenSMT2求解器上执行，表明子句共享的并行化加速了实例的求解，平均而言，取决于问题域的四到五倍。
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.