SAT-Based Techniques for Lexicographically Smallest Finite Models
Authors: Mikoláš Janota, Choiwah Chow, João Araújo, Michael Codish, Petr Vojtěchovský
AAAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We provide an implementation of the proposed algorithm and evaluate it on a variety of algebraic structures. The tool was evaluated on several popular algebraic structures (algebras) defined in Table 1. |
| Researcher Affiliation | Academia | 1Czech Technical University in Prague, Czechia 2Center for Mathematics and Applications (NOVA Math), Portugal 3Department of Mathematics, NOVA FCT, Portugal 4Ben-Gurion University of the Negev, Beer-Sheva, Israel 5University of Denver, USA |
| Pseudocode | Yes | Algorithm 1: Calculate lexmin (D, ) for given (D, ) by gradual construction. |
| Open Source Code | No | The paper mentions 'We call our tool mlex' but does not provide any explicit statement or link for its open-source availability. |
| Open Datasets | Yes | The evaluation was performed on randomly generated samples from five algebraic structures: groups, loops, general magmas, quasigroups, and semigroups. For groups, we randomly pick the groups given by the All Small Groups function in GAP. For magmas and semigroups, we generate them with the help of GAP functions such as Random. For quasigroups and loops, we use the Random Quasigroup and Random Loop functions in the LOOPS package in GAP. |
| Dataset Splits | No | The paper evaluates its algorithm on randomly generated samples and fixed orders, but does not mention any explicit training, validation, or test dataset splits, as the task is not a machine learning task involving training. |
| Hardware Specification | Yes | The experiments are run on an Intel Xeon CPU E5-2630 v2 2.6 GHz 24 computer, with 64 Gb RAM. |
| Software Dependencies | Yes | We call our tool mlex and it supports two SAT solvers, minisat (E en and S orensson 2003) and cadical (Biere 2017). |
| Experiment Setup | Yes | The evaluation was performed on randomly generated samples from five algebraic structures: groups, loops, general magmas, quasigroups, and semigroups. We consider a total of 210 random samples of the five algebraic structures listed in Table 1, of orders 16 to 128 in increments of 16. In addition, we include random samples of 5 magmas of each of the orders 192 and 256. Finally, a timeout of 30 minutes is used for calculating the lexmin copy of each model. For search strategies, we compare between linear-unsat-sat (lus) and modified binary search (bin2). |