{"id":"a361295a-77bc-43c2-a4c0-71a5d8aa61bd","arxiv_id":"2607.13344","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":4.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"EZSMTV3 is a mature SMT-translation framework for constraint answer set programming that adds weak-constraint optimization and mixed integer-real constraint support.","lead":"The paper describes EZSMTV3, a new version of a solver that turns logic programs with math constraints into questions for SMT solvers like Z3 and CVC5. It adds support for mixed integer-real constraints and optimization, and benchmarks the tool against existing constraint-answer-set solvers.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Weak-constraint optimization may not be sound for ASP-Core-2 programs: set-based cost (Def. 6) collapses duplicate labels, and the paper does not formalize GRINGO normalization or prove it preserves optimal answer sets.","rationale":"The strongest claim is that EZSMTV3 is a mature framework correctly supporting weak-constraint optimization across four CAS logics. The core completion/level-ranking translation is inherited from prior work and is not the main risk. The genuinely new and least supported part is Section 4: the semantics of weak constraints and its implementation. The paper's Definition 6 uses a set of labels, which silently changes the objective whenever two satisfied weak constraints share w@ℓ (and tuple). The paper's own Example 7 encodes W1 with duplicate -1@1 labels, and the declared optimum differs from what the ASP-Core-2 sum-over-rules semantics would select. Whether this is a bug or a deliberate deviation cannot be resolved from the paper: Proposition 2 is unproved, and the GRINGO normalization is explicitly not formalized. This is precisely the gap the reader flagged, though the reader framed it as the cardinality condition; the deeper issue is that the intended optimization semantics are ambiguous. The fix is straightforward: formalize GRINGO's weak-constraint normalization or avoid depending on it by specifying the input semantics; add a proof (or at least a differential test) that EZSMTV3's optimization answers match an independent reference. Until then, the correctness claim for the new feature should be conditional. I therefore recommend keeping the reader's CONDITIONAL verdict.","tokens_in":29144,"tokens_out":14482,"duration_ms":132037,"concrete_test":"Run EZSMTV3 on Example 7's program P1 with weak constraints W1 (bodies a, b, a,b at -1@1 and c at -2@1) using each backend. Independently compute the optimal answer sets by brute-force enumeration over the answer sets of P1 under (i) Definition 7 (set-based) and (ii) ASP-Core-2 sum-over-instances. Also run CLINGO 5.4 on the same encoding. If CLINGO reports {a,b} as optimal while EZSMTV3 reports only {c},{c,|x≥12|}, the feature is not ASP-Core-2 compliant. Broader test: random small programs with duplicate labels, compare EZSMTV3's optimal cost against CLINGO's and against brute-force enumeration.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central new feature claimed in the paper is support for weak-constraint optimization. Correctness of this feature requires that the objective minimized by EZSMTV3 after GRINGO normalization and Lierler's rewritings coincides with the optimization semantics users expect from ASP-Core-2. The paper defines weak(P,X) in Definition 6 as a set of tuples (w@ℓ,t1,...,tn), so multiple satisfied weak constraints sharing a label contribute only once. Under ASP-Core-2 (Calimeri et al. 2020b), each ground weak constraint whose body holds contributes its weight, so duplicates should sum. The divergence is visible in the paper's own Example 7: the set W1 has three weak constraints with label -1@1 on bodies a, b, and a,b. The paper declares {c} and {c,|x≥12|} optimal, whereas the standard sum-over-instances semantics ranks {a,b} (cost -3) strictly better than {c} (cost -2). The paper's bridge is Proposition 2, stated without proof, together with an unformalized assertion that GRINGO normalizes every weak-constraint program into a 'gringo o-program' with unique labels and auxiliary atoms, after which Lierler's pw-optimality-preserving rewritings are applied. The paper explicitly declines to formalize GRINGO's normalization ('Here we avoid describing formally the procedure implemented within GRINGO for \"normalizing\" optimization statements', Section 4.1). If GRINGO's grouping of duplicate labels reflects the set-based semantics rather than ASP-Core-2's per-rule semantics, then EZSMTV3's reported optimal answer sets can differ from CLINGO's on the same encodings, undermining both the correctness claim and the benchmark comparisons.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents EZSMTV3, an SMT-based constraint answer set programming framework that extends the earlier EZSMT+ system. The system uses GRINGO 5 with user-defined theory specifications for grounding, applies completion and level-ranking routines inherited from CMODELS(DIFF), translates the result into SMT-LIB, and uses CVC4/CVC5/Yices/Z3 to enumerate (extended) answer sets. The new features are support for CAS(LRA), CAS(LIRA), and CAS(IDL) languages in addition to CAS(LIA), and weak-constraint optimization. The paper defines a formal semantics for weak constraints over CAS programs, describes the implementation of the optimization interface via Lierler's w-system rewritings, and reports cumulative-time experiments on shared encodings against CLINGCON, CLINGO[LP], and CLINGO[DL].","tokens_in":29503,"tokens_out":9756,"duration_ms":119229,"significance":"If the weak-constraint issue is resolved, the paper has real value: the system and benchmarks are hosted, the encodings are shared across compared systems, no parameters are fitted to benchmark data, the architecture is modular, and the LIRA support is genuinely unique among the compared peers. The experimental presentation is honest, including the explicit admission that CLINGCON is superior on many CAS(LIA) instances. The completion/level-ranking translation builds on published, externally grounded work. However, the central new feature—weak-constraint optimization—is not yet established as sound for ASP-Core-2 programs; this is a correctness-level concern, not a presentation issue.","major_comments":[{"comment":"Definition 6 defines weak(P,X) as a set of tuples (w@ℓ,t1,...,tn), so the level cost P^X_ℓ sums the weight only once when several satisfied weak constraints carry the same (w@ℓ, terms). This is not the ASP-Core-2 semantics cited at the start of Section 4. In Example 7, W1 contains three weak constraints with weight −1@1 and no terms. Under ASP-Core-2, the answer set {a,b} satisfies all three and has level-1 cost −3, whereas {c} has cost −2 (from :∼ c. [−2@1]); thus {a,b} is the unique optimal answer set. The paper instead declares {c} and {c,|x≥12|} optimal, reflecting a set-based cost in which the three −1@1 constraints contribute once in total. If EZSMTV3 is to claim support for ASP-Core-2 weak constraints, the objective must count each grounded weak constraint whose body holds; as written, the paper defines a nonstandard optimization semantics. Please either implement and prove the st","section":"Section 4, Definition 6 and Example 7"},{"comment":"The soundness bridge for the implementation rests on two unproved assertions: (i) Proposition 2, stated without proof, and (ii) the claim that GRINGO rewrites every optimization program into a 'gringo o-program' whose weak-constraint labels are unique, after which Lierler's pw-optimality-preserving rewritings apply. The paper explicitly declines to formalize GRINGO's normalization ('Here we avoid describing formally the procedure implemented within GRINGO for \"normalizing\" optimization statements'). The illustrative rewriting of W1 in Section 4.1 merges the three weak constraints :∼ a, :∼ b, :∼ a,b into a single auxiliary rule aux1 plus :∼ aux1 [−1@1]; this is precisely the step that changes the objective from the sum over satisfied weak constraints to an indicator. Without a formal description of GRINGO's actual behavior (or a direct proof that it preserves ASP-Core-2 costs), Propositio","section":"Section 4.1, Proposition 2 and the GRINGO normalization claim"},{"comment":"Example 9 shows that for W1 the optimal and pw-optimal answer sets differ: the set-based optimal is {c}, while the pw-optimal is {a,b}. This is exactly the difference between Definition 6 and the standard per-instance sum semantics. The paper's subsequent claim that 'any gringo o-program satisfies the if-condition of Proposition 2' is therefore the load-bearing step, but it is asserted rather than proved. Even if the reader accepts Lierler's rewritings as preserving pw-optimality, the leap to Definition-6-optimality for the original program depends entirely on the unformalized GRINGO normalization. The manuscript should either state clearly that EZSMTV3 optimizes a set-based objective, or supply the missing equivalence proof.","section":"Section 4.1, Example 9 and the optimal vs pw-optimal distinction"}],"minor_comments":[{"comment":"The line 'Lines 30-35 are due to Line 12 in Listing 3...' is repeated twice verbatim. The second occurrence should be deleted or replaced with the intended explanation.","section":"Section 3.1.2, bullet list"},{"comment":"The text reads 'EZSMT V ersion 3' instead of 'EZSMT Version 3'; also the paper title on page 1 says 'EZSMT Version 3, Matured' while the body sometimes uses 'EZSMTV 3'. Please standardize the typography.","section":"Section 3, first sentence"},{"comment":"Calimeri et al. 2020a and 2020b are the same paper listed twice with different publication years/pages. Please consolidate to a single reference and use consistent citation keys.","section":"References"},{"comment":"The notation for unsolved instances is ambiguous in some rows, e.g., 'E(YICES) 592.44 (100)' in Figure 7. If the parenthetical numbers are timeouts, the cumulative time should be much larger; if they denote something else (e.g., number of instances), please state this explicitly and clarify whether timeout instances contribute to the cumulative time.","section":"Section 5, Figures 5-8"},{"comment":"The paper says 'all encodings used were identical for all systems involved' but later states that encodings were 'augmented with additional domain restrictions.' Please clarify that the shared encodings are identical only after the augmentation, and specify which systems used the augmented versions.","section":"Section 5, paragraph 1"}],"recommendation":"major_revision","confidential_remarks":"The weak-constraint semantics concern is substantive and should be resolved before publication. I would ask the authors to either align the implementation with ASP-Core-2's sum-over-instances semantics or clearly scope the paper as presenting a nonstandard set-based optimization objective, and to provide a formal proof or a direct semantic verification of the GRINGO normalization step. The rest of the paper, especially the modular architecture and shared-encoding benchmarks, is suitable for a TPLP system description once this correctness issue is addressed."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Read EZSMTV3. The core is a real, working artifact: GRINGO 5 front-end, completion and level ranking from CMODELS(DIFF), translation to SMT-LIB, four SMT backends, and LIRA support. The architecture is clearly described, the shared-encoding benchmarks are a plus, and the system plausibly does what it says. LIRA support is genuinely new relative to EZSMT+ and peers. The weak-constraint section has a load-bearing problem. Definition 6 makes weak(P,X) a set of tuples, so duplicate labels collapse. ASP-Core-2 sums each ground weak rule whose body holds. Example 7 shows the collision: standard reading gives {a,b} cost -3 and {c} cost -2, so {a,b} is the unique optimum; the paper declares {c} and {c,|x>=12|} optimal. The bridge is Proposition 2, stated without proof, plus an unformalized claim about GRINGO normalization. The paper explicitly declines to formalize that normalization. If GRINGO groups duplicate labels or introduces auxiliaries as sketched for W1, the minimized objective diverges from ASP-Core-2. This is not minor; it affects the soundness of the new optimization feature. The core translation is likely sound because it rests on published completion and level-ranking results. Benchmarks are okay but not strong: cumulative times only, no per-instance variance, no commit hash or full reproduction script. That is minor compared with the semantics issue. Overall, this is a solid system paper with one broken part. I would send it to peer review. A serious referee can separate the system work from the optimization semantics. The authors need to either prove that GRINGO normalization preserves ASP-Core-2 optimal answer sets with duplicate labels, or weaken their claim and fix Example 7. If not, EZSMTV3's optimization mode is only correct for the pw-style objective with unique identifiers, which is not what the paper promises. For a reading group, it is worth a session to debate the semantics. I would not cite it until corrected.","headline":"A real system artifact with a genuine hole: the weak-constraint semantics diverge from ASP-Core-2 when duplicate labels collapse, so the optimization feature needs proof or a fix before the paper can be trusted.","tokens_in":772,"tokens_out":1382,"would_cite":false,"duration_ms":48648,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68T27","68N17"],"pacs":[],"model":"deepseek-v4-flash","headline":"EZSMTV3 claims that constraint answer-set programs in four arithmetic logics — LIA, LRA, LIRA, and IDL — can be solved by grounding them, computing completion and level rankings, translating to SMT-LIB, and letting off-the-shelf SMT solvers","keywords":["constraint answer set programming","satisfiability modulo theories","answer set programming","weak constraints","level ranking","SMT-LIB","mixed integer-real arithmetic","EZSMT"],"falsifier":"Take the o-program (P1, W1) from Example 7, whose true optimal answer sets are {c} and {c, |x ≥ 12|}, and run EZSMTV3 with weak constraints on it. If the system returns {a, b} — the unique pw-optimal answer set — as optimal, then GRINGO's normalization plus the w-system rewriting has changed the optimization semantics. More generally, brute-force enumerate optimal answer sets for all gringo o-programs up to a few atoms and compare with EZSMTV3's answers; the first mismatch refutes the optimization claim.","tokens_in":29009,"feed_emoji":"🧩","tokens_out":6085,"duration_ms":83774,"temperature":0.7,"pith_summary":"This paper claims that constraint answer set programming has reached the point where a single extensible system can serve four constraint logics — linear integer arithmetic, linear real arithmetic, mixed integer-real arithmetic, and integer difference logic — without writing a custom search engine for any of them. The recipe: ground a CAS program with a grammar-extensible grounder, build the program's completion and, for non-tight programs, level-ranking formulas, translate the result into SMT-LIB, and hand it to an off-the-shelf SMT solver. The new piece relative to earlier EZSMT systems is optimization: weak constraints in the ASP-Core-2 style are rewritten into a single integer objective variable and solved by repeated incremental 'seek a smaller value' assertions. Benchmarks on encodings shared verbatim with CLINGCON, CLINGO[LP], and CLINGO[DL] place the resulting solvers in the same performance ballpark, and the LIRA mode handles constraints on both integers and reals that none of those peers supports.","feed_headline":"One translation pipeline, four constraint logics, SMT solvers do the search","feed_subtitle":"The framework adds weak-constraint optimization and mixed integer-real constraints, going beyond what CLINGCON, CLINGO[LP], and CLINGO[DL] c","key_machinery":"The load-bearing device is the completion-and-level-ranking translation: completion turns a CAS program into an SMT formula whose models over-approximate its answer sets, and, for non-tight programs, integer level-ranking atoms of the form |lr_a − lr_b ≥ 1| cut the over-approximation back to the true answer sets. Around that core, EZSMTV3 wraps a GRINGO-5 #theory grammar for each supported logic, an ASPIF reader with type assignment for integer versus real variables, and a solver interface that emits SMT-LIB and uses incremental solving to enumerate multiple (extended) answer sets. For optimization, the new mechanism is the weak-constraint rewriting: after grounding, each weak constraint bec","core_discovery":"The central claim is that the translational approach to CASP can act as a maturation framework: EZSMTV3 is a multi-stage pipeline — GRINGO 5 grounding under per-logic #theory grammars, ASPIF parsing, completion and level ranking, SMT-LIB emission, incremental SMT solving — that supports tight and non-tight programs in CAS(LIA), CAS(LRA), CAS(LIRA), and CAS(IDL). The system further claims that ASP-Core-2 weak constraints can be added to this pipeline soundly: after GRINGO normalizes weak constraints to a simpler gringo o-program form, w-system rewritings — positive-weight normalization, per-level rescaling, and collapse to level 1 — preserve pw-optimal answer sets, and by Proposition 2 these","pith_inferences":["If the pipeline is as modular as claimed, the natural next step is to treat CASP as a logic-programming front-end to SMT-LIB: new theories such as arrays, bit-vectors, or strings would enter by adding a GRINGO #theory block and small reader and type-handling rules, not by writing a solver.","The unformalized GRINGO normalization of weak constraints is where the optimization correctness argument has a gap; a formal specification of that normalization, or a brute-force differential test over thousands of small o-programs, would close or refute it.","The experimental gap between CLINGCON on LIA and EZSMTV3 suggests the next performance leap lies in translating aggregate expressions such as #sum more cleverly, not in making the completion-to-SMT translation faster.","Because the same encoding can be handed to four different SMT solvers, per-instance solver selection or portfolio solving is a cheap robustness improvement; the reported data already show CVC4 and CVC5 beating Z3 on LIRA and Yices leading on some IDL runs."],"forward_implications":["Any improvement in SMT solving for QF_LIA, QF_LRA, QF_IDL, or AUFLIRA becomes an improvement in EZSMTV3 automatically, since the interface is standard SMT-LIB.","Programs written for EZSMTV3's CAS(LIA) fragment can also be run by CLINGCON, and the CAS(LRA) and CAS(IDL) fragments align with CLINGO[LP] and CLINGO[DL], so shared encodings permit direct cross-system comparison.","Weak-constraint optimization extends the framework to minimization and maximization problems, and the anytime behavior means a user can interrupt and keep the best answer set found so far.","Non-tight programs are handled through configurable level-ranking schemes and upper bounds, giving users a trade-off between formula size and solving difficulty.","The LIRA mode lets one encoding mix integer and real decision variables, opening domains such as hybrid planning to declarative CASP modeling without a dedicated solver."],"fun_headline_variants":["EZSMTV3: One pipeline, four logics, SMT solvers for search","Translational CASP matured: EZSMTV3 adds weak constraints and mixed reals","EZSMTV3: Sound weak-constraint optimization across four SMT-backed logics","From grounding to SMT: EZSMTV3 unifies CASP with weak constraints","EZSMTV3: Translational CASP with optimization and mixed integer-real domains"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"Optimization correctness rests on two unproved links: Proposition 2's condition that the set of weak-constraint tuples has the same cardinality as the weak-constraint set, and the claim that GRINGO's normalization of weak constraints produces gringo o-programs for which that condition and the w-system rewritings preserve optimal answer sets; if GRINGO introduces duplicate tuples or auxiliary atoms in a way that violates this, EZSMTV3's 'optimal' answer sets could be merely pw","fun_headline_variants_meta":{"raw":{"variants":["EZSMTV3: One pipeline, four logics, SMT solvers for search","Translational CASP matured: EZSMTV3 adds weak constraints and mixed reals","EZSMTV3: Sound weak-constraint optimization across four SMT-backed logics","From grounding to SMT: EZSMTV3 unifies CASP with weak constraints","EZSMTV3: Translational CASP with optimization and mixed integer-real domains"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000262,"raw_usage":{"total_tokens":1443,"prompt_tokens":765,"completion_tokens":678,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":509,"completion_tokens_details":{"reasoning_tokens":561}},"tokens_in":509,"tokens_out":678,"duration_ms":6641,"temperature":1.0,"reasoning_tokens":561,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-02T05:26:50.893442+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take the o-program (P1, W1) from Example 7, whose true optimal answer sets are {c} and {c, |x ≥ 12|}, and run EZSMTV3 with weak constraints on it. If the system returns {a, b} — the unique pw-optimal answer set — as optimal, then GRINGO's normalization plus the w-system rewriting has changed the optimization semantics. More generally, brute-force enumerate optimal answer sets for all gringo o-programs up to a few atoms and compare with EZSMTV3's answers; the first mismatch refutes the optimization claim.","supporting_citations":[],"review_version":1}