×

Applying SAT solving in classification of finite algebras. (English) Zbl 1109.68103

Summary: 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.

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Alur, R. and Peled, D. (eds.): Proc. of Computer Aided Verification, 16th International Conference, CAV 2004, Vol. 3114 of LNCS, Springer, 2004. · Zbl 1056.68003
[2] Audemard, G., Bertoli, P., Cimatti, A., Korniowicz, A. and Sebastiani, R.: Integrating Boolean and mathematical solving: foundations, basic algorithms and requirements, in Proc. of CALCULEMUS-2002, Vol. 2385 of LNAI, 2002. · Zbl 1072.68603
[3] Barrett, C. and Berezin, S.: CVC Lite: A New Implementation of the Cooperating Validity Checker, in [1], 2004, pp. 515–518. · Zbl 1103.68605
[4] Colton, S.: The HR program for theorem generation, in [23], 2002. · Zbl 1072.68567
[5] Colton, S., Meier, A., Sorge, V. and McCasland, R.: Automatic generation of classification theorems for finite algebras, in Proc. of IJCAR 2004, Vol. 3097 of LNAI, 2004, pp. 400–414. Springer. · Zbl 1126.68562
[6] Fujita, M., Slaney, J. and Bennett, F.: Automatic generation of some results in finite algebra, in Proc. IJCAI-13, 1993, pp. 52–57.
[7] Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A. and Tinelli, C.: DPLL(T): Fast Decision Procedures, in [1], 2004, pp. 175–188. · Zbl 1103.68616
[8] Gap: GAP Reference Manual, The GAP Group, School of Mathematical and Computational Sciences, University of St. Andrews, 2000.
[9] Gomes, C. P., Selman, B., Crato, N. and Kautz, H.: Heavy-tailed phenomena in satisfiability and constraint satisfaction problems, J. Autom. Reason. 24 (2000), 67–100. · Zbl 0967.68145
[10] Kunen, K: Single axioms for groups, J. Autom. Reason. 9(3) (1992), 291–308. · Zbl 0794.20001
[11] McCune, W.: Single axioms for groups and Abelian groups with various operations, J. Autom. Reason. 10(1) (1993), 1–3. · Zbl 0794.20002
[12] McCune, W.: A Davis-Putnam program and its application to finite first order model search: quasigroup existence problems. Technical report ANL/MCS-TM-194, Argonne National Laboratory, Division of MSC, 1994.
[13] McCune, W.: Mace4 Reference Manual and Guide, Argonne National Laboratory. ANL/MCS-TM-264, 2003.
[14] Mckay, B. D., Meinart, A. and Myrvold, W.: Counting small Latin squares, in European Women in Mathematics Int. Workshop on Groups and Graphs, 2002, pp. 67–72.
[15] McKay, B. D. and Wanless, I. M.: The number of Latin squares of order eleven. Submitted for publication. Available at http://cs.anu.edu.au/\(\sim\)bdm/papers/1s11.pdf .
[16] Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L. and Malik, S.: Chaff: engineering an efficient SAT solver, in Proc. of the Design Automation Conference, 2001, pp. 530–535.
[17] Nonnengart, A. and Weidenbach, C.: Computing small clause normal forms, in Handbook of Automated Reasoning, Elsevier, 2001. · Zbl 0992.03018
[18] Pflugfelder, H. O.: Quasigroups and Loops: Introduction, Vol. 7 of Sigma Series in Pure Mathematics, Helderman Verlag, 1990. · Zbl 0715.20043
[19] Slaney, J.: FINDER, Notes and Guide, Center for Information Science Research Australian National University, 1995.
[20] Slaney, J., Fujita, M. and Stickel, M. E.: Automated reasoning and exhaustive search: quasigroup existense problems, Comput. Math. Appl. 29 (1995), 115–132. · Zbl 0827.20083
[21] Sutcliffe, G.: The IJCAR-2004 Automated Theorem Proving Competition AI Communications 18(1) (2005), 33–40.
[22] Sutcliffe, G. and Suttner, C.: The TPTP problem library: CNF release v1.2.1, J. Aut. Reason. 21(2) (1998), 177–203. · Zbl 0910.68197
[23] Voronkov, A. (ed.): Proc. of the 18th International Conference on Automated Deduction (CADE-18), Vol. 2392 of LNAI, Springer, 2002. · Zbl 0993.00050
[24] Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobald, C. and Topic, D.: SPASS Version 2.0. in [23], pp. 275–279.
[25] Zhang, H.: SATO: an efficient propositional prover, in Proc. of CADE-14, vol. 1249 of LNAI, 1997, pp. 272–275.
[26] Zhang, H.: Specifying Latin squares in propositional logic, in Automated Reasoning and Its Applications, Essays in honor of Larry Wos, MIT Press, 1997.
[27] Zhang, H., Bonacina, M. P. and Hsiang, J.: PSATO: a distributed propositional prover and its application to quasigroup problems, J. Symb. Comput. 21 (1996), 543–560. · Zbl 0863.68013
[28] Zhang, H. and Hsiang, J.: Solving open quasigroup problems by propositional reasoning, in Proc. of Int. Computer Symposium, Hsinchu, Taiwan, 1994.
[29] Zhang, J. and Zhang, H.: SEM User’s Guide, Department of Computer Science, University of Iowa, 2001.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.