{"id":"0cd0cad6-4e40-4eab-bb89-ba23acb95d56","arxiv_id":"2607.06446","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"unknown","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper defines FO Cost-Value Decision for token-sliding discovery and proves FPT and W[1]-hardness results for Partial Vertex Cover Discovery across various graph classes.","lead":"This paper introduces a framework for optimization in the token-sliding model, where tokens are moved on a graph to satisfy a value condition defined by first-order logic. It applies this to Partial Vertex Cover Discovery, yielding new tractability and hardness results.","discovery_kind":"unclear","skeptic_critique":{"model":"glm-5.2","headline":"No significant objection identified. Lemma 33's proof citation is imprecise but the result holds via FO model checking + DP, and the main applications do not depend on it.","rationale":"The reader correctly identifies the anchored distance independence assumption as a point worth scrutinizing, but overstates its load-bearing nature. Tracing the dependency graph: Theorem 9 (locally bounded cliquewidth) uses Lemma 31, which follows from Lemma 30 and standard FO model checking—no dependence on Lemma 33. Theorem 10 (existential FO Cost-Value Decision on monadically stable classes) uses quasi-bounded-size bounded-shrubdepth decompositions and Lemma 26—again no dependence on Lemma 33. Since Partial Vertex Cover Discovery is a quantifier-free special case, its tractability on both locally bounded cliquewidth and monadically stable classes follows from Theorems 9 and 10 directly. Lemma 33 is only used in Theorem 11 (Boolean FO Discovery on monadically stable classes) and Lemma 28 (which feeds Theorem 7, full FO Cost-Value Decision on locally structurally bounded expansion). These are secondary results. The imprecision in Lemma 33's proof—citing Theorem 10 when the correct argument is FO model checking + DP—is a real but minor issue. The result itself is correct: FO model checking on monadically stable classes is FPT (Dreier et al. [7, 9]), and the DP for cost-profit optimization over a polynomially-bounded budget is standard. Remark 5 informally describes this correct approach. The proof of Theorem 6 itself is careful: the Gaifman locality decomposition, the coarsening argument, the protection conditions, and the soundness/completeness proofs all check out. The number of enumerated cases (H, τ, ℓ, F) depends only on k and the value expression, ensuring FPT. The hardness results (Theorems 13, 17, 18) use standard reductions and appear correct. The d-degenerate algorithm (Theorem 12) correctly adapts the universal-set technique of Panolan et al. Overall, the paper makes a solid contribution. The ACCEPT verdict is appropriate.","tokens_in":27743,"tokens_out":14708,"duration_ms":588030,"concrete_test":"Verify Lemma 33 independently: on a monadically stable class C with FPT FO model checking, construct an explicit algorithm for anchored weighted multicolored distance-r independence that (1) uses FO model checking to enumerate feasible anchor-distance patterns and (2) uses standard DP over the polynomially-bounded budget to select optimal (cost, profit) pairs per anchor. If this two-step algorithm runs in f(p,r)·n^{O(1)} time, Lemma 33 holds without invoking Theorem 10.","verdict_should_be":"UNCHANGED","load_bearing_attack":"After tracing the dependency graph carefully, I do not find a significant load-bearing concern. The paper's central meta-theorem (Theorem 6) is proved via a careful Gaifman-locality decomposition with sound and complete reduction to two assumed ingredients. Those ingredients are verified for the target graph classes: locally structurally bounded expansion (Corollary 27 + Lemma 28), locally bounded cliquewidth (Lemma 30 + Lemma 31), and monadically stable classes (Theorem 10 + Lemma 33). The reader flags the anchored weighted multicolored distance-r independence assumption (Definition 4 / Lemma 33) as the weakest premise. I examined this and found a minor imprecision but not a correctness gap. Lemma 33's proof states 'It follows from Theorem 10, since the multicolored distance-r independence condition is FO definable.' However, the anchored version has candidates that are abstract objects (triples (C, a, q') in the proof of Theorem 6) with an anchor map to V(G), and a single anchor vertex can host multiple candidates with different (cost, profit) pairs. This means the problem does not directly reduce to an existential FO Cost-Value Decision instance on G, because FO Cost-Value Decision assumes a single unary cost and value per vertex per coordinate. The correct approach—described informally in Remark 5—is to use FO model checking on G to select anchor vertices satisfying the pairwise distance constraint, then handle the cost-profit selection among candidates sharing an anchor via standard DP (multiple-choice knapsack, solvable in polynomial time since the budget is unary-bounded). This uses FO model checking + DP, not Theorem 10. The result is correct; the citation is imprecise. Crucially, this imprecision is not load-bearing for the paper's headline applications. Partial Vertex Cover Discovery on locally bounded cliquewidth follows from Theorem 9 (which uses Lemma 31, independent of Lemma 33). Partial Vertex Cover Discovery on monadically stable classes follows from","agreement_with_reader":"partial"},"referee_report":{"model":"glm-5.2","summary":"This paper introduces FO Cost-Value Decision, a logical optimization framework that extends Boolean FO solution discovery to quantitative objectives where the value of a selected tuple is given by unary vertex weights plus first-order definable correction terms. The framework is motivated by and applied to Partial Vertex Cover Discovery, where the covered-edge count decomposes as a sum of degrees minus an adjacency-pattern correction. The central result is a conditional meta-theorem (Theorem 6) reducing FPT tractability of FO Cost-Value Decision to two ingredients: efficient Local FO Cost-Value Decision and efficient anchored weighted multicolored distance-r independence. The authors verify these ingredients on several graph classes (locally structurally bounded expansion, locally bounded cliquewidth, monadically stable), yielding FPT results for Partial Vertex Cover Discovery. The paper also proves W[1]-hardness for Partial Vertex Cover Discovery parameterized by k+b, NP-hardness and W[1]-hardness for Vertex Cover Discovery on planar graphs and with respect to cutwidth and clique cover number, and gives a dedicated FPT algorithm on d-degenerate graphs parameterized by k+d.","tokens_in":28641,"tokens_out":1300,"duration_ms":308188,"significance":"The paper makes a solid contribution by identifying and formalizing a natural quantitative gap in the solution discovery framework: many discovery objectives (exemplified by Partial Vertex Cover) involve correction terms that are not purely unary but depend on the adjacency pattern of the selected tuple. The FO Cost-Value Decision framework captures this cleanly, and the meta-theorem (Theorem 6) is a well-structured reduction to two algorithmic ingredients that are then verified on standard graph classes. The hardness results are explicit and cover complementary parameters. The FPT algorithm for d-degenerate graphs (Theorem 12) via universal sets is a nice self-contained result. The proofs build on established model-checking machinery (Gaifman locality via Theorem 19, LinEMSOL, aggregate queries on bounded expansion, monadic stability decompositions) and the reductions are traced carefully. The paper provides falsifiable complexity-theoretic predictions and the main meta-theorem is stated with clearly identified assumptions.","major_comments":[{"comment":"The proof states: 'It follows from Theorem 10, since the multicolored distance-r independence condition is FO definable.' However, the anchored version (Definition 4) has candidates that are abstract objects (triples (C, a, q') in the proof of Theorem 6) with an anchor map to V(G), and a single anchor vertex can host multiple candidates with different (cost, profit) pairs. This means the problem does not directly reduce to an existential FO Cost-Value Decision instance on G, because FO Cost-Value Decision assumes a single unary cost and value per vertex per coordinate. The correct approach—described informally in Remark 5—is to use FO model checking on G to select anchor vertices satisfying the pairwise distance constraint, then handle the cost-profit selection among candidates sharing an anchor via dynamic programming. The remark sketches this but the lemma does not formalize it. Since:","section":"Lemma 33 (p. 24)"}],"minor_comments":[{"comment":"The dependency on the meta-theorem of Grobler et al. [14] for the unary-weighted FO Value Discovery subproblem is stated without elaboration. A one-sentence explanation of how the Group Knapsack reduction works in the discovery setting would help the reader.","section":"Theorem 12 (p. 8)"},{"comment":"The reduction from Circulating Orientation to Vertex Cover Discovery is intricate. The budget-tightness argument (p. 11, 'Any moving pattern besides the one described above will take an additional step') is stated somewhat informally. A brief remark formalizing why no alternative filling pattern can stay within budget would strengthen the proof.","section":"Section 3.2 (p. 9–12)"},{"comment":"The figure caption and the text reference vertices 'ce' and 'de' in the cycle description ('edges {pe_1, qe_1} and {ce_{w(e)}, de_{w(e)}}'), but ce and de are not defined in the construction. These appear to be a typo for pe and qe.","section":"Figure 1 (p. 10)"},{"comment":"The statement 'Classes of locally structurally bounded expansion are monadically stable' is used to defer to Lemma 33. A brief justification or citation for this containment would be helpful, as it is not immediate to all readers.","section":"Lemma 28 (p. 21)"},{"comment":"The theorem is labeled 'Algorithmic version of [13]' but the text explains that the algorithmicity requires substituting ingredients from [7] and [13] into the decomposition construction of [2]. The reader would benefit from a sentence clarifying whether this substitution is routine or whether additional work is needed.","section":"Theorem 32 (p. 23–24)"},{"comment":"The partition assumption on the formulas φ_1,...,φ_m is stated as 'notational only' via refinement into the Boolean partition. It would help to note that m can be exponential in k and the formula size, and that this is absorbed into the parameter.","section":"Definition 1 (p. 2)"},{"comment":"The paper uses 'efficient' as a prefix for several properties (Definitions 3, 4, 22) to mean 'fixed-parameter tractable.' A footnote or remark clarifying this convention on first use would help.","section":"General"},{"comment":"These are identical citations (Gajarský et al., ACM TOCL 2020). One should be removed.","section":"References [11] and [12]"}],"recommendation":"minor_revision","confidential_remarks":"The reader's report and stress-test note both flag Lemma 33 as the weakest load-bearing point. I agree this is a genuine gap in the proof, but it is a gap in exposition rather than a correctness error: the approach described in Remark 5 is standard and the result follows from known FO model-checking machinery on monadically stable classes plus DP. The fix is to expand the lemma proof to formalize the two-step reduction. This is local and does not require new ideas, so minor revision is appropriate. The paper is otherwise well-structured and the central meta-theorem is sound."},"author_rebuttal":{"model":"glm-5.2","summary":"We thank the referee for the careful reading and the constructive assessment. The referee raises one major comment concerning the proof of Lemma 33, which correctly identifies a gap between the one-line argument currently in the manuscript and the actual algorithmic content needed. We agree with the referee's observation and will revise the lemma accordingly.","responses":[{"response":"The referee is correct. The one-line proof of Lemma 33 is insufficient as written. The issue is precisely the one identified: the anchored problem (Definition 4) has abstract candidate objects (triples (C, a, q') in the proof of Theorem 6) that do not correspond one-to-one with vertices of G, so the problem does not reduce directly to an existential FO Cost-Value Decision instance on G. The reduction described informally in Remark 5—adding unary predicates to G recording which candidates may use a given vertex as their anchor, together with the relevant local cost and profit information, then using FO model checking to select anchors satisfying the pairwise distance constraint, and finally handling the cost-profit bookkeeping among candidates sharing an anchor via dynamic programming—is the correct approach. We will revise Lemma 33 to formalize this two-step argument explicitly: (1) FO model checking on the monadically stable class (preserved under the bounded unary expansion recording candidate information) selects anchor vertices satisfying the pairwise distance-r constraint; (2) since the budget B is polynomially bounded and the number of colors p is a parameter, the cost-profit selection among candidates sharing an anchor is handled by standard dynamic programming. We note that this does not change any of the results that depend on Lemma 33 (Theorem 11, Lemma 28, and the consequent Theorems 7 and 9), as the algorithmic content is exactly that sketched in Remark 5; it only formalizes what the lemma currently leaves implicit.","revision_made":"yes","referee_comment":"[Lemma 33 (p. 24)] The proof states: 'It follows from Theorem 10, since the multicolored distance-r independence condition is FO definable.' However, the anchored version (Definition 4) has candidates that are abstract objects (triples (C, a, q') in the proof of Theorem 6) with an anchor map to V(G), and a single anchor vertex can host multiple candidates with different (cost, profit) pairs. This means the problem does not directly reduce to an existential FO Cost-Value Decision instance on G, because FO Cost-Value Decision assumes a single unary cost and value per vertex per coordinate. The correct approach—described informally in Remark 5—is to use FO model checking on G to select anchor vertices satisfying the pairwise distance constraint, then handle the cost-profit selection among candidates sharing an anchor via dynamic programming. The remark sketches this but the lemma does not. "}],"tokens_in":27669,"tokens_out":592,"duration_ms":152956,"standing_objections":[]},"desk_editor":{"model":"glm-5.2","letter":"This paper does two things worth your attention. First, it introduces FO Cost-Value Decision, a framework that extends Boolean solution discovery to optimization objectives where the value of a selected tuple is a sum of unary vertex weights plus FO-definable correction terms. The motivating example—Partial Vertex Cover Discovery, where edges with both endpoints selected must be subtracted—is natural and well-chosen. Second, it proves a set of dedicated hardness and tractability results for Partial Vertex Cover Discovery and Vertex Cover Discovery that go beyond what the framework alone gives you. Both halves deliver. The framework itself is, as the authors frankly state, a conceptual extension of standard Gaifman-locality-based model checking with an optimization layer bolted on. That honesty is appropriate. The meta-theorem (Theorem 6) reduces to two algorithmic ingredients—local FO cost-value decision and anchored weighted multicolored distance independence—and then verifies these ingredients on several graph classes. The verification for locally structurally bounded expansion (via the efficient reversal theorem and aggregate-query machinery) and for bounded cliquewidth (via LinEMSOL) is clean and correct. The dedicated results are where the paper earns extra credit. The d-degenerate algorithm (Theorem 12) adapts the universal-set covering argument of Panolan et al. in a tidy way. The hardness reductions are explicit and non-trivial: the Circulating Orientation reduction giving NP-hardness on planar graphs and W[1]-hardness for cutwidth is carefully constructed, and the clique-cover-number hardness is a clean reduction from Multicolored Independent Set. One soft spot: Lemma 33, which establishes anchored weighted multicolored distance-r independence on monadically stable classes, cites Theorem 10 as justification. But the anchored version has abstract candidates with anchor maps to V(G), so it doesn't directly reduce to an existential FO Cost-Value Decision instance. The fix—use FO model checking to select anchors satisfying the distance constraint, then handle cost-profit selection via standard DP—is described informally in Remark 5 and is straightforward. The result is correct; the citation is just imprecise. This matters for Theorem 11 (Boolean FO Discovery on monadically stable classes) but does not affect Theorems 7 or 9, which are the headline tractability results for Partial Vertex Cover Discovery. The paper is for researchers in parameterized complexity and algorithmic graph theory who work with model-checking meta-theorems. It deserves a serious referee. The framework is a genuine organizational contribution, the hardness results are solid, and the one proof imprecision is minor and fixable.","headline":"Solid paper introducing a clean optimization framework for solution discovery with concrete hardness results; one minor proof imprecision that doesn't undermine the main theorems.","tokens_in":28554,"tokens_out":1199,"would_cite":true,"duration_ms":83706,"reading_group":"no","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"glm-5.2","headline":"Moving tokens to cover edges: a logical framework for optimization under a movement budget","keywords":["solution discovery","token sliding","partial vertex cover","first-order logic","parameterized complexity","graph classes","fixed-parameter tractability","meta-theorem"],"falsifier":"Exhibit a graph class of locally bounded cliquewidth (or a monadically stable class) on which the anchored weighted multicolored distance-r independence problem is W[1]-hard, which would collapse the meta-theorem's applicability to that class.","tokens_in":27930,"feed_emoji":"","tokens_out":1289,"duration_ms":183766,"temperature":0.7,"pith_summary":"The paper introduces FO Cost-Value Decision, a framework that extends first-order logic model-checking to handle quantitative optimization: vertices carry both costs and values, and first-order formulas define correction terms that adjust the value of a selected tuple based on structural patterns (such as adjacency between chosen vertices). The motivating application is Partial Vertex Cover Discovery, where k tokens start at initial positions on a graph and must be slid within a movement budget b to cover at least t edges; the edge-counting objective is inherently non-additive because edges with both endpoints selected are double-counted. The central meta-theorem (Theorem 6) shows that FO Cost-Value Decision is fixed-parameter tractable on any graph class satisfying two conditions: efficient local FO cost-value decision (solving the problem within bounded-radius neighborhoods) and efficient anchored weighted multicolored distance independence (a packing problem that selects far-apart local candidates while respecting cost and value bounds). The authors verify these two conditions for classes of locally structurally bounded expansion, locally bounded cliquewidth, and, for the existential fragment, monadically stable classes. As a consequence, Partial Vertex Cover Discovery is FPT on all these graph classes, parameterized by the number of tokens k. The paper also establishes hardness boundaries: Partial Vertex Cover Discovery is W[1]-hard parameterized by k+b (so the movement budget alone does not help), and Vertex Cover Discovery is NP-hard on planar graphs and W[1]-hard parameterized by cutwidth or clique cover number. A dedicated FPT algorithm for Partial Vertex Cover Discovery on d-degenerate graphs parameterized by k+d is also given, using universal-set splitters to reduce to a group knapsack problem.","feed_headline":"Tokens, costs, and logic: FPT optimization for partial vertex cover discovery","feed_subtitle":"A first-order framework with FO-definable correction terms yields tractability on sparse and dense graph classes, while hardness persists on","key_machinery":"FO Cost-Value Decision framework; anchored weighted multicolored distance-r independence; Gaifman locality decomposition; universal-set splitters for degenerate graphs; LinEMSOL optimization on bounded cliquewidth; quasi-bounded-size bounded-shrubdepth decompositions for monadically stable classes","core_discovery":"The paper identifies that quantitative discovery problems with non-additive objectives—where the value of a selected vertex set depends on structural patterns among the chosen vertices, not just per-vertex weights—can be captured by first-order value expressions combining unary weights with FO-definable correction terms. The key algorithmic insight is that Gaifman locality for first-order logic decomposes any such optimization into local computations on bounded-radius neighborhoods, followed by a global packing step (anchored weighted multicolored distance independence) that selects mutually far-apart local candidates while aggregating their costs and values. This two-ingredient recipe is a ","pith_inferences":["If full FO Cost-Value Decision is eventually proven FPT on monadically stable classes (as the authors expect), the existential-fragment restriction in Theorem 10 would become unnecessary, unifying all the monadic-stability results.","The anchored distance-independence formulation is strictly weaker than full FO model-checking, so the meta-theorem could in principle yield tractability on classes where full model-checking is hard, provided the packing problem remains tractable—a direction the authors note but do not exploit.","The universal-set technique for d-degenerate graphs suggests that similar derandomization or covering arguments could yield dedicated FPT algorithms for other non-additive discovery problems on sparse graphs without invoking the full logical machinery.","The NP-hardness on planar graphs for Vertex Cover Discovery, combined with FPT on bounded-treewidth classes, implies that the problem's hardness is tied to planar graph structure in a way that standard sparsity-based meta-theorems do not resolve."],"forward_implications":["Any graph class where local FO model-checking and distance-based packing are both tractable inherits FPT for weighted FO optimization with correction terms, providing a template for extending logical meta-theorems beyond Boolean feasibility to quantitative objectives.","Partial Vertex Cover Discovery is tractable on common sparse and dense graph classes (bounded expansion, bounded cliquewidth, monadically stable) parameterized only by the number of tokens, making it accessible on graphs where the general k+b parameterization is W[1]-hard.","The separation between W[1]-hardness for k+b and FPT for k on structurally restricted classes clarifies that graph structure, not movement budget size, is the algorithmic lever for discovery problems.","The framework can model discovery variants of any problem whose objective decomposes as a sum of unary vertex weights plus an FO-definable correction, including problems beyond vertex cover such as dominating-set-quality or budgeted subgraph optimization."],"fun_headline_variants":["A first-order framework for partial vertex cover discovery","Non-additive optimization in token sliding via FO logic","Local logic and global packing for FO value discovery","FO-definable correction terms for vertex cover discovery","Capturing non-additive vertex weights in solution discovery"],"cache_read_input_tokens":0,"weakest_assumption_plain":"The meta-theorem's tractability depends on the anchored weighted multicolored distance-r independence problem being FPT on the target graph classes. The paper treats this as a mild extension of ordinary distance-based packing and argues it reduces to standard FO model-checking machinery, but if this reduction is more delicate than claimed—or fails on the classes at the boundary such as monadically stable graphs—the main tractability results would not hold.","fun_headline_variants_meta":{"raw":{"variants":["A first-order framework for partial vertex cover discovery","Non-additive optimization in token sliding via FO logic","Local logic and global packing for FO value discovery","FO-definable correction terms for vertex cover discovery","Capturing non-additive vertex weights in solution discovery","Parameterized complexity of partial vertex cover discovery"]},"model":"glm-5.2","effort":"high","cost_usd":0.0,"raw_usage":{"total_tokens":1408,"prompt_tokens":676,"completion_tokens":732,"prompt_tokens_details":null},"tokens_in":676,"tokens_out":732,"duration_ms":44023,"temperature":1.0,"reasoning_tokens":695,"cache_read_input_tokens":0,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-08T05:30:36.776112+00:00","model_set":{"reader":"glm-5.2"},"falsifier":"Exhibit a graph class of locally bounded cliquewidth (or a monadically stable class) on which the anchored weighted multicolored distance-r independence problem is W[1]-hard, which would collapse the meta-theorem's applicability to that class.","supporting_citations":[],"review_version":1}