3 papers
cs.LO2025
Complete Symmetry Breaking for Finite Models
Marek DanÄo, Mikoláš Janota, Michael Codish +1
This paper introduces a SAT-based technique that calculates a compact and complete symmetry-break for finite model finding, with the focus on structures with a single binary operat…
cs.LO2025
SAT-Based Techniques for Lexicographically Smallest Finite Models
Mikoláš Janota, Choiwah Chow, João Araújo +2
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 e…
cs.LO2025
Cube-based Isomorph-free Finite Model Finding
Choiwah Chow, Mikoláš Janota, João Araújo
Complete enumeration of finite models of first-order logic (FOL) formulas is pivotal to universal algebra, which studies and catalogs algebraic structures. Efficient finite model e…