Propositional Encodings of Acyclicity and Reachability by Using Vertex Elimination
Authors: Masood Feyzbakhsh Rankooh, Jussi Rintanen5861-5868
AAAI 2022 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | An empirical study demonstrates that our methods do often outperform both earlier encodings of these constraints as well as Graph SAT especially when underlying graphs have a low directed elimination width. |
| Researcher Affiliation | Academia | Department of Computer Science, Aalto University, Helsinki, Finland |
| Pseudocode | No | No structured pseudocode or algorithm blocks were found in the paper. |
| Open Source Code | No | The paper does not provide any specific repository link, explicit code release statement, or mention of code in supplementary materials for the methodology described. |
| Open Datasets | Yes | Moreover, we have used planning problem set of (Pandey and Rintanen 2018), which are solvable by both acyclicity checking and eventual reachability checking of their underlying graphs. |
| Dataset Splits | No | The paper does not provide specific dataset split information (exact percentages, sample counts, citations to predefined splits, or detailed splitting methodology) needed to reproduce the data partitioning. |
| Hardware Specification | No | All experiments were run in a cluster of Linux machines, with a 1800 second timeout limit per instance, and a memory limit of 64 GB. (This is not specific enough about CPU/GPU models or other detailed hardware specs.) |
| Software Dependencies | No | All instances have been solved using Graph SAT, which becomes the Glucose SAT solver (Audemard and Simon 2009) in the absence of special graph constraints. For the planning benchmarks we have also used Kissat (Biere et al. 2020), which has won the first place in the main track of the SAT Competition 2020. (While specific solvers are named and cited, explicit version numbers like 'Glucose 3.0' or 'Kissat 4.2' are not provided.) |
| Experiment Setup | Yes | As the heuristic for elimination orderings of the vertex elimination methods, we have used mindegree, that is, eliminating a vertex with minimal total number of incoming and outgoing edges in the graph produced after the elimination of previously eliminated vertices. ... All experiments were run in a cluster of Linux machines, with a 1800 second timeout limit per instance, and a memory limit of 64 GB. |