{"id":"25abf165-993a-494b-9a41-7c3bfe4f937c","arxiv_id":"1908.05907","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":4.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A preprocessing algorithm that converts small subproblems of a CSP into a regular constraint shows strong speedups on Black Hole, mixed results on Battleships, and best performance combined with table substitution.","lead":"This paper proposes replacing small parts of a constraint satisfaction problem with a single regular constraint that encodes all solutions of that part. Tests on two puzzle benchmarks show large speedups in one, mixed results in the other, and best results when regular and table constraints are combined.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The DFA construction is mathematically sound, but the empirical claim that regularization improves solver speed is not established: the only fully automatic regular variant is slower on Battleships and rarely fastest on Black Hole, and key runs are manual, unseeded, and unreleased.","rationale":"I read the construction in Section 3 as a prefix-trie DFA over the enumerated solutions of the sub-CSP; it accepts exactly the solution set and is deterministic, so the replacement preserves the solution set of the sub-CSP. The load-bearing weakness is therefore not mathematical correctness but the empirical support for the claimed speedup. The reader's weakest assumption about automatic detection and preprocessing cost aligns with this: the method is only useful if a suitable small sub-CSP can be found and solved cheaply, and the paper's own experiments show the plain Regular approach failing on Battleships. The reader's CONDITIONAL verdict already captures this; my stress-test adds no reason to move to ACCEPT or REJECT, but reinforces the need for controlled, reproducible experiments with separate transformation-time reporting and paired comparisons on matched solved instances.","tokens_in":7818,"tokens_out":9842,"duration_ms":109701,"concrete_test":"Re-run the full pipeline on the 35 Battleships and 50 Black Hole instances using the Akgun et al. heuristic, a fixed random seed, and released code, recording preparation time separately from search time. For each instance solved by both the original and the regularized model within the time limit, compute paired log-time ratios and report the median and the number of instances where the regularized model is faster. If the plain Regular variant is not faster than Original on the instances both models solve, and only the hand-selected TableRegularIntersected combination helps, then the central practical claim is not supported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim that replacing a sub-CSP by the constructed regular constraint can improve search speed rests on the experimental evaluation, and that evaluation is the weakest point of the paper. The paper's own Table 3 shows the plain 'Regular' approach on Battleships is on average 11.6% slower than the Original and is never the fastest on any instance; only the manually combined TableRegularIntersected variant shows a large gain. In Black Hole, the 'Regular' variant is fastest in only 2 of 50 instances, with most of the average gain coming from instances where the Original times out; no paired comparison on instances solved by both models is reported. The paper also admits in Remark 3 that the best combined variant was not computed automatically, and Remark 4 states that transformation times were not measured. Since Section 3 explicitly defers automatic detection of suitable sub-CSPs to future work, the current evidence does not establish that the method works as a practical, automatic preprocessing step. The construction itself appears correct, and the issue is not formal soundness but the unsupported practical speedup claim.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a preprocessing transformation for constraint satisfaction problems: a small sub-CSP is solved completely, all of its solutions are enumerated, and a deterministic finite automaton is constructed from the prefix sets of these solutions. The resulting regular constraint over the sub-CSP variables is then substituted for the original constraints of the sub-CSP. The authors argue that this strengthens propagation and reduces search effort, and they evaluate the idea on the Black Hole and Solitaire Battleships benchmarks against the original model and against table-constraint substitution. The construction itself is simple and mathematically transparent; the paper's central claim, however, is that the transformation improves solver speed in practice, and that claim rests on the experimental evaluation.","tokens_in":8020,"tokens_out":5393,"duration_ms":56687,"significance":"The DFA construction is sound: every transition is derived from a solution prefix, so the automaton accepts exactly the solution tuples of the enumerated sub-CSP, and replacing the sub-CSP constraints by the resulting regular constraint preserves the solution set of the full CSP. The approach has no fitted parameters and is not tuned to the benchmarks, and the comparison to the tabulation baseline is a useful reference point. If the empirical speedup claim were established, the method would be a simple and portable preprocessing technique for constraint solvers. However, the current experimental evidence is weakened by comparing averages over different solved-instance subsets, by relying on a manually combined variant for the strongest positive result, and by not measuring transformation times. The practical, automatic-preprocessing claim is therefore not yet fully supported.","major_comments":[{"comment":"The average solution times appear to be computed only over instances solved by each model: the Original model solves 7 of 50 Black Hole instances, while the modified models solve 47. Comparing averages such as 516.432s versus 58.796s therefore mainly reflects that the modified models solve many more instances, not that they are faster on the same instances. The paper should report a paired comparison restricted to instances solved by all compared models, state explicitly how timeouts are treated in the averages, and give per-instance statistics rather than a single average that mixes different solved-instance subsets.","section":"Section 4.1, Table 2"},{"comment":"In the Solitaire Battleships benchmark, the pure Regular variant is on average 11.6% slower than the Original model and is never the fastest on any of the 35 instances. The large reported average improvement of 60.8% comes from TableRegularIntersected, which combines table and regular constraints and, as Remark 3 states, was not computed fully automatically. Consequently this benchmark does not support the claim that the proposed transformation, applied automatically as a preprocessing step, improves solver speed; at best it indicates potential for a manually guided combination of tabulation and regularization.","section":"Section 4.2, Table 3 and Remark 3"},{"comment":"Transformation times are not measured; the paper only states that the total transformation time was less than three seconds for all Black Hole instances and less than four seconds for all Battleships instances, in comparison to 10- or 30-minute solution limits. Since the method is proposed as a preprocessing step, the transformation cost is part of the cost-benefit comparison and should be reported per instance and included in the reported total times rather than asserted to be negligible after the fact.","section":"Remark 4 (end of Section 4.2)"},{"comment":"Automatic detection of suitable sub-CSPs is explicitly deferred: the text states that 'an algorithm to detect such sub-CSPs must be developed in the future.' The experiments use the heuristic of [1] for Black Hole and manually indicated constraints for Battleships. The paper's stated goal of an automatic preprocessing transformation is therefore only partially realized in the evaluation. A revised version should either automate the detection for both benchmarks or clearly frame the contribution as a transformation whose automatic triggering remains open.","section":"Section 3"}],"minor_comments":[{"comment":"Table 3 is titled 'Overwiev of the Black Hole bechmark' but it presents the Solitaire Battleships results; the title and the typo should be corrected.","section":"Table 3"},{"comment":"The equivalence between the constructed DFA and the original sub-CSP is never stated as a formal lemma. A short proof by induction on the prefix length would make the formal contribution self-contained and would make the correctness claim explicit.","section":"Section 3, around Eqs. (3)-(7)"},{"comment":"The 50 Black Hole instances are randomly generated, but no seeds or benchmark files are provided. Releasing the instances or the generator would allow reproducibility and would enable a fair paired re-evaluation.","section":"Section 4.1"},{"comment":"The figures plot percentage improvements with negative values drawn at 1/10 of the real distance, which distorts the visual comparison. Plotting absolute solution times, or using a log scale, would give a more faithful picture of the per-instance behavior.","section":"Figures 1 and 2, footnote 2"}],"recommendation":"major_revision","confidential_remarks":"The main risk is that the empirical evaluation, which is the only evidence for the practical speedup claim, is under-powered and partly manual. If the authors provide paired comparisons on common solved instances, report transformation times, and make the benchmark and code available, I would be satisfied. Otherwise the paper should be reframed as a proof-of-concept transformation rather than a validated automatic optimization technique."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"I read the Löffler et al. paper. Here is my take.\n\nThe core idea is straightforward: take a small sub-CSP, solve it completely, build a DFA whose language is exactly the set of solution tuples, and replace the sub-CSP with a regular membership constraint. The construction is correct by construction—the DFA accepts exactly the solutions, so the original and transformed CSPs have the same solution set. The comparison to tabulation is a fair benchmark, and the combination of regular and table constraints is a sensible thing to try.\n\nThe paper is also transparent about its limitations. Remark 3 admits that the best-performing variant, TableRegularIntersected, was not fully automatic. Remark 4 says transformation times were not measured (though the authors note they were under four seconds). The paper does not hide the variability in the results.\n\nThe soft spots are all in the experimental evaluation. On Battleships, the plain Regular variant is on average 11.6% slower than Original, never fastest, and solves only 17 of 35 instances. The large average gain comes from TableRegularIntersected, which was manually assembled. On Black Hole, Regular is fastest in only 2 of 50 instances; most of the average gain comes from instances where Original times out. Averages are computed over different solved-instance sets, so they are not paired comparisons. The instances are unseeded, code and data are not released, and automatic detection of suitable sub-CSPs is deferred to future work. So the central claim that this method \"improves resolution speed\" is not established by the reported experiments.\n\nThe formal construction is not flawed, and the idea might hold for some problem classes once the evaluation is redone with paired comparisons, seeded instances, released code, and a fully automatic pipeline. As it stands, the paper reads like an extended abstract that needs another round of serious experimental work.\n\nWho is this for? Researchers working on CSP reformulation and preprocessing. The theoretical part is worth a look; the empirical part should not be cited as evidence of a general speedup.\n\nIn peer review: it deserves a referee rather than a desk rejection, because the formal construction is sound and the topic is relevant. But the review should focus heavily on the evaluation. I would recommend major revision with the experiments redone properly.","headline":"Correct DFA construction, honest about its own limitations, but the empirical speedup claim is not established by the reported evaluation.","tokens_in":8515,"tokens_out":3170,"would_cite":false,"duration_ms":31583,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Substituting a small solved sub-CSP with a single regular membership constraint preserves the solution set and speeds up constraint search in benchmarks.","keywords":["constraint satisfaction problems","regular membership constraint","deterministic finite automaton","sub-CSP substitution","constraint propagation","preprocessing","tabulation","Solitaire Battleships"],"falsifier":"Run the transformation on a benchmark suite and measure transformation time separately from search time: if any instance has transformation plus search slower than the original model, the claimed speedup fails, and the plain Regular Battleships results (average 11.6% slower) already provide such a case. Separately, enumerate all tuples accepted by the constructed DFA and compare them with the enumerated solutions of the sub-CSP; any mismatch would falsify the solution-set preservation claim.","tokens_in":7616,"feed_emoji":"🧩","tokens_out":12937,"duration_ms":109967,"temperature":0.7,"pith_summary":"Constraint satisfaction problems can be modelled in more than one way, and the chosen model decides how fast a solver finds answers. This paper proposes a preprocessing transformation: solve a small sub-CSP completely, collect all of its solution tuples, and encode that set as a deterministic finite automaton $M$; then replace the sub-CSP's constraints by the single regular membership constraint $\\mathrm{regular}(X', M)$. Because the automaton accepts exactly the tuples that satisfy the sub-CSP, the original problem's solution set is unchanged while the replacement constraint can propagate more strongly and fail earlier in search. In the Black Hole case study the regularized models found a first solution on average 82--84% faster than the original model and solved 47 of 50 instances within ten minutes instead of 7; in Solitaire Battleships plain regularization was slower, but a hybrid of regular and table constraints gave the best average improvement at 60.8%. Because the transformation happens before search, it can be combined with redundant modeling and parallel search techniques.","feed_headline":"One regular constraint replaces a solved sub-CSP to speed search","feed_subtitle":"Replacing a solved subproblem with one regular constraint keeps all solutions and cuts first-solution time by 84%.","key_machinery":"The prefix-set DFA construction: for each position $i$, the set $T_i$ contains every length-$i$ prefix of a solution, and this set of prefixes becomes the state set of the automaton together with a start state and one accepting state for full solutions. This mechanism carries the argument because the automaton accepts exactly the finite language of solution tuples, and it underlies the regular membership constraint—the constraint that a tuple of values must be a word accepted by the automaton. The regular constraint's propagation algorithm filters each variable's domain to values that can still belong to an accepted word, which is what lets the solver prune more and fail earlier than it would with the original constraints.","core_discovery":"The central discovery is that any finite set of solution tuples of a sub-CSP can be encoded exactly as the language of a DFA built directly from the tuples' prefixes. For solutions $s_1,\\dots,s_k$ over variables $x_1,\\dots,x_n$, the construction forms $T_i$, the set of all length-$i$ prefixes of solutions, and makes each prefix a state; the start state stands for the empty prefix, and a transition consumes one domain value whenever the resulting longer prefix is also present. The only accepting state represents the complete solutions. The resulting DFA accepts a word exactly when that word is one of the enumerated solution tuples, so replacing the constraints of the sub-CSP by $\\mathrm{regular}(X', M)$ preserves the solution set of the original CSP. The paper's experimental claim is that this replacement can also make search faster: in Black Hole the regularized configurations improved average first-solution time by 82.054% to 84.165%, and in Solitaire Battleships the strongest configuration combined regularized constraints with table constraints and improved average time by 60.763%.","pith_inferences":["A natural extension is to minimize the constructed DFA; standard automaton minimization could shrink the state set and make the regular constraint cheaper to propagate, an improvement the paper does not test.","The DFA size depends on the number of distinct prefixes rather than the number of full tuples, so regularization may scale better than tabulation when many solutions share long prefixes; this is consistent with the paper's closing intuition but its benchmarks do not demonstrate it.","The detection of sub-CSPs could be turned into a cost model that estimates enumeration time and automaton size against expected search savings, automating what the paper currently does with a heuristic.","The Battleships slowdown of plain Regular suggests a testable rule of thumb: regularization helps when the sub-CSP is small and its automaton stays small, and it hurts when a long variable sequence makes the automaton large or its propagation costly."],"forward_implications":["Any finite sub-CSP can be collapsed into a single regular constraint without changing the solution set of the whole CSP, making the transformation a sound preprocessing step.","Regularized models can reduce search effort: in the Black Hole benchmark, first-solution times improved by roughly 82--84% on average and 47 of 50 instances were solved within ten minutes, versus 7 for the original model.","Regularization is competitive with tabulation and the two can be mixed: on Solitaire Battleships, combining regularized counting constraints with table constraints was the best configuration, improving average first-solution time by 60.8%.","Because the substitution is a preprocessing step, it can be combined with redundant modeling, parallel search, and parallel consistency techniques without interfering with them.","The performance of the replacement depends on how the sub-CSP is chosen; plain Regular was slower on Battleships, so detecting suitable sub-CSPs is essential for the approach to pay off."],"supporting_citations":[{"why":"Supplies the weak-propagation heuristic used to detect the sub-CSPs that get replaced; the heuristic was originally designed for tabulation.","marker":"[1]"},{"why":"Gives the declarative Black Hole model used in the first case study.","marker":"[5]"},{"why":"Defines the Solitaire Battleships problem and supplies the benchmark instances used in the second case study.","marker":"[6]"},{"why":"Models the Black Hole patience game for solver comparison, providing benchmark context.","marker":"[7]"},{"why":"Provides the deterministic finite automaton definition on which the prefix-set construction rests.","marker":"[11]"},{"why":"Presents the optimized STR2 table constraint that defines the tabulation approach the paper compares against and combines with.","marker":"[12]"},{"why":"Introduces the regular language membership constraint and its filtering, the target constraint used as the replacement.","marker":"[19]"}],"fun_headline_variants":["Sub-CSP replaced by one regular constraint cuts fails","DFA from solution prefixes exactly encodes sub-CSP","Regularize sub-CSPs to speed first-solution by 84%","One regular constraint per sub-CSP speeds search","DFA encoding of sub-CSP solutions: faster solving"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The method only pays off when a sub-CSP small enough to enumerate quickly can be found automatically; the paper uses a heuristic designed for table constraints and explicitly leaves automatic detection to future work, so when no such sub-CSP exists the preprocessing cost dominates and search slows down, as happened with plain Regular on Solitaire Battleships.","fun_headline_variants_meta":{"raw":{"variants":["Sub-CSP replaced by one regular constraint cuts fails","DFA from solution prefixes exactly encodes sub-CSP","Regularize sub-CSPs to speed first-solution by 84%","One regular constraint per sub-CSP speeds search","DFA encoding of sub-CSP solutions: faster solving"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000337,"raw_usage":{"total_tokens":1830,"prompt_tokens":874,"completion_tokens":956,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":490,"completion_tokens_details":{"reasoning_tokens":875}},"tokens_in":490,"tokens_out":956,"duration_ms":8870,"temperature":1.0,"reasoning_tokens":875,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T13:00:49.506237+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the transformation on a benchmark suite and measure transformation time separately from search time: if any instance has transformation plus search slower than the original model, the claimed speedup fails, and the plain Regular Battleships results (average 11.6% slower) already provide such a case. Separately, enumerate all tuples accepted by the constructed DFA and compare them with the enumerated solutions of the sub-CSP; any mismatch would falsify the solution-set preservation claim.","supporting_citations":[{"cited_title":"In: Principles and Practice of Constraint Programming - 24th In ternational Confer- ence, CP 2018, Lille, France, August 27-31, 2018, Proceedin gs","cited_arxiv_id":null,"evidence_quote":"Supplies the weak-propagation heuristic used to detect the sub-CSPs that get replaced; the heuristic was originally designed for tabulation."},{"cited_title":"Constraints 22(4), 512–529 (2017), https://doi.org/10.1007/s10601-017-9270-5","cited_arxiv_id":null,"evidence_quote":"Gives the declarative Black Hole model used in the first case study."},{"cited_title":"http://www.csplib.org/Problems/prob014, last visited on 2019-05-07","cited_arxiv_id":null,"evidence_quote":"Defines the Solitaire Battleships problem and supplies the benchmark instances used in the second case study."},{"cited_title":"AI Communications 20(3), 211–226 (2007), http://content.iospress.com/articles/ai-communications/aic405","cited_arxiv_id":null,"evidence_quote":"Models the Black Hole patience game for solver comparison, providing benchmark context."},{"cited_title":"Con- straints 16(4), 341–371 (2011), https://doi.org/10.1007/s10601-011-9107-6","cited_arxiv_id":null,"evidence_quote":"Presents the optimized STR2 table constraint that defines the tabulation approach the paper compares against and combines with."},{"cited_title":"In: Wallace, M","cited_arxiv_id":null,"evidence_quote":"Introduces the regular language membership constraint and its filtering, the target constraint used as the replacement."}],"review_version":1}