Applying SAT Solving in Classification of Finite Algebras
Applying SAT Solving in Classification of Finite Algebras
复制标题
SAT 求解在有限代数分类中的应用
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
V. Sorge
中科院分区：
文献类型：
--
作者：
A. Meier;V. Sorge
数学结构的分类在纯数学研究中起着重要的作用。然而，这是一项细致的任务，可以通过使用自动化技术来辅助。许多自动化方法集中在分类的定量方面，比如对给定基数的某些结构的同构类进行计数。相比之下，我们设计了一种自举算法，该算法通过生成描述同构类的唯一区分属性的分类定理来执行定性分类。为了充分验证分类，证明一系列问题是必要的，即使在相对较小的代数结构的情况下，这对于经典的自动定理证明者来说也是相当具有挑战性的。但由于问题是在有限域中，采用布尔可满足性求解是可能的。本文给出了可满足解在有限代数中生成完全验证分类定理的应用。我们探索了多种方法来有效地编码布尔SAT求解器以及内置方程理论的求解器中出现的问题。我们给出了实验证据，证明了它们的有效性，从而改进了整个自举算法。
The classification of mathematical structures plays an important role for research in pure mathematics. It is, however, a meticulous task that can be aided by using automated techniques. Many automated methods concentrate on the quantitative side of classification, like counting isomorphism classes for certain structures with given cardinality. In contrast, we have devised a bootstrapping algorithm that performs qualitative classification by producing classification theorems that describe unique distinguishing properties for isomorphism classes. In order to fully verify the classification it is essential to prove a range of problems, which can become quite challenging for classical automated theorem provers even in the case of relatively small algebraic structures. But since the problems are in a finite domain, employing Boolean satisfiability solving is possible. In this paper we present the application of satisfiability solvers to generate fully verified classification theorems in finite algebra. We explore diverse methods to efficiently encode the arising problems both for Boolean SAT solvers as well as for solvers with built-in equational theory. We give experimental evidence for their effectiveness, which leads to an improvement of the overall bootstrapping algorithm.