Applying SAT Solving in Classification of Finite Algebras |
| |
Authors: | Andreas Meier Volker Sorge |
| |
Affiliation: | (1) DFKI GmbH, Saarbrucken, Germany;(2) School of Computer Science, University of Birmingham, Birmingham, UK |
| |
Abstract: | 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. |
| |
Keywords: | application of SAT finite algebra mathematics |
本文献已被 SpringerLink 等数据库收录! |
|