{"id":"4b64c46e-721d-4ea1-a923-5f93e800a86a","arxiv_id":"2502.00145","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"Bounded-length planning is extended from finding one plan to counting all plans and answering probabilistic and facet queries, with new complexity results and a practical tool.","lead":"Classical planners usually find one plan; this paper studies how to count every plan of bounded length and answer questions about the plan space, such as how often an action appears. It proves complexity bounds for these reasoning tasks and releases Planalyst, a tool that compiles planning problems into a form that supports counting, probability queries, and uniform sampling.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The claimed one-to-one correspondence between SAT models and plans in F_plan≤ℓ is unproven and the described constraints are insufficient to ensure it; if it fails, every count and derived probability/facet query from Planalyst is invalid.","rationale":"The paper's primary contribution is a practical system that counts plans and answers reasoning queries via knowledge compilation. Every output of this system is derived from the model count of F_plan≤ℓ[Π]. The reader identified the one-to-one correspondence between models and plans as the weakest assumption; I agree. The described encoding is under-specified: listing only positive effect propagation and padding does not guarantee that a satisfying assignment uniquely determines a state trajectory. Without frame axioms and complete operator semantics, the number of models can exceed the number of plans. The paper's own remark about other encodings losing the bijection underscores that this is not automatic. The complexity theorems (C=P-, NP-, DP-completeness) are standard and plausible, and the proofs, though sketchy, can likely be completed; they do not depend on the SAT encoding's bijection. Thus the theoretical core is not at risk. The empirical results, however, are meaningful only if the counts are exact. A concrete validation against exhaustive enumeration would settle the concern. Since the authors can address this by adding a correctness proof or a verification experiment, the CONDITIONAL verdict is appropriate; no change is needed.","tokens_in":21647,"tokens_out":12992,"duration_ms":129445,"concrete_test":"Run Planalyst's Count on 50 small benchmark tasks where the exact number of plans can be obtained by exhaustive enumeration (e.g., using K* or a brute-force state-space search with the same length bound). Require exact numerical agreement on all tasks. Additionally, for one task with a small plan space, enumerate all satisfying assignments of the compiled d-DNNF (or the CNF) and all plans, and check that the induced map from assignments to plans is a bijection; any assignment that does not correspond to a valid plan, or any plan with multiple assignments, refutes the one-to-one claim.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central practical claim relies on a bijection between satisfying assignments of the sequential SAT encoding F_plan≤ℓ[Π] and plans of length at most ℓ (Section 2). The paper describes only four constraint groups: initial state, goal, at-most-one operator per step, and a one-way 'operator effect implies state' clause, plus a padding formula that propagates unused steps to the end. This is insufficient: it omits preconditions, negative effects, frame axioms, and state persistence when no operator is applied. As a result, a single fixed operator sequence can be embedded in many distinct state-variable assignments, generating spurious models that inflate the model count relative to the true plan count. The statement in Section 6.3 that other encodings 'lose the one-to-one correspondence' confirms the property is delicate, yet the paper gives no proof that the chosen Madagascar-based encoding actually has it, nor does it validate counts against an independent source. All practical claims about counting, conditional probability, facets, and uniform sampling in Sections 6 and 7 are unsound if the bijection fails.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces a taxonomy of qualitative and quantitative reasoning problems over the plan space of classical planning tasks with polynomially bounded plan length. It proves complexity results: Poly-Brave-Plan-Exist is NP-complete, Poly-Cautious-Plan-Exist is coNP-complete, Poly-Probabilistic-Reason is C=P-complete, FacetReason is NP-complete, and Exact-k-Facets is DP-complete. On the practical side, it presents Planalyst, which compiles a SAT encoding of a planning task into a d-DNNF and uses the compiled form to count plans and answer queries such as conditional probabilities, facet membership, and uniform sampling. The empirical evaluation compares Planalyst's counting mode with the top-quality planners K* and SymK, reporting favorable coverage when plan spaces are large.","tokens_in":21864,"tokens_out":8959,"duration_ms":82749,"significance":"If the results hold, the paper would provide a valuable bridge between model counting and classical planning, with a useful complexity classification and a practical tool that scales to large plan spaces. The authors make their code, benchmarks, and data publicly available (Section 6.1), which is a strength. The facet-based reasoning notion is original and potentially useful for plan-space navigation. However, the current version is built on an encoding whose claimed one-to-one correspondence is neither fully specified nor proved, which undermines both the theoretical reductions and the empirical counts; the proofs in Appendix B are also too sketchy in places. The potential significance is high, but the validity of the main pipeline is not yet established.","major_comments":[{"comment":"The claim that F_plan≤ℓ[Π] has a one-to-one correspondence between its models and the ℓ-bounded plans of Π is not supported by the described constraints. The listed constraints (initial state, goal, at-most-one operator per step, and the implication from operator effects to state variables) omit operator preconditions, negative effects, and frame axioms that would propagate unchanged state variables between steps. As a result, a single operator sequence can correspond to many models with arbitrary state assignments, and models can exist for sequences that are not executable plans. This undermines the plan counts and probability/facet queries reported in Sections 6 and 7, as well as the parsimonious reductions in Appendix B (Lemma 6, Theorems 9, 10, 11, and 13) that rely on this encoding. The note in Section 6.3 that other encodings 'lose the one-to-one correspondence' shows the property is nontrivial, but no proof or citation is given that the Madagascar-based encoding used by Planalyst actually possesses it. Please provide the full encoding, prove or cite the bijection property, and validate the counts against an independent source on small instances.","section":"Section 2 (Planning as Satisfiability)"},{"comment":"The hardness proofs are presented as sketches and are too incomplete to support the complexity classifications. Lemma 6 states that hardness is obtained by 'vacuously extending' Bylander's reduction, with no construction of the reduction. Lemma 11's hardness direction similarly asserts that 'we need to make every facet candidate into a facet' without specifying how this is achieved. These results are load-bearing for the paper's theoretical contributions, so the reductions should be given in full or backed by precise references that contain the arguments.","section":"Appendix B (Lemma 6 and Lemma 11)"},{"comment":"The empirical evaluation in Tables 2 and 3 reports only coverage, i.e., whether each approach determined a count within the resource limits, not the actual count values. Without a comparison of counts on instances where all solvers succeed, the reported plan counts (including cases with more than 10^21 plans) cannot be verified against the baseline planners that enumerate plans. Reporting the counts on a common subset would directly test the bijection assumption behind Planalyst.","section":"Section 6 (Empirical Evaluation)"}],"minor_comments":[{"comment":"The phrase 'l-bounded' should be 'ℓ-bounded'; the text also contains several LaTeX artifacts (e.g., 's/llbracketo/rrbracket' and '⋀' symbols) that should be cleaned before publication.","section":"Section 2"},{"comment":"The formula in the proof includes 'o_ℓ' which should be 'o_i' to range over all time points.","section":"Appendix B, Lemma 6"},{"comment":"The statement 'Let Π be a program' should read 'Let Π be a planning task'.","section":"Theorem 13"},{"comment":"The formal definition of F_plan≤ℓ is only sketched; please state the full clause set or give a reference that specifies it.","section":"Section 2"},{"comment":"The significance measure Sℓ(Π,o) is defined but not demonstrated; a small example or empirical illustration would improve readability.","section":"Section 4"}],"recommendation":"major_revision","confidential_remarks":"The central encoding assumption is the main concern. If the authors cannot provide a correct encoding with a provable bijection and empirical count validation, the practical contributions would not stand. The complexity results might be salvageable independently, but the proofs need to be completed. The paper fits the scope of the journal, but the current version is not ready."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's my take on Speck et al. The genuinely new pieces are the complexity classification — probabilistic plan-space queries are C=P-complete, facet queries are NP/coNP/DP-complete — and the Planalyst tool, which compiles a planning task into a d-DNNF and counts plans without enumerating them. The facet notion, operators that occur in some but not all plans, is a useful intermediate reasoning mode, and the taxonomy is clean. The empirical section shows real scaling, counting tasks with over 10^12 plans, and the code and data are on Zenodo. That part is solid.\n\nThe soft spot is the SAT encoding's one-to-one correspondence. Section 2 asserts it but does not prove it. The listed constraints are only four groups: initial state, goal, at-most-one operator per step, and 'operator effect implies state.' As stated, that omits preconditions, negative effects, frame axioms, and state persistence when no operator is applied. A fixed operator sequence could then be embedded in many different state-variable assignments, inflating the count relative to the real plan count. The paper's later remark that other encodings 'lose the one-to-one correspondence' confirms the property is delicate. In practice the tool uses Madagascar's encoding, which is standard and known correct, so this may be an expository gap rather than a functional bug. But because the practical claims depend on exact counting, the paper should either give the full encoding or cite the precise formulation and prove the bijection. The experiments also validate by coverage rather than exact count agreement; the paper does not report whether Count and Enum agree on all solved instances, nor compare counts against an independent source.\n\nThe appendix proofs are sketches in places — Lemma 6 hardness 'vacuously extends' Bylander, Theorem 10 'slightly adapts' a reduction — but the reductions are standard and plausible. No circularity: they reduce to prior published results and use them as baselines.\n\nOverall this is a useful paper for anyone working on plan-space analysis, top-quality planning, or model counting in planning. The theoretical classification is the main contribution; the tool is a nice addition. The missing bijection proof is the one thing I would ask for in revision. It deserves a serious referee and should go to review.","headline":"New complexity results for plan-space reasoning are plausible and the Planalyst tool scales, but the central counting claim needs a proof of the SAT-plan bijection.","tokens_in":22388,"tokens_out":3543,"would_cite":true,"duration_ms":33633,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q17","68T20"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper claims a complete complexity classification for reasoning over polynomially bounded plan spaces and a d-DNNF compilation tool that counts trillions of plans without enumerating them.","keywords":["classical planning","plan counting","model counting","knowledge compilation","d-DNNF","facet reasoning","complexity classification","probabilistic reasoning"],"falsifier":"Run Planalyst on the paper's running example, whose plan space at bound 4 has exactly two plans; any reported count other than 2 falsifies the encoding-plus-compilation claim. For a sharper test, take a task with exactly one plan of length $\\ell-1$ and ask the count at bound $\\ell$: the padding convention forces exactly one model, so any count other than 1 means the one-to-one correspondence fails.","tokens_in":21480,"feed_emoji":"🧮","tokens_out":10904,"duration_ms":100903,"temperature":0.7,"pith_summary":"The paper's goal is to make the full space of plans of a classical planning task answerable to the same counting-based style of reasoning that model counting brought to propositional logic. It proves a complexity map for plan spaces of polynomially bounded length: counting plans is $\\#\\mathrm{P}$-complete, deciding whether the fraction of plans satisfying a query equals a given value is complete for $\\mathrm{C}_{=}\\mathrm{P}$, a counting class based on equal numbers of accepting and rejecting paths, and deciding whether an operator is a \\emph{facet}---present in some but not all plans---is $\\mathrm{NP}$-complete. On the practical side, the paper claims that compiling the planning task's SAT encoding into a d-DNNF, a decision-diagram normal form on which counting and conditioning are polynomial, lets a tool called Planalyst answer counts, probabilities, and facet queries without enumerating plans. The payoff is empirical: on benchmarks with huge plan spaces, counting outperforms planners that enumerate plans, handling tasks with more than $10^{12}$ plans.","feed_headline":"Counting plans beats enumerating them at 10^12 plans","feed_subtitle":"A planning task compiled to a d-DNNF answers counts, probabilities, and facet queries without listing plans.","key_machinery":"The load-bearing object is the sequential SAT encoding $F^{\\mathrm{plan}}_{\\le\\ell}[\\Pi]$: a CNF formula whose variables name state variables and operators at each time step up to $\\ell$, with clauses for the initial state, goal, no two operators at one step, and successor-state consistency, plus a padding condition that moves unused steps to the end so that satisfying assignments correspond one-to-one to plans of length at most $\\ell$. The paper compiles this formula into a d-DNNF (a decomposable negation normal form, a rooted DAG whose conjunction nodes have disjoint variable sets and whose disjunctions are deterministic), on which model counting, conditioning on literals, backbone extraction, and uniform sampling run in polynomial time. The d-DNNF does the work: one compilation answers any number of later queries, turning the hard counting problem into a one-time compilation cost plus cheap graph traversals.","core_discovery":"On its own terms, the paper's discovery is a complete complexity map for reasoning over polynomially bounded plan spaces, together with a compilation pipeline that makes part of that map practical. The map reads: $\\#\\mathrm{Poly}$-Bounded-Plan is $\\#\\mathrm{P}$-complete; $\\mathrm{Poly}$-Probabilistic-Reason, the problem of deciding whether the fraction of plans satisfying a CNF query equals a rational $p$, is $\\mathrm{C}_{=}\\mathrm{P}$-complete; FacetReason, deciding whether an operator is a facet (in some bounded-length plan but not all), is $\\mathrm{NP}$-complete; and Exact-$k$-Facets is $\\mathrm{DP}$-complete. The paper further claims that a d-DNNF compiled from the sequential SAT encoding $F^{\\mathrm{plan}}_{\\le\\ell}[\\Pi]$ supports exact plan counting, conditioning-based probability queries, backbone-style brave and cautious queries, and uniform sampling, each in polynomial time after compilation. Empirically, the claim is that this counting mode outperforms enumeration-based top-quality planners as the length bound grows, including benchmark tasks with more than $10^{12}$ plans.","pith_inferences":["We infer that the one-to-one padding convention is the hinge of the whole pipeline: any move to a more compact parallel SAT encoding would require re-proving the correspondence before counts from the compiled diagram could be trusted.","An untested but natural next step is to use facet significance as a feature for learning pruning functions and for choosing the next operator in greedily constructed plans; the paper motivates this but does not evaluate it.","A testable extension is to compare exact d-DNNF-conditioned probabilities against approximate model counters on plan spaces between $10^6$ and $10^{12}$ plans, since exact $\\mathrm{C}_{=}\\mathrm{P}$ reasoning is likely to be the practical bottleneck.","Because uniform sampling from the d-DNNF is cheap, the same pipeline could correct the sampling bias known to affect plan-generation benchmarks; the paper mentions unbiased sampling but reports no sampling experiments."],"forward_implications":["Counting plans of length at most a polynomial bound is $\\#\\mathrm{P}$-complete, so no general polynomial-time exact counter exists under standard assumptions; the practical route must be compilation or approximation.","Asking for the probability of a query over the plan space is strictly harder than counting, so probability queries should be answered from two exact counts or from the compiled d-DNNF rather than by enumeration.","Facet membership is only $\\mathrm{NP}$-complete, so many plan-space navigation and significance questions can be answered without counting, enabling interactive exploration of spaces too large to enumerate.","Planalyst's counting mode solves more benchmark tasks than enumeration-based top-quality planners as the length bound grows, and the advantage widens with the bound, consistent with counting dominating enumeration once the plan space explodes.","Once a d-DNNF is built, brave and cautious operator queries and uniform plan sampling have negligible additional cost, giving explainability and unbiased data-collection applications for free."],"supporting_citations":[{"why":"Establishes NP-completeness of bounded plan existence and supplies the reduction template that the new hardness proofs extend.","marker":"[Bylander, 1994]"},{"why":"Shows #Poly-Bounded-Plan is #P-complete and Poly-Bounded-Top-k-Exist is PP-hard; provides the parsimonious planning reduction used in the new hardness proofs and the symbolic counting baseline.","marker":"[Speck et al., 2020]"},{"why":"Supplies the knowledge compilation map and the d-DNNF tractability guarantees that make counting and conditioning polynomial after compilation.","marker":"[Darwiche and Marquis, 2002]"},{"why":"Introduces planning as satisfiability, the basis of the sequential encoding $F^{\\mathrm{plan}}_{\\le\\ell}[\\Pi]$.","marker":"[Kautz and Selman, 1992]"},{"why":"Defines the class $\\mathrm{C}_{=}\\mathrm{P}$ used in Theorem 9 and provides the equal-accepting-and-rejecting-paths characterization that the reduction targets.","marker":"[Fenner et al., 1999]"},{"why":"Defines the class DP and the facets notion that the paper adapts to planning; used for the Exact-k-Facets classification.","marker":"[Papadimitriou and Yannakakis, 1982]"},{"why":"Supplies the CNF-to-d-DNNF compiler used in the Planalyst pipeline to build the decision diagram.","marker":"[Lagniez and Marquis, 2017]"},{"why":"Supplies the reasoning engine that executes counting, backbone, and uniform-sampling queries on the compiled d-DNNF.","marker":"[Sundermann et al., 2024]"},{"why":"Supplies a top-k enumeration planner used as one of the main empirical baselines that Planalyst is compared against.","marker":"[Katz et al., 2018]"},{"why":"Supplies the SAT-based grounding and encoding front end used to build the planning formula in the implementation.","marker":"[Rintanen, 2014]"}],"fun_headline_variants":["Plan reasoning complexity fully mapped","Count plans without enumerating them","Compile plan tasks to count plans","Facet queries reveal operator significance","Plan counting scales beyond 10^12"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the propositional formula built from the planning task has exactly one satisfying assignment for every plan of length at most the bound, with unused steps padded to the end, and no satisfying assignment for anything that is not a plan.","fun_headline_variants_meta":{"raw":{"variants":["Plan reasoning complexity fully mapped","Count plans without enumerating them","Compile plan tasks to count plans","Facet queries reveal operator significance","Plan counting scales beyond 10^12"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000406,"raw_usage":{"total_tokens":2119,"prompt_tokens":959,"completion_tokens":1160,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":575,"completion_tokens_details":{"reasoning_tokens":1102}},"tokens_in":575,"tokens_out":1160,"duration_ms":12331,"temperature":1.0,"reasoning_tokens":1102,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-09T20:01:48.610189+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run Planalyst on the paper's running example, whose plan space at bound 4 has exactly two plans; any reported count other than 2 falsifies the encoding-plus-compilation claim. For a sharper test, take a task with exactly one plan of length $\\ell-1$ and ask the count at bound $\\ell$: the padding convention forces exactly one model, so any count other than 1 means the one-to-one correspondence fails.","supporting_citations":[{"cited_title":"A knowledge compilation map","cited_arxiv_id":null,"evidence_quote":"Supplies the knowledge compilation map and the d-DNNF tractability guarantees that make counting and conditioning polynomial after compilation."},{"cited_title":"Planning as satisfiability","cited_arxiv_id":null,"evidence_quote":"Introduces planning as satisfiability, the basis of the sequential encoding $F^{\\mathrm{plan}}_{\\le\\ell}[\\Pi]$."},{"cited_title":"An improved decision- DNNF compiler","cited_arxiv_id":null,"evidence_quote":"Supplies the CNF-to-d-DNNF compiler used in the Planalyst pipeline to build the decision diagram."},{"cited_title":"Reusing d- DNNFs for efficient feature-model counting","cited_arxiv_id":null,"evidence_quote":"Supplies the reasoning engine that executes counting, backbone, and uniform-sampling queries on the compiled d-DNNF."},{"cited_title":"A novel iterative approach to top-k planning","cited_arxiv_id":null,"evidence_quote":"Supplies a top-k enumeration planner used as one of the main empirical baselines that Planalyst is compared against."},{"cited_title":"Madagascar: Scalable planning with SAT","cited_arxiv_id":null,"evidence_quote":"Supplies the SAT-based grounding and encoding front end used to build the planning formula in the implementation."}],"review_version":1}