Algebraic Theory Exploration: A Comparison of Technologies

Quratul Ain Mahesar, Volker Sorge

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

We present a case study in comparing tools for theory exploration in finite algebra. Our aim is to compare experimentally diverse technologies for generating finite algebraic structures. In particular, we compare the performance of model generators, constraint solvers and satisfiability solvers in their ability to generate large algebraic structures, in our case quasigroups, that exhibit some desired property. In addition to a straight forward comparison of technologies using a number of non-trivial properties, we also experiment with techniques that further constrain the original problems by pre-computing additional information and observe its effect on the performance of different systems. We thereby use two particular constructions, one based on randomisation the other on pre-computing additional knowledge. The former filters randomly pre-computed elements by automated theorem proving to exclude unsuitable instantiations. The latter employs a concept of generating systems particularly suitable for quasigroups, that can be easily computed for small size quasigroups and evolved to be suitable for larger size structures. We present comparative experimental results to evaluate our proposed approaches in terms of increasing the solvability horizon as well as time reduction in finding the solutions for the algebraic structures with particular properties. The experimental results give us insight into the suitable selection of the systems that could benefit from the presented algebraic techniques.

Original languageEnglish
Title of host publicationSYNASC 2012
Subtitle of host publication14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
EditorsAndrei Voronkov, Viorel Negru, Tetsuo Ida, Tudor Jebelean, Dana Petcu, Stephen Watt, Daniela Zaharie
PublisherIEEE Computer Society
Pages70-77
Number of pages8
ISBN (Print)9780769549347, 9781467350266
DOIs
Publication statusPublished - 26 Sep 2012
Externally publishedYes
Event14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2012 - Timisoara, Romania
Duration: 26 Sep 201229 Sep 2012

Conference

Conference14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2012
CountryRomania
CityTimisoara
Period26/09/1229/09/12

Fingerprint

Dive into the research topics of 'Algebraic Theory Exploration: A Comparison of Technologies'. Together they form a unique fingerprint.

Cite this