A Regular Matching Constraint for String Variables
Authors: Roberto Amadini, Peter J. Stuckey
IJCAI 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Empirical evidences show the effectiveness of our approach, implemented within the constraint programming framework, and tested against state-ofthe-art string solvers. Empirical results underline the importance of implementing native support for the match constraint. We compared the performance of our approach against different state-of-the-art string solving technologies. We implemented our match propagator in G-STRINGS, a string solver based on CP solver GECODE. We compare its performance against the approach using decomposition (1), which we will call G-STRINGSdec. We also include in the evaluation the state-of-the-art SMT solvers CVC5 [Barbosa et al., 2022] and Z3 [de Moura and Bjørner, 2008]. Fig. 3 shows the runtimes in seconds for n = 2, 3, . . . , 26. The results are shown in Tab. 1 |
| Researcher Affiliation | Collaboration | Roberto Amadini1 , Peter J. Stuckey2,3 1University of Bologna, Bologna, Italy 2Monash University, Melbourne, Victoria, Australia 3OPTIMA ARC Industrial Transformation and Training Centre, Melbourne, Australia |
| Pseudocode | Yes | Algorithm 1 PROPMATCH function. Algorithm 2 CHECKBLOCK function. |
| Open Source Code | No | We will disclose the source code in case of acceptance of the paper. |
| Open Datasets | No | For the Latin Square problem: "We use 2n string variables: r1, . . . , rn for the rows and c1, . . . , cn for the columns". For Shortest Matching Superstring: "We generated 16 sets Sl,n of patterns for n {32, 64, 128, 256} and l {5, 10, 15, 20}. Each Sl,n contains n random patterns such that there exists a string of length l matched by all patterns (but there could be a shorter one)." While they describe how they generated their problem instances/data, there is no statement about public availability or access information for these generated datasets. |
| Dataset Splits | No | The paper describes how problem instances were generated (e.g., Latin square for n=2 to 26, Shortest matching superstring with n and l parameters) but does not specify formal training, validation, or test splits of any dataset. It implies evaluation on generated instances. |
| Hardware Specification | Yes | We run all the experiments on a Ubuntu 22.04 machine with 8 GB of RAM and 1.60 GHz Intel i5 CPU, with a timeout of 300s. |
| Software Dependencies | Yes | We used CVC5 1.0.2 and Z3 4.11.2 with Z3str3 string solver (we also tried Z3seq, which did not improve Z3 s performance). |
| Experiment Setup | Yes | We encoded the problem in Mini Zinc [Nethercote et al., 2007] for G-STRINGS and G-STRINGSdec, while for SMT solvers we used the SMT-LIB [Barrett et al., 2010] language. For SMT solvers, we replaced each match constraint with a corresponding str.indexof function... We run all the experiments on a Ubuntu 22.04 machine with 8 GB of RAM and 1.60 GHz Intel i5 CPU, with a timeout of 300s. For the shortest matching superstring problem: "l is an upper bound on the length of the shortest string matched by all patterns. We use this information to provide an initial bound for each problem." |