Frontiers of Combining Systems - 12th International Symposium, FroCoS 2019, London, UK, September 4-6, 2019, Proceedings
Frontiers of Combining Systems - 12th International Symposium, FroCoS 2019, London, UK, September 4-6, 2019, Proceedings
复制标题
组合系统前沿 - 第十二届国际研讨会，FroCoS 2019，英国伦敦，2019 年 9 月 4-6 日，会议记录
DOI：
10.1007/978-3-030-29007-8_1
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Reger G
中科院分区：
文献类型：
--
作者：
Reger G
这项工作认为，（多排序）一阶逻辑的有限模型发现的MACE风格的方法。这种现有的方法迭代地假设增加域的大小和编码相应的模型存在问题作为SAT问题。最初的MACE工具及其后继者考虑了避免在所产生的SAT问题中引入对称性的技术，但这从来不是以前工作的重点，也没有得到集中关注。在这项工作中，我们正式的对称性避免问题，一个健全的对称性破缺启发式的概念，提出了一些这样的prostitics和评估他们的实验与吸血鬼定理证明器中的实施。我们的研究结果表明，这些新的算法在SMT-LIB和TPTP的一些基准测试中提高了性能。最后，我们表明，直接对称性破缺技术可以用来提高有限模型的发现，但其成本意味着对称性避免仍然是首选的方法。
This work considers the MACE-style approach to finite model finding for (multi-sorted) first-order logic. This existing approach iteratively assumes increasing domain sizes and encodes the corresponding model existence problem as a SAT problem. The original MACE tool and its successors have considered techniques for avoiding introducing symmetries in the resulting SAT problem, but this has never been the focus of the previous work and has not received concentrated attention. In this work we formalise the symmetry avoiding problem, characterise the notion of a sound symmetry breaking heuristic, propose a number of such heuristics and evaluate them experimentally with an implementation in the Vampire theorem prover. Our results demonstrate that these new heuristics improve performance on a number of benchmarks taken from SMT-LIB and TPTP. Finally, we show that direct symmetry breaking techniques could be used to improve finite model finding, but that their cost means that symmetry avoidance is still the preferable approach.