Co-Certificate Learning with SAT Modulo Symmetries
Authors: Markus Kirchweger, Tomáš Peitl, Stefan Szeider
IJCAI 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | In the following we will present an experimental comparison of SMS+CCL to various alternative methods on the task of finding non-3-colorable triangle-free graphs with 10 14 vertices, showing how we can visit fewer candidate graphs and learn small sets of colorings thanks to SMS and CCL. This section is devoted to a description of our SAT encoding for the search of KS graphs, followed by a discussion of experimental results. |
| Researcher Affiliation | Academia | Markus Kirchweger , Tom aˇs Peitl and Stefan Szeider Algorithms and Complexity Group, TU Wien, Austria {mk, peitl, sz}@ac.tuwien.ac.at |
| Pseudocode | No | The paper describes algorithmic steps in narrative text and via a flowchart (Figure 1) but does not contain a formally labeled 'Pseudocode' or 'Algorithm' block. |
| Open Source Code | Yes | All our code is available on Git Hub3. 3https://github.com/markirch/sat-modulo-symmetries |
| Open Datasets | No | The paper describes methods for generating graphs with specific properties (e.g., triangle-free, non-010-colorable KS graphs) rather than utilizing pre-existing public datasets for training or evaluation. Therefore, there is no explicit mention of a publicly available or open dataset being used. |
| Dataset Splits | No | The paper focuses on graph generation and verification rather than machine learning model training, and thus does not include descriptions of training/test/validation dataset splits. |
| Hardware Specification | Yes | We ran our experiments on a cluster with different processors4 under Ubuntu 18.04. 4Intel Xeon {E5540, E5649, E5-2630 v2, E5-2640 v4}@ at most 2.60 GHz, AMD EPYC 7402@2.80GHz |
| Software Dependencies | Yes | We use version 4.11.2 of Z3 and all tests are executed with a single thread. In our implementation, the user can choose between Cadical with the IPASIR-UP interface [Fazekas et al., 2023] (a state of the art incremental CDCL SAT-solver with inprocessing) and Clingo (an ASP solver containing a CDCL SAT solver). |
| Experiment Setup | Yes | In order to construct representative cubes, we would effectively have to reimplement SMS in a look-ahead solver; we instead opted for the simpler option of using the same SMS solver for the cubing process as for the subsequent solving. We proceed as follows for generating the cubes. We start the solver and whenever the number of assigned edge variables exceeds a pre-defined threshold, we add the partial assignment on the edge variables to the list of cubes, and exclude the current partial assignment on the edge variables from the solver. ... We first let the solver run for a specific amount of time (prerun) before generating the cubes. (Table 5: n #cubes prerun #var. t max(t) 22 18659 2 days 120 112 sec 8946 sec 23 313665 2 days 140 137 sec 63812 sec) |