SAT-Based Techniques for Lexicographically Smallest Finite Models
Mikoláš Janota, Choiwah Chow, João Araújo, Michael Codish, Petr Vojtěchovský
TL;DR
The paper addresses canonicalizing finite algebraic structures by computing the lexicographically smallest isomorphic copy, enabling direct isomorphism checks and easy cataloging. It introduces a SAT-based framework that builds the lexmin magma in a black-box fashion, gradually constructing the target table via isomorphic copies and a permutation f, rather than materializing an explicit target representation. A suite of propagation techniques—including first-row identification, budgeting, row invariants, mid-row refinement, upper-bounds from partial models, and monotone search strategies—significantly reduces SAT calls and improves robustness. Empirical evaluation on diverse algebraic structures demonstrates that these enhancements yield strong performance, validating the practicality of SAT-based LexMin for routine algebraic cataloging and isomorphism-aware enumeration. The work opens avenues for tighter solver integration and extension to multi-table structures and constrained non-isomorphic enumerations.
Abstract
This paper proposes SAT-based techniques to calculate a specific normal form of a given finite mathematical structure (model). The normal form is obtained by permuting the domain elements so that the representation of the structure is lexicographically smallest possible. Such a normal form is of interest to mathematicians as it enables easy cataloging of algebraic structures. In particular, two structures are isomorphic precisely when their normal forms are the same. This form is also natural to inspect as mathematicians have been using it routinely for many decades. We develop a novel approach where a SAT solver is used in a black-box fashion to compute the smallest representative. The approach constructs the representative gradually and searches the space of possible isomorphisms, requiring a small number of variables. However, the approach may lead to a large number of SAT calls and therefore we devise propagation techniques to reduce this number. The paper focuses on finite structures with a single binary operation (encompassing groups, semigroups, etc.). However, the approach is generalizable to arbitrary finite structures. We provide an implementation of the proposed algorithm and evaluate it on a variety of algebraic structures.