Probabilistic Inference for Predicate Constraint Satisfaction
Authors: Yuki Satake, Hiroshi Unno, Hinata Yanagi1644-1651
AAAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We have implemented the presented method and obtained promising results on existing benchmarks as well as new ones that are beyond the scope of existing CHC solvers. 5 Implementation and Evaluation We have implemented a constraint solver PCSAT for the full class of p CSP based on the presented method. We adopted MINISAT (E en and S orensson 2004) and Z3 (de Moura and Bjørner 2008) as the backend SAT and SMT solvers, respectively. We conducted three sets of experiments. |
| Researcher Affiliation | Academia | Yuki Satake,1 Hiroshi Unno,1,2 Hinata Yanagi1 1University of Tsukuba, 2RIKEN AIP {satake, uhiro, hinata}@logic.cs.tsukuba.ac.jp |
| Pseudocode | No | The paper describes its methods in prose and does not include any explicit pseudocode or algorithm blocks. |
| Open Source Code | No | The paper states 'We have implemented the presented method' but does not provide an explicit statement about releasing the source code for their implementation or a link to a code repository. |
| Open Datasets | Yes | We have implemented the presented method and obtained promising results on existing benchmark sets from Sy Gu S-Comp 2017 and 2018 (Invariant Synthesis Track), and CHC-COMP 2019 (LIA-nonlin Track) as well as a new benchmark set... 6http://sygus.org/comp/ 7https://chc-comp.github.io/ |
| Dataset Splits | No | The paper uses existing benchmark sets (Sy Gu S-Comp, CHC-COMP) but does not provide explicit details about train/validation/test dataset splits, such as percentages or sample counts, that would be needed to reproduce the data partitioning for these benchmarks. |
| Hardware Specification | Yes | All the experiments were conducted on 3.1GHz Intel Xeon Platinum 8000 CPU and 32 Gi B RAM. |
| Software Dependencies | No | The paper mentions using 'MINISAT (E en and S orensson 2004) and Z3 (de Moura and Bjørner 2008) as the backend SAT and SMT solvers' but does not provide specific version numbers for these software dependencies. |
| Experiment Setup | Yes | We evaluated the impact of our SID-based multiple solution enumeration technique on the convergence speed of CEGIS using the benchmark set consisting of 127 linear CHCs from the Inv Track category of Sy Gu S-Comp 2018 with 300s timeout. Figure 1 summarizes the results of running PCSAT with different configurations obtained by varying the number #cand of candidate solutions generated in the synthesis phase, and enabling or disabling SID... |