{"id":"f7cb5d13-2436-4fe0-ba89-7a56bf972ced","arxiv_id":"2506.14713","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Linear Planar 3-SAT is NP-complete, its reconfiguration is PSPACE-complete, and these results imply NP-completeness of bounded 2D connected multi-agent pathfinding and PSPACE-completeness of the unbounded version.","lead":"This paper defines two new restricted versions of Boolean satisfiability, linear planar 3-SAT, and proves their satisfiability and reconfiguration problems are NP-complete and PSPACE-complete respectively. It uses these fragments to prove that connected multi-agent pathfinding on a 2D grid is PSPACE-complete and that the bounded version is NP-complete.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Claim 8.10(2) asserts without proof that every variable-set configuration is reachable from the initial bridge-line configuration; Claim 8.12 depends on this to simulate flips, so PSPACE-hardness has an unproved gap.","rationale":"The reader's weakest_assumption identifies exactly the gap I find most load-bearing. The proof of Claim 8.10(2) asserts without proof that arbitrary variable-set configurations are reachable from the initial line configuration; since Claim 8.12's forward direction invokes Point 2 at each step from the current configuration, this is not a cosmetic omission. If Point 2 is false even for n = 3, the bridge gadgets do not confine flips as required and the PSPACE reduction collapses; if it is true, a short reachability proof or an exhaustive BFS verification should be added. I do not see a more serious issue elsewhere: the cycle-augmentation section is elaborate and the kite-graph arguments are mostly self-contained, and I agree with the reader that the definitional glitches around G_lit are secondary. The appropriate verdict is unchanged from the reader's: CONDITIONAL pending the missing proof.","tokens_in":36986,"tokens_out":6066,"duration_ms":62617,"concrete_test":"Restrict to the bridge line of Figure 24 for n = 3 and n = 4 variables. Model the subproblem with agent set A = {b_alpha} union {a_x, b_x}_{x in V\\{alpha}} and the 2n-2 isolated requesters. A state is an assignment of each agent in A to a cell of the line (next to a requester or in the unique free slot) that keeps all requesters connected, with variable agents not in the middle. Build the full state graph under the exact CMAPF transition rule (simultaneous one-step moves of agents in A, including the no-swap condition). For every state c and every i in A, check whether there is a path from c to a state in which i is the unique free agent. If every check passes, Claim 8.10(2) survives this test; if some (c, i) fails, the claim is false as stated and the reduction needs a different bridge design or a corrected invariant.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The weakest point is Claim 8.10(2), used in the forward direction of Claim 8.12. To simulate a flip of variable x, the proof must, from the current configuration after previous flips, move agents in A\\{b_x} so that b_x becomes free. The proof of Claim 8.10(2) first gives a procedure from the initial configuration of Figure 24, then concludes: 'We proved that c can be reached from the initial configuration. As movements in CMAPF are reversible, the initial configuration is reachable from c. Thus, we can obtain a configuration where i is free to move from c.' But no proof is given that every all-variables-set configuration c is reachable from the initial configuration, and that reachability is exactly what the simulation requires. The line of A agents with 2|V|-1 agents and 2|V|-2 isolated requesters is not trivially connected: in any configuration all but one agent may be pinned next to a requester, and the free agent's movement options are constrained by the grid and by the connectivity requirement. Showing that the unique free slot can be routed from an arbitrary state to any chosen agent i requires an invariant or a state-space argument, not a one-line assertion. Without Point 2 holding for arbitrary c, the claimed equivalence in Claim 8.12 between grid executions and variable-flip sequences is unsupported, so the PSPACE-hardness of 2D CMAPF in Theorem 8.8 rests on an unproved claim. This is fixable: a rigorous proof that all variable-set configurations of the bridge line are mutually reachable would complete the argument.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces two new fragments of 3-SAT, Linear Planar 3-SAT and Linear Literal-Planar 3-SAT, and proves that the satisfiability problems for both fragments are NP-complete. It then proves PSPACE-completeness for the corresponding reconfiguration problems, via reductions from NCL and from known planar 3-SAT reconfiguration results, using a new theory of planar cycle augmentation and dually connected matchings. The main applications are complexity classifications of Connected Multi-Agent Pathfinding on two-dimensional grids: Bounded 2D CMAPF is claimed NP-complete even with bound 2 and radius 1, and unbounded 2D CMAPF is claimed PSPACE-complete.","tokens_in":37308,"tokens_out":7572,"duration_ms":74373,"significance":"If the proofs are completed as claimed, the results are significant: they settle the complexity of 2D CMAPF, left open in earlier work, and provide new SAT fragments that may be useful for planar and linear planning reductions. The paper also develops an interesting self-contained theory of planar cycle augmentation and kite-graphs. Strengths include explicit, mostly detailed reduction chains, an extensive appendix on planar graph operations, and clear statements separating new results from prior work. The main deficits are concentrated in the most intricate gadget argument, Claim 8.10, and in a definitional inconsistency in Section 7; both are load-bearing for the PSPACE-hardness application.","major_comments":[{"comment":"The proof of Point 2 first gives a procedure from the initial configuration of Figure 24 and then asserts: \"We proved that c can be reached from the initial configuration.\" No proof of this assertion is given for an arbitrary variable-set configuration c, and this reachability is exactly what is needed in Claim 8.12, where a flip must be simulated from an arbitrary configuration reached after earlier flips. The reversibility of CMAPF does not help unless every such c is first shown reachable from the initial configuration. As written, the equivalence between CMAPF executions and variable-flip sequences is unsupported, so Theorem 8.8 rests on an unproved claim. The counting argument in Point 1 also does not by itself establish uniqueness of a free agent: |A| = 2|V|-1 and 2|V|-2 requesters show that if not all agents are adjacent to requesters then at least one agent is not, but they do not rule out several simultaneously movable agents. A complete proof of both points, or a revised simulation that avoids them, is required.","section":"§8.4, Claim 8.10(2)"},{"comment":"Lemma 7.5 defines E' = {(l,¬l) | (l,¬l) ∈ E} as the \"set of paired literals\" in G_lit(ϕ). However, Definition 2.2 defines G_lit(ϕ) as a bipartite graph with only literal-clause edges; paired edges between opposite literals are introduced only later in Definition 3.2 as part of G_lit(ϕ,π). Thus either the graph used in Lemma 7.5 contains edges not present in the graph defined earlier, in which case the cycle augmentation instance is not on the stated graph, or E' is empty and the dually connected matching argument cannot even get started. This discrepancy needs to be fixed explicitly, for example by defining the augmented literal graph used in the Section 7 reduction and checking that Lemma 7.5 refers to that graph.","section":"§7, Lemma 7.5 and Definition 2.2"}],"minor_comments":[{"comment":"The clause list in formula (1) ends with (g∨h∨j) but the third negative clause is written (¬c∨¬f∨¬i); the variable should likely be j for consistency.","section":"§3.1, Eq. (1)"},{"comment":"The text says \"Theorem 3.2 shows that Planar Linear 3-SAT has strictly less possible inputs\" but Proposition 3.2 is the correct reference; the same numbering slip appears elsewhere.","section":"§3.1, after Prop. 3.2"},{"comment":"The sentence \"We set ν:=ν_s and ν:=ν_t\" should define ν' as ν_t; otherwise the target assignment is overwritten.","section":"§7.1, before Lemma 7.2"},{"comment":"In the final sentence of the proof, \"Therefore G_lit(ϕ,π) is planar and valid\" should refer to the constructed variable-clause graph G_var(ϕ',π'), not to G_lit(ϕ,π).","section":"§4.2, proof of Theorem 4.6"},{"comment":"The proof says \"Similar to the proof of Theorem 8.6\" but the claim being proved is Claim 8.6; the intended reference should be corrected.","section":"§8.3, Claim 8.6 proof"}],"recommendation":"major_revision","confidential_remarks":"The reviewer's stress-test concern about Claim 8.10(2) is genuine and is the main obstacle to accepting the PSPACE-hardness result. The Section 7 paired-edge discrepancy is also substantive and should be resolved in the revision. Both issues appear fixable within the paper's existing framework, so I do not recommend rejection; however, the current manuscript should not be accepted without a repaired proof of the bridge-line reachability claim."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear colleague,\n\nThe headline: this is a serious paper, not a finished one. It introduces Linear Planar 3-SAT and Linear Literal-Planar 3-SAT, proves both NP-complete, proves PSPACE-completeness for their reconfiguration problems, and uses these to claim NP-completeness of Bounded 2D CMAPF and PSPACE-completeness of 2D CMAPF. The new fragments and the cycle-augmentation toolkit are genuinely useful; the reductions in Sections 4 and 7 are mostly careful, and the kite-graph sufficient condition with the dual-coloring algorithm is a nice idea. The application to 2D CMAPF answers a question left open in [15], so the stakes are real.\n\nWhat I think is solid: Theorem 4.1, the reduction from monotone planar 3-SAT to linear literal-planar 3-SAT, is well explained, with explicit linearity and validity arguments. Theorem 4.6, the reduction to monotone linear planar 3-SAT, is neat and the friend-assignment argument checks out. The cycle-augmentation algorithm in Section 5 is involved, but the invariants are stated and the appendix support is substantial. The NCL reduction in Section 7.1, including Lemma 7.4 showing that G_lit(phi) is a subdivision of the constraint graph, is credible and gives a reusable result. The citation pattern is fine: self-citations appear as context, not as load-bearing evidence.\n\nThe soft spot is exactly where the reader's stress-test lands. Claim 8.10(2) asserts that from any all-variables-set configuration, any chosen agent in A can be made free. The proof gives a routing procedure from the initial configuration, then says \"we proved c can be reached from the initial configuration\"—but no such proof appears for arbitrary c. Since Claim 8.12 uses that reachability to simulate each variable flip, the PSPACE-hardness of 2D CMAPF currently rests on an unproved state-space connectivity claim. I think it is probably true—the line has the right counting, and reversibility helps—but it needs an invariant, not a one-liner.\n\nA smaller issue: Lemma 7.5 defines E' as pairs (l, not l) \"such that (l, not l) in E\", but E is the literal-clause edge set, which contains no paired edges. The dually connected matching needs a graph that already has those paired edges, or a different definition. This is a notation/set-up problem, probably easy to repair.\n\nNet: the NP-completeness results and cycle-augmentation theory are in good shape; the PSPACE-hardness application has a real gap. I would send this to a serious referee, because the contribution is substantial and the gap is identifiable and likely fixable. I would also take it to a reading group—the discussion around Claim 8.10 is exactly the kind of thing a group will either resolve or sink.","headline":"Solid new 3-SAT fragments and a useful cycle-augmentation toolkit, but the 2D CMAPF PSPACE-hardness proof has a load-bearing reachability gap that needs a real proof.","tokens_in":37888,"tokens_out":2771,"would_cite":true,"duration_ms":27859,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q17","68Q25","03B05"],"pacs":[],"model":"deepseek-v4-flash","headline":"Combining linearity and planarity in 3-SAT preserves NP-completeness and PSPACE-completeness, and the new fragments settle the complexity of connected multi-agent pathfinding on 2D grids.","keywords":["linear planar 3-SAT","linear literal-planar 3-SAT","monotone linear planar 3-SAT","3-SAT reconfiguration","planar cycle augmentation","connected multi-agent pathfinding","PSPACE-completeness","NP-completeness"],"falsifier":"Search the state space of the variable-gadget line in Figure 24, restricted to configurations with all variable agents set and at most one free bridge agent, for a configuration that cannot be reached from the initial configuration without first freeing two bridge agents; exhibiting such a configuration would refute Claim 8.10 and break the PSPACE-hardness reduction.","tokens_in":36783,"feed_emoji":"🤖","tokens_out":7970,"duration_ms":75358,"temperature":0.7,"pith_summary":"The paper asks whether the two most useful SAT restrictions for planning, linearity and planarity, can be combined without losing hardness, and answers yes. It introduces linear planar 3-SAT and the stricter linear literal-planar 3-SAT, proves both NP-complete, and proves their reconfiguration problems PSPACE-complete, using a new monotone linear planar fragment as an intermediate. These results are then applied to connected multi-agent pathfinding on 2D grids, a setting where only the 3D case had previously been settled: the bounded version is NP-complete even with execution bound 2 and communication radius 1, and the unbounded version is PSPACE-complete. A reader should care because the new SAT fragments are designed to make hardness proofs for planar, grid-based planning problems substantially more direct.","feed_headline":"2D connected multi-agent pathfinding is PSPACE-complete","feed_subtitle":"New linear planar 3-SAT fragments settle the 2D case; the bounded version is NP-complete even with bound 2.","key_machinery":"The argument is carried by three mechanisms. First, the SAT reduction machinery: to make a monotone planar formula linear, each variable occurrence is replaced by a fresh literal connected through chains of two-literal clauses, and linear literal-planar formulas are turned into monotone linear planar formulas by renaming each negative literal to a fresh variable and adding a paired two-literal clause. Second, the planar cycle augmentation theory: a sufficient condition, the existence of a kite-graph, a bipartite planar Eulerian graph in which each target vertex has degree 2, guarantees a cycle over the target vertices that can be added while preserving planarity, and when the instance has a dually connected matching such a cycle is computable in polynomial time; this is what lets the reconfiguration reduction build the literal cycle that prior planar reconfiguration results lacked. Third, the CMAPF gadget architecture: variable agents encode truth values by position, mobile literal agents in clause gadgets can move only when their literal is satisfied, and the bridge agents on the variable line enforce that at most one variable flips per step.","core_discovery":"The discovery is that the linear and planar restrictions on 3-CNF formulas are compatible in a strong sense: formulas that are simultaneously linear and planar, with respect to a variable cycle, and in the stricter literal-planar variant with respect to a literal cycle, remain NP-complete for satisfiability, and their reconfiguration problems are PSPACE-complete. The intermediate monotone linear planar fragment is also NP- and PSPACE-complete, and the NP-hardness holds even when each variable appears negatively in at most one clause. The paper applies these fragments to grid planning: it proves that Bounded 2D CMAPF is NP-complete even for bound 2 and radius 1, and that 2D CMAPF is PSPACE-complete. Supporting this chain, it shows that planar cycle augmentation is NP-complete but admits a polynomial-time sufficient condition based on kite-graphs and dually connected matchings.","pith_inferences":["Inference: the same friend-assignment technique used to reduce linear literal-planar reconfiguration to monotone linear planar reconfiguration could likely prove PSPACE-completeness for a monotone literal-planar fragment, a variant the paper does not define.","Inference: the kite-graph and dually-connected-matching criterion suggests a polynomial-time algorithm for planar cycle augmentation on graph classes that reliably admit such matchings; testing outerplanar or bounded-treewidth graphs would be a direct next step.","Inference: because the 2D hardness survives radius 1 and bound 2, the geometry of the 2D grid rather than the communication range is the source of hardness; whether the reduction adapts to hexagonal or king-move grids is a testable extension not addressed in the paper.","Inference: if the missing reachability proof in Claim 8.10 is supplied, the same bridge-gadget architecture should extend to other connectivity-constrained motion planning problems, such as the tethered-robot and snake-like robot settings named in the paper."],"forward_implications":["If the proofs are correct, Linear Planar 3-SAT is NP-complete, giving a planar and linear SAT fragment that can serve as a source for hardness reductions to planar motion-planning problems.","Linear Literal-Planar 3-SAT reconfiguration is PSPACE-complete, and so is its monotone linear planar restriction even when each negative literal appears in at most one clause.","Bounded 2D CMAPF is NP-complete even with execution bound 2 and communication radius 1, so the hardness of the bounded problem does not require long paths or long-range communication.","Unbounded 2D CMAPF is PSPACE-complete, settling the 2D case left open by prior work that only handled 3D grids.","Because the constructed gadgets trap each agent in its own connected component, the same hardness transfers to the anonymous version of CMAPF in which targets are not assigned to specific agents."],"supporting_citations":[{"why":"It defines Planar 3-SAT and the variable-cycle augmentation that the paper uses to define its planar fragments.","marker":"[2]"},{"why":"It establishes NP-completeness of Linear 3-SAT, the linearity restriction that the paper combines with planarity.","marker":"[9]"},{"why":"It shows Monotone Planar 3-SAT is NP-complete and serves as the source problem for the first reduction to Linear Literal-Planar 3-SAT.","marker":"[16]"},{"why":"It proves 3-SAT reconfiguration PSPACE-complete on planar formulas, and supplies the gadget construction that the paper refines for linear literal-planar reconfiguration.","marker":"[13]"},{"why":"It establishes PSPACE-completeness of Nondeterministic Constraint Logic configuration-to-configuration, the reduction source for the reconfiguration results.","marker":"[17]"},{"why":"It proves CMAPF PSPACE-complete in 3D grids and bounded CMAPF NP-complete, the result the 2D theorems extend by removing the third dimension.","marker":"[15]"},{"why":"It proves connected multi-agent pathfinding PSPACE-complete on general graphs, providing the known hardness baseline for CMAPF.","marker":"[19]"},{"why":"It gives polynomial-time planarity testing and embedding, used to place planar cycle augmentation in NP and to construct embeddings in the reductions.","marker":"[21]"},{"why":"It shows Hamiltonicity is NP-complete on maximal planar graphs, the reduction source for the NP-hardness of planar cycle augmentation.","marker":"[22]"}],"fun_headline_variants":["Linear planar 3-SAT: new hardness results for 2D pathfinding","2D connected multi-agent pathfinding proven PSPACE-complete","Bounded 2D CMAPF NP-complete even with bound 2","New SAT fragment yields PSPACE-completeness of 2D pathfinding","Linear planar 3-SAT reveals grid pathfinding complexity"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The PSPACE-hardness application rests on Claim 8.10's assertion that every configuration with all variable agents set can be reached from the initial configuration, and hence that any chosen bridge agent can be freed; the paper demonstrates this only from the initial configuration, leaving unsupported the equivalence between CMAPF moves and single variable flips claimed in Claim 8.12.","fun_headline_variants_meta":{"raw":{"variants":["Linear planar 3-SAT: new hardness results for 2D pathfinding","2D connected multi-agent pathfinding proven PSPACE-complete","Bounded 2D CMAPF NP-complete even with bound 2","New SAT fragment yields PSPACE-completeness of 2D pathfinding","Linear planar 3-SAT reveals grid pathfinding complexity"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00082,"raw_usage":{"total_tokens":3570,"prompt_tokens":908,"completion_tokens":2662,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":524,"completion_tokens_details":{"reasoning_tokens":2566}},"tokens_in":524,"tokens_out":2662,"duration_ms":19611,"temperature":1.0,"reasoning_tokens":2566,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T19:49:48.893916+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Search the state space of the variable-gadget line in Figure 24, restricted to configurations with all variable agents set and at most one free bridge agent, for a configuration that cannot be reached from the initial configuration without first freeing two bridge agents; exhibiting such a configuration would refute Claim 8.10 and break the PSPACE-hardness reduction.","supporting_citations":[{"cited_title":"Lichtenstein, Planar formulae and their uses, SIAM journal on computing 11 (2) (1982) 329–343","cited_arxiv_id":null,"evidence_quote":"It defines Planar 3-SAT and the variable-cycle augmentation that the paper uses to define its planar fragments."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"It establishes NP-completeness of Linear 3-SAT, the linearity restriction that the paper combines with planarity."},{"cited_title":"de Berg, A","cited_arxiv_id":null,"evidence_quote":"It shows Monotone Planar 3-SAT is NP-complete and serves as the source problem for the first reduction to Linear Literal-Planar 3-SAT."},{"cited_title":"Cardinal, E","cited_arxiv_id":null,"evidence_quote":"It proves 3-SAT reconfiguration PSPACE-complete on planar formulas, and supplies the gadget construction that the paper refines for linear literal-planar reconfiguration."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"It establishes PSPACE-completeness of Nondeterministic Constraint Logic configuration-to-configuration, the reduction source for the reconfiguration results."},{"cited_title":"Calviac, O","cited_arxiv_id":null,"evidence_quote":"It proves CMAPF PSPACE-complete in 3D grids and bounded CMAPF NP-complete, the result the 2D theorems extend by removing the third dimension."},{"cited_title":"Tateo, J","cited_arxiv_id":null,"evidence_quote":"It proves connected multi-agent pathfinding PSPACE-complete on general graphs, providing the known hardness baseline for CMAPF."},{"cited_title":"Wigderson, The complexity of the hamiltonian circuit problem for maximal planar graphs, EECS Department Report 298 (1982)","cited_arxiv_id":null,"evidence_quote":"It shows Hamiltonicity is NP-complete on maximal planar graphs, the reduction source for the NP-hardness of planar cycle augmentation."}],"review_version":2}