Algebraic Theory Exploration: A Comparison of Technologies

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.