Sweep-Based Propagation for String Constraint Solving
Authors: Roberto Amadini, Graeme Gange, Peter Stuckey
AAAI 2018 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental evidences show that sweep-based propagation is able to significantly outperform state-of-the-art approaches for string constraint solving. |
| Researcher Affiliation | Academia | Roberto Amadini, Graeme Gange, Peter J. Stuckey Department of Computing and Information Systems The University of Melbourne, Australia {roberto.amadini,gkgange,pstuckey}@unimelb.edu.au |
| Pseudocode | Yes | function PUSH+(Sl,u, Y , (i, o)) (is, os) (i, o) k l while k > 0 i |Y | do T l ,u Y [i] if S T = then Incompatible blocks (i, o) (i + 1, 0) if l > o then If not nullable, (is, os) (i, o) restart from here k l end if else if k (u o) then Remainder fits in Y [i] return (is, os), (i, o) else Fill Y [i] and continue k k (u o) (i, o) (i + 1, 0) end if end while return (is, os), (i, o) end function |
| Open Source Code | Yes | The source code is publicly available at (G-Strings 2017) G-Strings. 2017. Source code. Accessed November 2017. https://bitbucket.org/robama/g-strings. |
| Open Datasets | No | We extended the benchmarks used in (Amadini et al. 2017) by generating new instances of the SQL problem introduced in (Amadini et al. 2016). We then randomly generated 200 harder instances from this problem; in particular, for each ℓ {250, 500, 1000, 5000, 10000} we generated 20 satisfiable and 20 unsatisfiable instances. The paper describes generating custom instances of existing benchmarks but does not provide explicit public access information (link, DOI, repository) for these generated datasets. |
| Dataset Splits | No | The paper conducts experiments by solving problem instances but does not specify any training, validation, or test dataset splits in the context of data partitioning for model training/evaluation. |
| Hardware Specification | Yes | We ran the experiments on Ubuntu 15.10 machines with 16 GB of RAM and 2.60 GHz Intel R i7 CPU. |
| Software Dependencies | Yes | We used the last stable releases Z3STR3 1.0.0 and CVC4 1.5. |
| Experiment Setup | Yes | For each of these problems we derived 5 instances by varying the maximum string length ℓ {250, 500, 1000, 5000, 10000}. We then randomly generated 200 harder instances from this problem; in particular, for each ℓ {250, 500, 1000, 5000, 10000} we generated 20 satisfiable and 20 unsatisfiable instances. solving time is set to the timeout T = 600 seconds if a solver can not solve a problem. |