A SAT Solver + Computer Algebra Attack on the Minimum Kochen–Specker Problem
Authors: Zhengyu Li, Curtis Bright, Vijay Ganesh
IJCAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Tables 2 and 3 contain our experimental results. As can be seen from Table 2, the sequential version of MATHCHECK outperforms the sequential SAT-only (Maple SAT) and CAS-only (nauty) tools. |
| Researcher Affiliation | Academia | Zhengyu Li1 , Curtis Bright2 , Vijay Ganesh1 1School of Computer Science, Georgia Institute of Technology, United States 2School of Computer Science, University of Windsor, Canada brian.li@gatech.edu, cbright@uwindsor.ca, vganesh45@gatech.edu |
| Pseudocode | No | The paper describes methods and algorithms in text but does not include any structured pseudocode or algorithm blocks (e.g., labeled 'Pseudocode' or 'Algorithm'). |
| Open Source Code | Yes | 1Code at https://github.com/Brian Li009/MathCheck |
| Open Datasets | No | The paper addresses a mathematical search problem (finding the minimum Kochen Specker vector system) using SAT solvers and CAS, rather than empirical training on a labeled dataset. |
| Dataset Splits | No | The paper describes a mathematical search and verification process, not a machine learning methodology that uses training, validation, and test dataset splits. |
| Hardware Specification | Yes | Results in Table 2 were conducted on a cluster of Intel E52683 v4 Broadwell @ 2.1GHz CPUs, each with access to 4 Gi B of RAM and running 64-bit Cent OS Linux 7. Results in Table 3 were conducted on a cluster of Dual Intel Xeon Gold 6226 CPUs @ 2.7 GHz (24 cores/node). |
| Software Dependencies | Yes | We used the g++ compiler version 9.3.0 with option -O3 to compile the SAT solvers used. |
| Experiment Setup | Yes | In MATHCHECK, we implement a slight modification of traditional Cn C practices to resolve the above challenges. In addition, we use a new Cn C solver ALPHAMAPLESAT [Jha et al., 2024] that provides significant speedup for the cubing process. In our proposed method, the cubing solver of ALPHAMAPLESAT operates on a much smaller CNF instance obtained by omitting all non-colorability constraints (Section 4.4). This approach is substantiated by empirical evidence suggesting that the same set of cubes can be obtained even without the non-colorability constraints. ALPHAMAPLESAT iteratively generates cubes until the total number of cubes surpasses a predefined cutoff, which is based on available computational resources. Following cube generation, each subproblem is processed by the simplification solver (Ca Di Ca L with OG), and then it is passed to the conquering solver (Maple SAT with OG) and solved in parallel. To efficiently manage the termination of each subproblem, a termination strategy is implemented: if the proof size for a subproblem exceeds 7 Gi B, the problem is further divided into more cubes and solved accordingly. |