{"id":"2cd28e27-8565-4132-ba63-f7322f1164a1","arxiv_id":"2412.00941","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Limit-sure reachability in POMDPs under constant-memory policies is NP-complete.","lead":"This paper proves that checking whether a POMDP can reach a target with probability arbitrarily close to 1 using a fixed small amount of memory is NP-complete. The result closes a gap between the undecidability of the general problem and the NP-completeness of the almost-sure version.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 6's polynomial-size integer-rank witness is the load-bearing gap: the proof's 'w.l.o.g.' reduction from arbitrary Puiseux policies to integer ranks is not justified, and the inequality system over ranks is only finite, not polynomial, so NP membership is not established by the printed…","rationale":"The strongest claim is NP-completeness. NP-hardness (Proposition 1, §3.3) is a direct DAG reduction from 3-SAT and appears solid, including the reduction to deterministic policies via Kuhn's theorem. The NP upper bound is the vulnerable direction. It has three stages: Lemma 1 (POMDP to blind MDP), Lemma 6 (Puiseux witness to integer rank witness of polynomial size), and Lemma 7 (polynomial-time verifier).\n\nLemma 1's proof has an undefined conditional policy when σ'((·,z)) sums to zero, but the lemma itself is true: a zero-denominator observation acts as an absorbing trap in the blind MDP, so any arbitrary definition of the POMDP policy there cannot decrease the POMDP's reachability value. This is a typo-level gap, not a load-bearing flaw. Lemma 7 is plausible: the support of exit distributions can be decided by minimum directed spanning tree weights, and the iterative construction runs in polynomial time.\n\nLemma 6 is different: it contains the central constructive claim that the NP certificate exists. The printed proof neither defines the rank functional correctly nor proves the 'w.l.o.g.' passage from arbitrary Puiseux functions to integer powers of ε. The inequality system over ranks is only shown to be finite, not polynomial, and the Cramer-rule paragraph does not address the fact that the graph constraints are existential over exponentially many exit graphs. If the intended perturbation argument can be made to work, the theorem stands; if not, the NP upper bound collapses to an existential-theory-of-reals-style bound.\n\nTherefore the verdict should remain conditional: the result is plausible and the lower bound is solid, but Lemma 6 must be rewritten and independently checked before the upper bound is accepted. I agree with the reader's identification of Lemma 6 as the main weakness, but I do not share the emphasis on Lemma 1's division-by-zero issue, which is easily patched.","tokens_in":21177,"tokens_out":20263,"duration_ms":213349,"concrete_test":"Re-derive Lemma 6 in two parts. (a) For a fixed Puiseux policy, define r(a)=ord_{ε→0} σ(ε)(a); prove that setting i(a)=N·r(a) for a common denominator N preserves every nonempty support supp(δ(B,·)) and hence the graph of communicating classes. (b) For a fixed total preorder of ranks, write the constraints fixing a given communicating-class graph as linear inequalities, extract a square subsystem of size |A| that is tight at an integer solution, and check whether Cramer's rule bounds the bit length by poly(|S|) despite the full system being exponential. Run both steps on the 4-state blind MDP of Example 1, plus a variant with actions whose Puiseux exponents are 1/2 and 1/3, to see where the printed proof breaks.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 1 is NP-complete; the lower bound (§3.3) is a solid DAG reduction from 3-SAT. The load-bearing question is the NP upper bound. The certificate guessed is an integer rank policy, whose existence is the content of Lemma 6 (§3.2). The proof of Lemma 6 starts from a Puiseux policy supplied by Lemma 2 and asserts, without argument, that it is 'without loss of generality' of the form σ(ε)(a)=ε^{i(a)}; the displayed definition of i(a) just before this assertion is ill-formed (the infimum expression has unbound state variables and does not define a rank per action). A general Puiseux policy can have rational leading exponents, so the passage to integer powers must be proved: one must show that the graph of communicating classes—defined by supports of exit distributions and minimal exit-graph weights—is preserved. The subsequent construction of the inequality system is also only existential: there are finitely many exit graphs, but potentially exponentially many, and the proof does not show that a polynomial-size subsystem suffices to force a given graph. The Cramer's-rule paragraph therefore does not establish the claimed polynomial-size rank witness. If the true witness sometimes requires exponentially many constraints to characterize, or requires ranks of exponential bit length, the NP membership argument fails. Lemma 1's undefined policy when an observation has zero probability is a genuine typo, but it is patchable (define an arbitrary distribution there; the blind process is absorbed), so it is not the main risk.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies limit-sure reachability in partially observable Markov decision processes (POMDPs) under memoryless and, more generally, constant-memory policies. The main claimed result, Theorem 1, is that deciding whether a POMDP with a reachability objective is limit-sure winning under memoryless policies is NP-complete; Corollaries 2 and 3 extend this to constant-memory policies and parity objectives. The upper bound is developed through a sequence of reductions: Lemma 1 reduces POMDPs to blind MDPs, Lemma 2 uses Tarski-Seidenberg to obtain Puiseux-function policy witnesses, Lemmas 3–5 characterize limit-sure winning in the induced Puiseux Markov chains via communicating classes, Lemma 6 asserts the existence of polynomial-size integer-rank policy witnesses, and Lemma 7 provides a polynomial-time verifier for such witnesses. The lower bound is an explicit reduction from 3-SAT (Proposition 1). The paper closes with extensions to parity objectives and parametric Markov chains.","tokens_in":21436,"tokens_out":19657,"duration_ms":193963,"significance":"If the proof is completed, the result is significant: it settles the complexity of limit-sure reachability for the practically important class of small-memory POMDP policies, complementing the EXPTIME-completeness of almost-sure winning and the undecidability of general limit-sure winning. The high-level strategy is interesting and plausible, and the 3-SAT lower-bound construction appears solid. The paper also deserves credit for a clear presentation of the rank-policy concept and for explicitly separating the lower and upper bounds. However, the NP upper bound as printed rests on Lemma 6, whose proof contains a load-bearing gap: the passage from arbitrary Puiseux policies to integer-rank policies is asserted rather than proved, and the polynomial-size certificate claim is not established because the characterizing inequality system may have exponentially many constraints. A second gap occurs in Lemma 1's converse direction. These issues are local and appear fixable, but they must be repaired before the central claim can be accepted.","major_comments":[{"comment":"The step in which an arbitrary Puiseux policy σ is replaced, 'without loss of generality', by a rank policy of the form σ(ε)(a) = ε^{i(a)} / Σ_b ε^{i(b)} is not proved. The displayed definition of i(a), namely i(a) := inf{ r ≥ 0 : lim_{ε→0+} (Σ_a σ(ε)(a)δ(s,a)(s̃))/ε^r }, is ill-formed: the left-hand side does not depend on s and s̃ while the right-hand side does, and the sum over a makes the right-hand side independent of a. A genuine Puiseux policy can have leading exponents α_a ∈ Q and nonzero coefficients; the proof must show that after substituting ε ← ε^L for a common denominator L and dropping the coefficients, the communicating classes and exit-distribution supports are unchanged. This is load-bearing because the rank policy is exactly the NP certificate guessed in the upper bound.","section":"§3.2, Lemma 6"},{"comment":"The claim that the inequality system characterizing the graph of communicating classes has a polynomial-size solution is not established. The system is over the |A| variables (i(a))_{a∈A}, but it contains constraints for every pair of exit graphs of every communicating class; a communicating class B can have exponentially many exit graphs, so the finite system can be exponential. The proof does not show that a polynomial-size subsystem suffices to force the same graph, nor does it explain how Cramer's rule is applied to a system of polynomial size. Consequently, the 'moreover' part of Lemma 6 — that the rank policy description is of polynomial size — does not follow from the argument as written. Without this, Lemma 7 gives a verifier for a certificate whose existence has not been proved, and the NP upper bound is incomplete.","section":"§3.2, Lemma 6"},{"comment":"In the converse direction of the reduction from POMDPs to blind MDPs, the policy σ(z)(a) := σ'((a,z)) / Σ_{ã} σ'((ã,z)) is undefined when the denominator is zero. This case can occur even for observations that are reached with positive probability under σ': in the blind MDP, a state with observation z is then trapped by self-loops, whereas an arbitrary choice of σ(z) in the POMDP may advance the process. Defining an arbitrary distribution at such z does not by itself restore the coupling argument as printed. The value-equality statement may still be true — for example, one might perturb any limit-sure witness to give every observation positive mass and use a semicontinuity argument — but that argument is not supplied, and the reduction is the first step of the upper bound.","section":"§3.2, Lemma 1"}],"minor_comments":[{"comment":"In the proof of the converse direction, the final displayed conclusion states that lim_{ε→0+} P(exit(C) < ∞) = 0, but the argument appears to establish the opposite: the probability of eventually exiting any non-target subset C should tend to 1, not 0. Please correct this sign or explain the intended event.","section":"§3.2, Lemma 5"},{"comment":"The selection defining i(s → s̃) is not fully specified: the proof says 'for some a ∈ I(s → s̃)' without stating whether this selection is part of the guessed witness or is existentially quantified in the inequality system. The subsequent constraints depend on this choice, so the definition should be made precise.","section":"§3.2, Lemma 6"},{"comment":"There is a typo in 'this line of work doe not apply'; it should read 'does not apply'.","section":"§1, Related works"}],"recommendation":"major_revision","confidential_remarks":"The main risk to the paper is the NP upper bound, specifically Lemma 6. If the polynomial-size rank-policy witness cannot be established, the central claim reduces to NP-hardness plus an upper bound that is not proven. The gaps appear to be repairable, but they are substantial enough that the paper should not be accepted in its current form. The result, if completed, would be a good fit for the journal and of interest to the POMDP and stochastic-games communities."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nYou should know this paper proves that limit-sure reachability for POMDPs under memoryless (and constant-memory) policies is NP-complete. That is a genuine new result, filling a real gap: almost-sure under small memory is known NP-complete, limit-sure in general is undecidable, and nobody had pinned down limit-sure under small memory. The lower bound via 3-SAT is clean and correct, and the paper's use of Puiseux Markov chains and Solan's exit-graph machinery is appropriate.\n\nWhat I like: the paper is honest about the technical difference between almost-sure and limit-sure (Example 1 is helpful), and the overall architecture is sensible—reduce POMDP to blind MDP, argue a Puiseux witness exists via real-closed fields, then claim a rank policy of polynomial size, then give a polynomial-time verifier. If the rank-policy witness step holds, the NP upper bound follows.\n\nNow the soft spot, and it is load-bearing: Lemma 6 does not establish that a limit-sure winning blind MDP admits a rank policy witness of polynomial size. The proof starts from a Puiseux policy supplied by Lemma 2 and asserts, without proof, that we can take it to be of the form ε^{i(a)} with integer exponents. A general Puiseux policy can have rational leading exponents; you have to show that the communicating-class graph is preserved when you pass to integer powers. That is not done. The inequality system over ranks is finite, but finite is not polynomial—there can be exponentially many exit graphs, and the proof does not show a polynomial-size subsystem forces the right graph. The Cramer's-rule paragraph therefore does not deliver the polynomial-size integer solution claimed. This is not a typo; it is an actual gap in the NP membership argument.\n\nLemma 1's inverse policy is undefined when an observation has zero probability under σ', but that is a minor patchable issue. I also noticed the displayed formula for i(a) just before the 'without loss of generality' passage is indeed ill-formed, with unbound state variables.\n\nIn short: the result is probably true, and the paper deserves a serious referee, but it needs major revision, not copy-editing. The authors need to prove the transition from Puiseux to integer rank policies, or find another witness argument. I'd send it to review with a request for heavy revision; I would not accept it as is. For a reading group, worth a session if you're working on POMDP complexity.","headline":"Solid new NP-completeness result for limit-sure reachability under small-memory POMDP policies; the core upper-bound witness argument in Lemma 6 needs repair before the result is fully proved.","tokens_in":22030,"tokens_out":1996,"would_cite":true,"duration_ms":18034,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q17","68Q25","90C40"],"pacs":[],"model":"deepseek-v4-flash","headline":"Determining whether a POMDP can reach its target with probability arbitrarily close to 1 under a memoryless or small-memory policy is NP-complete.","keywords":["POMDP","limit-sure winning","memoryless policies","reachability","NP-completeness","rank policies","Puiseux functions","parity objectives"],"falsifier":"Exhibit a blind MDP for which the minimal rank policy witness requires integer ranks whose binary representation is super-polynomial in the number of states. If such an MDP exists, the polynomial-size witness claim (Lemma 6) is false and the NP upper bound does not hold. Alternatively, search for a limit-sure winning blind MDP whose rank policy must use a number of distinct ranks exponential in the state count; its existence would also refute the proof.","tokens_in":20951,"feed_emoji":"🎯","tokens_out":4373,"duration_ms":35410,"temperature":0.7,"pith_summary":"This paper settles the computational complexity of limit-sure reachability in partially observable Markov decision processes (POMDPs) under memoryless and constant-memory policies: the problem is NP-complete. The authors show that, unlike almost-sure winning, the limit-sure property is witnessed not by a single policy but by a sequence of policies whose probabilities concentrate on higher-rank actions as the allowed error tends to zero. They prove that every limit-sure winning blind MDP admits a rank policy witness of polynomial size, and that such a witness can be verified in polynomial time, giving the NP upper bound. The NP-hardness comes from a reduction from 3-SAT. If correct, this closes the complexity gap between almost-sure (NP-complete) and limit-sure problems for small-memory policies.","feed_headline":"Small-memory POMDP reachability is NP-complete","feed_subtitle":"A strategy that wins with probability 1-epsilon needs action ranks; deciding whether one exists is NP-complete.","key_machinery":"The argument is carried by rank policies and the graph of communicating classes of the induced Puiseux Markov chain. A rank policy assigns each action a rank i(a) and plays it with probability proportional to $epsilon^{{i(a)}}$; the graph of communicating classes has one vertex per communicating class of the epsilon-parameterized Markov chain and edges recording which classes are reachable in the limit as epsilon goes to zero. The graph's structure—in particular whether every reachable absorbing communicating class other than the target has a nonempty exit distribution—characterizes limit-sure reachability (Lemma 5). The NP upper bound follows because the ranks can be chosen as polynomial-size integers and verified in polynomial time using minimum directed spanning tree computations.","core_discovery":"The central discovery is that limit-sure reachability under memoryless policies in POMDPs is neither polynomial-time solvable nor undecidable; it is NP-complete. The key technical insight is the introduction of rank policies: memoryless policies in which each action is assigned a non-negative integer rank and is played with probability proportional to epsilon raised to that rank. As epsilon tends to zero, lower-rank actions receive higher probability, and if low-rank actions form a cycle, higher-rank actions determine the exit distribution from that cycle. The paper proves that any limit-sure winning blind MDP admits a rank policy witness whose ranks are integers of polynomial bit size, and that the witness property can be checked in polynomial time. This stands in contrast to almost-sure winning, where uniform randomization over the support of a policy suffices, and to the general limit-sure problem, which is undecidable.","pith_inferences":["If the polynomial-size rank witness lemma is correct, a practical consequence follows: limit-sure reachability for small-memory POMDPs can be encoded into SAT or mixed-integer programming, enabling solver-based synthesis of controllers that achieve the target with arbitrary precision.","The gap between NP-completeness for small memory and undecidability for general policies suggests that any hardness for general policies must come from unbounded memory; this may transfer to other objectives such as mean-payoff or total reward.","A testable extension is that the rank-policy witness characterization may give a sound and complete abstraction for parametric Markov chains, complementing the known NP results for almost-sure reachability in that setting.","The distinction between limit-sure and almost-sure witnesses hints that approximation schemes for POMDPs may need to reason about asymptotic action probabilities, not just supports, which could inform the design of heuristics for planning under partial observability."],"forward_implications":["Limit-sure winning under memoryless policies is decidable in NP, in contrast with the undecidability of the general limit-sure problem for unrestricted policies.","Constant-memory policies do not change the complexity: the problem remains NP-complete for any memory bound that is polynomial in the size of the POMDP.","The NP-completeness extends to parity (omega-regular) objectives under constant memory, since recurrent classes of a Markov chain satisfy parity with probability either 0 or 1.","Limit-sure winning and almost-sure winning have the same complexity for small-memory policies but require different witnesses: rank policies rather than uniform supports of actions.","The polynomial-size rank witness characterization gives a concrete target for encoding the problem into SAT or mixed-integer linear programming solvers."],"supporting_citations":[{"why":"Provides the exit distribution and exit graph theorems for Puiseux Markov chains that underlie the characterization of limit-sure reachability and the polynomial-time verifier.","marker":"[Sol03]"},{"why":"Establishes that the field of Puiseux functions is real-closed, which lets the authors translate the first-order reachability condition into the existence of Puiseux policy witnesses.","marker":"[BK76]"},{"why":"Supplies the Tarski-Seidenberg principle used to move between the real numbers and the Puiseux function field in Lemma 2.","marker":"[BPR06]"},{"why":"Gives the fixpoint characterization of reachability values in Markov chains used to formulate the first-order decision problem for limit-sure winning.","marker":"[BK08]"},{"why":"Provides the polynomial-time minimum directed spanning tree algorithm used to compute exit graph weights in the verifier of Lemma 7.","marker":"[GGST86]"},{"why":"Establishes NP-hardness of limit-sure winning for partial-observation games, which the paper adapts to POMDPs via a uniform distribution over the adversary's choices.","marker":"[CKS13]"},{"why":"The 3-SAT problem is the source of the explicit NP-hardness reduction in Proposition 1.","marker":"[Kar72]"}],"fun_headline_variants":["Limit-sure reachability in POMDPs: memoryless is NP-complete","Memoryless POMDP limit-sure reachability is NP-complete","Fixed-memory POMDP reachability: NP-complete, not undecidable","Small-memory POMDP policies: limit-sure reachability NP-complete"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The NP membership proof assumes that every limit-sure winning blind MDP has a rank policy witness with integer ranks of polynomial bit size; if some instance requires exponentially large ranks, the guessed witness would be too long and the NP upper bound collapses.","fun_headline_variants_meta":{"raw":{"variants":["Limit-sure reachability in POMDPs: memoryless is NP-complete","Memoryless POMDP limit-sure reachability is NP-complete","Fixed-memory POMDP reachability: NP-complete, not undecidable","Small-memory POMDP policies: limit-sure reachability NP-complete"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001188,"raw_usage":{"total_tokens":4866,"prompt_tokens":869,"completion_tokens":3997,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":485,"completion_tokens_details":{"reasoning_tokens":3910}},"tokens_in":485,"tokens_out":3997,"duration_ms":25348,"temperature":1.0,"reasoning_tokens":3910,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T04:51:24.285144+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Exhibit a blind MDP for which the minimal rank policy witness requires integer ranks whose binary representation is super-polynomial in the number of states. If such an MDP exists, the polynomial-size witness claim (Lemma 6) is false and the NP upper bound does not hold. Alternatively, search for a limit-sure winning blind MDP whose rank policy must use a number of distinct ranks exponential in the state count; its existence would also refute the proof.","supporting_citations":[],"review_version":1}