Abstract
We propose a new benchmark set consisting of problems generated during the construction of classification theorems for quasigroups. It extends and generalises the domain of quasigroup existence problems, to which SAT solvers have been applied successfully in the past, to a rich class of benchmarks of varying difficulty.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alur, R., Peled, D. (eds.): CAV 2004. LNCS, vol. 3114. Springer, Heidelberg (2004)
Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D. (eds.) [1], pp. 515–518
Colton, S., Meier, A., Sorge, V., McCasland, R.: Automatic generation of classification theorems for finite algebras. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 400–414. Springer, Heidelberg (2004)
Fujita, M., Slaney, J., Bennett, F.: Automatic Generation of Some Results in Finite Algebra. In: Proc. of IJCAI–13, pp. 52–57. Morgan Kaufmann, San Francisco (1993)
Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Dpll(t): Fast decision procedures. In: Alur, R., Peled, D. (eds.) [1], pp. 175–188
Kumar, S.R., Russel, A., Sundaram, R.: Approximating latin square extensions. Algorithmica 24, 128–138 (1999)
Laywine, C., Mullen, G.: Discrete Mathematics using Latin Squares. Wiley, Chichester (1998)
McCune, W.W.: A davis-putnam program and its application to finite first-order model search: quasigroup existence problems. Report, Argonne Nat. Labs (1994)
Meier, A., Sorge, V.: Applying sat solving in classification in finite algebra. Submitted to the Journal of Automated Reasoning
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient sat solver. In: Proc. of the Design Automation Conference, pp. 530–535 (2001)
Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Handbook of Automated Reasoning. Elsevier, Amsterdam (2001)
Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobald, C., Topic, D.: SPASS version 2.0. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 275–279. Springer, Heidelberg (2002)
Zhang, H.: Specifying latin squares in propositional logic. In: Automated Reasoning and Its Applications, Essays in honor of Larry Wos. MIT Press, Cambridge (1997)
Zhang, H., Bonacina, M., Hsiang, J.: PSATO: a distributed propositional prover and its application to quasigroup problems. J. of Symb. Computation 21, 543–560 (1996)
Zhang, H., Hsiang, J.: Solving Open Quasigroup Problems by Propositional Reasoning. In: Proc. of International Computer Symposium (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Meier, A., Sorge, V. (2005). A New Set of Algebraic Benchmark Problems for SAT Solvers. In: Bacchus, F., Walsh, T. (eds) Theory and Applications of Satisfiability Testing. SAT 2005. Lecture Notes in Computer Science, vol 3569. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11499107_39
Download citation
DOI: https://doi.org/10.1007/11499107_39
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26276-3
Online ISBN: 978-3-540-31679-4
eBook Packages: Computer ScienceComputer Science (R0)