Complete Symmetry Breaking for Finite Models
Authors: Marek Dančo, Mikoláš Janota, Michael Codish, João Jorge Araújo
AAAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experiments We implemented Algorithms 1 and 2 in Python3 using the Py SAT package (Ignatiev, Morgado, and Marques Silva 2018) with Ca Di Ca L 1.9.5 (Biere et al. 2020) as the back-end SAT solver. The knowledge-compilation-based tool d4 (Lagniez and Marquis 2017) was used for model counting. ... Table 2 summarizes the main achieved results. For each algebra class we list the highest size (n) where we were able to calculate the number of non-isomorphic models. ... These results highlight the power of our approach. |
| Researcher Affiliation | Academia | Marek Danˇco1, Mikol aˇs Janota1, Michael Codish2, Jo ao Jorge Ara ujo3 1Czech Technical University in Prague, Czechia 2Ben-Gurion University of the Negev, Beer-Sheva, Israel 3Department of Mathematics, NOVA FCT, Portugal EMAIL |
| Pseudocode | Yes | Algorithm 1 Compute Canonizing Set 1: Init: Π = 2: while A Mn π Sn s.t. minΠ(A) and π(A) A do 3: Π = Π {π} 4: end while 5: return Π |
| Open Source Code | No | No explicit statement or link for the paper's specific source code is provided. The text mentions implementing algorithms in Python using third-party tools like PySAT, CaDiCaL, and d4, but not the release of their own implementation code. |
| Open Datasets | No | No external datasets are used in the experiments. The paper focuses on computing algebraic structures defined by first-order logic formulas. While it references 'The On-Line Encyclopedia of Integer Sequences (OEIS)' for verifying counts, this is not a dataset used for input to the experiments. |
| Dataset Splits | No | The paper does not involve traditional datasets with train/test/validation splits. It is focused on generating and counting algebraic structures based on first-order logic formulas. |
| Hardware Specification | Yes | The experiments were run on a server with four AMD EPYC 7513 32-Core Processor@2.6GHz and with 504 GB of memory. |
| Software Dependencies | Yes | We implemented Algorithms 1 and 2 in Python3 using the Py SAT package (Ignatiev, Morgado, and Marques Silva 2018) with Ca Di Ca L 1.9.5 (Biere et al. 2020) as the back-end SAT solver. The knowledge-compilation-based tool d4 (Lagniez and Marquis 2017) was used for model counting. |
| Experiment Setup | Yes | For each problem, we set a memory limit of 50GB and a timeout of 24 hours. We use the rowby-row (vecr( )) and diagonal (vecd( )) vectorization as the bases of the lexicographic ordering (see Preliminaries)... Several representative algebra classes with domain sizes n 2..10 are considered... |