Efficient and Complete FD-solving for extended array constraints
Authors: Quentin Plazar, Mathieu Acher, Sébastien Bardin, Arnaud Gotlieb
IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experiments show that the proposed solver significantly outperforms FD solvers, and successfully competes with the best SMT-solvers. |
| Researcher Affiliation | Academia | INRIA Bretagne-Atlantique, Rennes, France 2 CEA, LIST, Gif-sur-Yvette, F-91191, France 3 Simula Research Laboratory, Certus Center, Lysaker, Norway |
| Pseudocode | Yes | Algorithm 1: Propagator for consistent(L1, L2) |
| Open Source Code | No | The paper mentions implementing the technique inside fdcc, but does not provide a specific link or explicit statement about the availability of the source code for their implementation. |
| Open Datasets | Yes | First we take the 550 array formulas from the SMTCOMP benchmark, the standard competition in SMT solving with formulas coming essentially from hard verification-oriented industrial and academic case-studies. |
| Dataset Splits | No | The paper does not explicitly provide details about training/validation/test splits for the formulas used from the SMT-COMP benchmark, nor does it specify a cross-validation setup beyond using the benchmark formulas directly for evaluation. |
| Hardware Specification | Yes | Experiments were run on an Intel(R) Core(TM) i7-5600U (2,6 GHz) (2 cores), 16GB RAM, running Linux Fedora 22. |
| Software Dependencies | No | The paper mentions 'fdcc [Bardin and Gotlieb, 2012]', 'SICStus clpfd', 'Yices [Dutertre, 2014]', 'Math SAT [Cimatti et al., 2013]', 'CVC4 [Barrett et al., 2011]', and 'Z3 solver [De Moura and Bjørner, 2008]'. While it names software, it does not provide specific version numbers for these tools or libraries beyond the publication year of their foundational papers. |
| Experiment Setup | Yes | We compare each solver on the number of successfully resolved formulas... with a timeout set to 30 seconds... The results for a timeout of 120 seconds are also shown without discussion, since there is only very little difference. |