Pith. sign in

REVIEW 3 major objections 5 minor 100 references

Counting and Reasoning with Plans

T0 review · 3 major / 5 minor · reviewed 2026-08-09 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2502.00145 v1 pith:5KPAZUQR submitted 2025-01-31 cs.AI

David Speck , Markus Hecher , Daniel Gnad , Johannes K. Fichte , Augusto B. Corrêa This is my paper · ORCID
classification cs.AI MSC 68Q1768T20
keywords classicalplanningplancountingmodelknowledgecompilationd-DNNFfacetreasoningcomplexityclassificationprobabilistic
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

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.

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 (3)
  1. [Section 2 (Planning as Satisfiability)] 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.
  2. [Appendix B (Lemma 6 and Lemma 11)] 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.
  3. [Section 6 (Empirical Evaluation)] 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.
minor comments (5)
  1. [Section 2] 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.
  2. [Appendix B, Lemma 6] The formula in the proof includes 'o_ℓ' which should be 'o_i' to range over all time points.
  3. [Theorem 13] The statement 'Let Π be a program' should read 'Let Π be a planning task'.
  4. [Section 2] The formal definition of F_plan≤ℓ is only sketched; please state the full clause set or give a reference that specifies it.
  5. [Section 4] The significance measure Sℓ(Π,o) is defined but not demonstrated; a small example or empirical illustration would improve readability.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: theoretical results reduce to published prior work and parsimonious reductions, and the SAT-model/plan bijection is an unproven correctness assumption rather than a circular one.

full rationale

The paper's derivation chain is not circular in the sense of defining its conclusions into its inputs. The complexity results in Theorems 9, 10, 11, and 13 are obtained by standard reductions from or to known problems: Poly-Brave-Plan-Exist and Poly-Cautious-Plan-Exist reduce to SAT via the planning-to-SAT encoding (Lemma 6); Poly-Probabilistic-Reason is shown C=P-complete by a parsimonious Cook-Levin reduction to a C=P-hard equality-of-paths problem and a membership argument reducing the probability query to equality of two counts (Theorem 9); FacetReason and the facet-counting problems reduce from SAT via a parsimonious planning reduction cited to Speck et al. 2020 and Bylander 1994. Some of these prior results are co-authored by current authors, but they are peer-reviewed, externally published results used as baselines and reduction sources, not as unverified assumptions of the paper's own conclusions. The practical claims rely on the asserted one-to-one correspondence between models of F_plan≤ℓ[Π] and plans of length at most ℓ. Section 2 states this correspondence but does not prove it, and Section 6.3 notes that other encodings 'lose the one-to-one correspondence between plans and SAT models.' That is a genuine correctness risk for the empirical pipeline, but it is not circularity: the number of plans is not defined as the number of SAT models, and the paper's comparisons to the independent enumeration-based planners K* and SymK provide an external check on the counts. No fitted parameter is renamed as a prediction, no self-citation is used as the sole load-bearing support for the central claims, and no known result is merely relabeled as unification. Therefore the circularity score is low.

Assumptions & free parameters 1 free parameters · 4 assumptions · 0 invented entities

The central theoretical claims do not fit any numeric parameters. They rely on the exactness of the SAT-to-plan encoding and on prior parsimonious reductions for hardness. The main experimental knob is the length-bound multiplier, reported for all values. No new ontological entities are introduced; facet is a defined reasoning mode, not a new entity.

free parameters (1)
  • length-bound multiplier c = 1.0, 1.1, 1.2, 1.3, 1.4, 1.5
    Hand-chosen experimental parameter in Section 6.1 that scales the per-task plan length bound before counting; it directly shapes all coverage and plan-count statistics, though it is disclosed for every value rather than fitted to make a point.
assumptions (4)
  • domain assumption The sequential SAT encoding F_plan<=l[Pi] is a one-to-one correspondence between satisfying assignments and plans of length at most l.
    Introduced in Section 2 under 'Planning as Satisfiability'; the padding convention moves unused steps to the end. All counting, probability, and facet queries inherit this bijection, so any duplicate or missing model changes every result.
  • standard math Parsimonious reductions from SAT and Turing-machine counting to planning preserve solution counts exactly.
    Used in Appendix B hardness proofs (Theorems 9, 10, Lemma 11) via Bylander (1994) and Speck et al. (2020); if these reductions are not parsimonious, the completeness claims weaken.
  • domain assumption Only polynomially bounded plan lengths are considered (l <= ||Pi||^c).
    The scope in the abstract and Table 1; this restriction is what makes Poly-Bounded-Plan-Exist NP-complete instead of PSPACE-complete, so the complexity results do not transfer to unbounded plans.
  • domain assumption Empirical benchmark tasks are optimal IPC domains with unit operator costs and without conditional effects or axioms.
    Stated in Section 6.1; the experimental comparison and the practical claims about scalability are limited to this task family.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Counting and Reasoning with Plans." pith.science (2026). https://pith.science/paper/5KPAZUQR

@misc{pith2026250200145,
  author       = {Pith},
  title        = {Pith review of: Counting and Reasoning with Plans},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/5KPAZUQR}},
  note         = {Machine review of arXiv:2502.00145}
}
read the original abstract

Classical planning asks for a sequence of operators reaching a given goal. While the most common case is to compute a plan, many scenarios require more than that. However, quantitative reasoning on the plan space remains mostly unexplored. A fundamental problem is to count plans, which relates to the conditional probability on the plan space. Indeed, qualitative and quantitative approaches are well-established in various other areas of automated reasoning. We present the first study to quantitative and qualitative reasoning on the plan space. In particular, we focus on polynomially bounded plans. On the theoretical side, we study its complexity, which gives rise to rich reasoning modes. Since counting is hard in general, we introduce the easier notion of facets, which enables understanding the significance of operators. On the practical side, we implement quantitative reasoning for planning. Thereby, we transform a planning task into a propositional formula and use knowledge compilation to count different plans. This framework scales well to large plan spaces, while enabling rich reasoning capabilities such as learning pruning functions and explainable planning.

Figures

Figures reproduced from arXiv: 2502.00145 by the authors.

Figure 1
Figure 1. State space of our running example task Π [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Quantitative reasoning is a fine-grained reasoning mode be [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

100 extracted references · 79 canonical work pages

  1. [1]

    Faceted answer-set navigation

    Christian Alrabbaa, Sebastian Rudolph, and Lukas Schweizer. Faceted answer-set navigation. In Proc.\ RuleML+RR 2018 , pages 211--225, 2018

    2018

  2. [2]

    Advances in WASP

    Mario Alviano, Carmine Dodaro, Nicola Leone, and Francesco Ricca. Advances in WASP . In Francesco Calimeri, Giovambattista Ianni, and Miroslaw Truszczynski, editors, Proceedings of the Thirteenth Conference on Programming and Nonmonotonic Reasoning (LPNMR 2015) , pages 40--54, 2015

    2015

  3. [3]

    Inconsistency proofs for ASP: the ASP - DRUPE format

    Mario Alviano, Carmine Dodaro, Johannes Klaus Fichte, Markus Hecher, Tobias Philipp, and Jakob Rath. Inconsistency proofs for ASP: the ASP - DRUPE format. Theory Pract. Log. Program. , 19(5-6):891--907, 2019

    2019

  4. [4]

    ASP and subset minimality: Enumeration, cautious reasoning and MUS es

    Mario Alviano, Carmine Dodaro, Salvatore Fiorentino, Alessandro Previti, and Francesco Ricca. ASP and subset minimality: Enumeration, cautious reasoning and MUS es. Artificial Intelligence , 320:103931, 2023

    2023

  5. [5]

    Optimizing planning domains by automatic action schema splitting

    Carlos Areces, Facundo Bustos, Mart \' n Ariel Dominguez, and J \"o rg Hoffmann. Optimizing planning domains by automatic action schema splitting. In Steve Chien, Alan Fern, Wheeler Ruml, and Minh Do, editors, Proceedings of the Twenty-Fourth International Conference on Automated Planning and Scheduling (ICAPS 2014) , pages 11--19. AAAI Press, 2014

    2014

  6. [6]

    Partial grounding in planning using small language models

    Felipe Areces, Benjamin Ocampo, Carlos Areces, Mart \' n Dom \' nguez, and Daniel Gnad. Partial grounding in planning using small language models. In ICAPS 2023 Workshop on Knowledge Engineering for Planning and Scheduling , 2023

    2023

  7. [7]

    On the glucose SAT solver

    Gilles Audemard and Laurent Simon. On the glucose SAT solver. Int. J. Artif. Intell. Tools , 27(1):27, 2018

    2018

  8. [8]

    A new exact solver for (weighted) max \# sat

    Gilles Audemard, Jean - Marie Lagniez, and Marie Miceli. A new exact solver for (weighted) max \# sat. In Frisch and Gregory sat2022 , pages 28:1--28:20

Show all 100 references
  1. [9]

    Stable model counting and its application in probabilistic logic programming

    Rehan Abdul Aziz, Geoffrey Chu, Christian Muise, and Peter Stuckey. Stable model counting and its application in probabilistic logic programming. In Blai Bonet and Sven Koenig, editors, Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence ( AAAI 2015) , p...

    2015

  2. [10]

    Learning planning domains from non-redundant fully-observed traces: Theoretical foundations and complexity analysis

    Pascal Bachor and Gregor Behnke. Learning planning domains from non-redundant fully-observed traces: Theoretical foundations and complexity analysis. In Dy and Natarajan aaai2024 , pages 20028--20035

  3. [11]

    CadiBack : Extracting backbones with CaDiCaL

    Armin Biere, Nils Froleyks, and Wenxi Wang. CadiBack : Extracting backbones with CaDiCaL . In Mahajan and Slivovsky sat2023 , pages 3:1--3:12

  4. [12]

    Course of action generation for cyber security using classical planning

    Mark Boddy, Johnathan Gohde, Tom Haigh, and Steven Harp. Course of action generation for cyber security using classical planning. In Susanne Biundo, Karen Myers, and Kanna Rajan, editors, Proceedings of the Fifteenth International Conference on Automated Planning and Schedulin...

    2005

  5. [13]

    Representative answer sets: Collecting something of everything

    Elisa B \" o hl, Sarah Alice Gaggl, and Dominik Rusovac. Representative answer sets: Collecting something of everything. In Kobi Gal, Ann Now \'e , Grzegorz J. Nalepa, Roy Fairstein, and Roxana R a dulescu, editors, Proceedings of the 26th European Conference on Artificial Int...

    2023

  6. [14]

    Policies that generalize: Solving many planning problems with the same policy

    Blai Bonet and Hector Geffner. Policies that generalize: Solving many planning problems with the same policy. In Qiang Yang and Michael Wooldridge, editors, Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI 2015) , pages 2798--2804. AAAI ...

    2015

  7. [15]

    The computational complexity of propositional STRIPS planning

    Tom Bylander. The computational complexity of propositional STRIPS planning. Artificial Intelligence , 69(1--2):165--204, 1994

    1994

  8. [16]

    A system for explainable answer set programming

    Pedro Cabalar, Jorge Fandinno, and Brais Mu \ n iz. A system for explainable answer set programming. Electronic Proceedings in Theoretical Computer Science , 325:124--136, September 2020

    2020

  9. [17]

    Interactive plan selection using linear temporal logic, disjunctive action landmarks, and natural language instruction

    Tathagata Chakraborti, Jungkoo Kang, Francesco Fuggitti, Michael Katz, and Shirin Sohrabi. Interactive plan selection using linear temporal logic, disjunctive action landmarks, and natural language instruction. In Dy and Natarajan aaai2024 , pages 23775--23777

  10. [18]

    Chen, Sylvie Thi \'e baux, and Felipe Trevizan

    Dillon Z. Chen, Sylvie Thi \'e baux, and Felipe Trevizan. Learning domain-independent heuristics for grounded and lifted planning. In Dy and Natarajan aaai2024 , pages 20078--20086

  11. [19]

    Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence ( AAAI 2020)

    Vincent Conitzer and Fei Sha, editors. Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence ( AAAI 2020) . AAAI Press, 2020

    2020

  12. [20]

    Stephen A. Cook. The complexity of theorem-proving procedures. In Michael A. Harrison, Ranan B. Banerji, and Jeffrey D. Ullman, editors, Proceedings of the 3rd Annual ACM Symposium on the Theory of Computing (STOC 1971) , pages 151--158. ACM , 1971

    1971

  13. [21]

    Corr \^e a, Markus Hecher, Malte Helmert, Davide Mario Longo, Florian Pommerening, and Stefan Woltran

    Augusto B. Corr \^e a, Markus Hecher, Malte Helmert, Davide Mario Longo, Florian Pommerening, and Stefan Woltran. Grounding planning tasks using tree decompositions and iterated solving. In Koenig et al. icaps2023

  14. [22]

    A knowledge compilation map

    Adnan Darwiche and Pierre Marquis. A knowledge compilation map. Journal of Artificial Intelligence Research , 17:229--264, 2002

    2002

  15. [23]

    Knowledge compilation

    Adnan Darwiche and Pierre Marquis. Knowledge compilation. Annals of Mathematics and Artificial Intelligence , 2024

    2024

  16. [24]

    Compiling knowledge into decomposable negation normal form

    Adnan Darwiche. Compiling knowledge into decomposable negation normal form. In Thomas Dean, editor, Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence ( IJCAI 1999) , pages 284--289. Morgan Kaufmann, 1999

    1999

  17. [25]

    Decomposable negation normal form

    Adnan Darwiche. Decomposable negation normal form. Journal of the ACM , 48(4):608--647, 2001

    2001

  18. [26]

    On the tractable counting of theory models and its application to truth maintenance and belief revision

    Adnan Darwiche. On the tractable counting of theory models and its application to truth maintenance and belief revision. Journal of Applied Non-Classical Logics , 11(1-2):11--34, 2001

    2001

  19. [27]

    New advances in compiling CNF into decomposable negation normal form

    Adnan Darwiche. New advances in compiling CNF into decomposable negation normal form. In Ram \' o n L \' o pez de M \' a ntaras and Lorenza Saitta, editors, Proceedings of the 16th Eureopean Conference on Artificial Intelligence, ( ECAI 2004), Valencia, Spain, August 22-27, 20...

    2004

  20. [28]

    Probabilistic planning via heuristic forward search and weighted model counting

    Carmel Domshlak and J \" o rg Hoffmann. Probabilistic planning via heuristic forward search and weighted model counting. Journal of Artificial Intelligence Research , 30:565--620, 2007

    2007

  21. [29]

    Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence ( AAAI 2024)

    Jennifer Dy and Sriraam Natarajan, editors. Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence ( AAAI 2024) . AAAI Press, 2024

    2024

  22. [30]

    A new approach to plan-space explanation: Analyzing plan-property dependencies in oversubscription planning

    Rebecca Eifler, Michael Cashmore, J \" o rg Hoffmann, Daniele Magazzeni, and Marcel Steinmetz. A new approach to plan-space explanation: Analyzing plan-property dependencies in oversubscription planning. In Conitzer and Sha aaai2020 , pages 9818--9826

  23. [31]

    Epistemic logic programs: Non-ground and counting complexity

    Thomas Eiter, Johannes Klaus Fichte, Markus Hecher, and Stefan Woltran. Epistemic logic programs: Non-ground and counting complexity. In Kate Larson, editor, Proceedings of the 32nd International Joint Conference on Artificial Intelligence (IJCAI 2024) , pages 3333--3341. ijca...

    2024

  24. [32]

    aspmc: New frontiers of algebraic answer set counting

    Thomas Eiter, Markus Hecher, and Rafael Kiesel. aspmc: New frontiers of algebraic answer set counting. Artificial Intelligence , 330:104109, 2024

    2024

  25. [33]

    Optimizing the optimization of planning domains by automatic action schema splitting

    Mojtaba Elahi and Jussi Rintanen. Optimizing the optimization of planning domains by automatic action schema splitting. In Dy and Natarajan aaai2024 , pages 20096--20103

  26. [34]

    Fenner, Frederic Green, Steven Homer, and Randall Pruim

    Stephen A. Fenner, Frederic Green, Steven Homer, and Randall Pruim. Determining acceptance possibility for a quantum computation is hard for the polynomial hierarchy. ECCC , TR99-003 , 1999

    1999

  27. [35]

    Answer set solving with bounded treewidth revisited

    Johannes Klaus Fichte, Markus Hecher, Michael Morak, and Stefan Woltran. Answer set solving with bounded treewidth revisited. In Marcello Balduccini and Tomi Janhunen, editors, Proceedings of the Fourteenth Conference on Programming and Nonmonotonic Reasoning (LPNMR 2017) , pa...

    2017

  28. [36]

    Fichte, Markus Hecher, and Florim Hamiti

    Johannes K. Fichte, Markus Hecher, and Florim Hamiti. The model counting competition 2020. ACM Journal of Experimental Algorithmics , 26(13):1--26, 2021

    2020

  29. [37]

    Rushing and strolling among answer sets -- navigation made easy

    Johannes Klaus Fichte, Sarah Alice Gaggl, and Dominik Rusovac. Rushing and strolling among answer sets -- navigation made easy. In Honavar and Spaan aaai2022 , pages 5651--5659

  30. [38]

    Johannes Klaus Fichte, Markus Hecher, and Mohamed A. Nadeem. Plausibility reasoning via projected answer set counting - A hybrid approach. In Luc De Raedt , editor, Proceedings of the 31st International Joint Conference on Artificial Intelligence (IJCAI 2022) , pages 2620--262...

    2022

  31. [39]

    Proofs for propositional model counting

    Johannes Klaus Fichte, Markus Hecher, and Valentin Roland. Proofs for propositional model counting. In Frisch and Gregory sat2022 , pages 30:1--30:24

  32. [40]

    IASCAR: incremental answer set counting by anytime refinement

    Johannes Klaus Fichte, Sarah Alice Gaggl, Markus Hecher, and Dominik Rusovac. IASCAR: incremental answer set counting by anytime refinement. Theory Pract. Log. Program. , 24(2):505--532, 2024

    2024

  33. [41]

    Benton, and Christian Muise

    Jeremy Frank, Alison Paredes, J. Benton, and Christian Muise. Bias in planning algorithms. In ICAPS Workshop on Reliable Data-Driven Planning and Scheduling (RDDPS) , 2024

    2024

  34. [42]

    Frisch and Peter Gregory, editors

    Alan M. Frisch and Peter Gregory, editors. Proceedings of Twenty-Fifth International Conference on Theory and Applications of Satisfiability Testing (SAT 2022) . Schloss Dagstuhl -- Leibniz-Zentrum f \"u r Informatik, 2022

    2022

  35. [43]

    Solution enumeration for projected boolean search problems

    Martin Gebser, Benjamin Kaufmann, and Torsten Schaub. Solution enumeration for projected boolean search problems. In Willem Jan van Hoeve and John N. Hooker, editors, Proceedings of the 6th International Conference on Integration of AI and OR Techniques in Constraint Programmi...

    2009

  36. [44]

    Advances in gringo series 3

    Martin Gebser, Roland Kaminski, Arne K \"o nig, and Torsten Schaub. Advances in gringo series 3. In James P. Delgrande and Wolfgang Faber, editors, Proceedings of the Eleventh Conference on Programming and Nonmonotonic Reasoning (LPNMR 2011) , pages 345--351, 2011

    2011

  37. [45]

    Clingo = ASP + control: Preliminary report

    Martin Gebser, Roland Kaminski, Benjamin Kaufmann, and Torsten Schaub. Clingo = ASP + control: Preliminary report. arXiv:1405.3694 [cs.PL], 2014

    2014 arXiv

  38. [46]

    Computational complexity of probabilistic turing machines

    John Gill. Computational complexity of probabilistic turing machines. SIAM Journal on Computing , 6(4):675--695, 1977

    1977

  39. [47]

    Learning how to ground a plan -- Partial grounding in classical planning

    Daniel Gnad, \'A lvaro Torralba, Mart \' n Ariel Dom \' nguez, Carlos Areces, and Facundo Bustos. Learning how to ground a plan -- Partial grounding in classical planning. In Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence ( AAAI 2019) , pages 7602--...

    2019

  40. [48]

    A planning approach to repair domains with incomplete action effects

    Alba Gragera, Raquel Fuentetaja, \' A ngel Garc \' a Olaya, and Fernando Fern \' a ndez. A planning approach to repair domains with incomplete action effects. In Koenig et al. icaps2023 , pages 153--161

  41. [49]

    Plingo: A System for Probabilistic Reasoning in Clingo Based on LP \( ^ MLN \)

    Susana Hahn, Tomi Janhunen, Roland Kaminski, Javier Romero, Nicolas R \" u hling, and Torsten Schaub. Plingo: A System for Probabilistic Reasoning in Clingo Based on LP \( ^ MLN \) . In Proc.\ RuleML+RR 2022 , pages 54--62, 2022

    2022

  42. [50]

    Malte Helmert and Carmel Domshlak. Landmarks, critical paths and abstractions: What's the difference anyway? In Alfonso Gerevini, Adele Howe, Amedeo Cesta, and Ioannis Refanidis, editors, Proceedings of the Nineteenth International Conference on Automated Planning and Scheduli...

    2009

  43. [51]

    The Fast Downward planning system

    Malte Helmert. The Fast Downward planning system. Journal of Artificial Intelligence Research , 26:191--246, 2006

    2006

  44. [52]

    Concise finite-domain representations for PDDL planning tasks

    Malte Helmert. Concise finite-domain representations for PDDL planning tasks. Artificial Intelligence , 173:503--535, 2009

    2009

  45. [53]

    Encoding lifted classical planning in propositional logic

    Daniel H \"o ller and Gregor Behnke. Encoding lifted classical planning in propositional logic. In Thi \'e baux and Yeoh icaps2022 , pages 134--144

  46. [54]

    Proceedings of the Thirty-Sixth AAAI Conference on Artificial Intelligence ( AAAI 2022)

    Vasant Honavar and Matthijs Spaan, editors. Proceedings of the Thirty-Sixth AAAI Conference on Artificial Intelligence ( AAAI 2022) . AAAI Press, 2022

    2022

  47. [55]

    Everardo, Ankit K

    Mohimenul Kabir, Flavio O. Everardo, Ankit K. Shukla, Markus Hecher, Johannes Klaus Fichte, and Kuldeep S. Meel. Approxasp - a scalable approximate answer set counter. In Honavar and Spaan aaai2022 , pages 5755--5764

  48. [56]

    Cost-optimal planning with landmarks

    Erez Karpas and Carmel Domshlak. Cost-optimal planning with landmarks. In Craig Boutilier, editor, Proceedings of the 21st International Joint Conference on Artificial Intelligence ( IJCAI 2009) , pages 1728--1733. AAAI Press, 2009

    2009

  49. [57]

    K* search over orbit space for top-k planning

    Michael Katz and Junkyu Lee. K* search over orbit space for top-k planning. In Edith Elkind, editor, Proceedings of the 32nd International Joint Conference on Artificial Intelligence (IJCAI 2023) . IJCAI, 2023

    2023

  50. [58]

    Reshaping diverse planning

    Michael Katz and Shirin Sohrabi. Reshaping diverse planning. In Conitzer and Sha aaai2020 , pages 9892--9899

  51. [59]

    A novel iterative approach to top-k planning

    Michael Katz, Shirin Sohrabi, Octavian Udrea, and Dominik Winterer. A novel iterative approach to top-k planning. In Mathijs de Weerdt, Sven Koenig, Gabriele R \"o ger, and Matthijs Spaan, editors, Proceedings of the Twenty-Eighth International Conference on Automated Planning...

    2018

  52. [60]

    Planning as satisfiability

    Henry Kautz and Bart Selman. Planning as satisfiability. In Bernd Neumann, editor, Proceedings of the 10th European Conference on Artificial Intelligence ( ECAI 1992) , pages 359--363. John Wiley and Sons, 1992

    1992

  53. [61]

    Knowledge compilation and more with SharpSAT-TD

    Rafael Kiesel and Thomas Eiter. Knowledge compilation and more with SharpSAT-TD . In Pierre Marquis, Tran Cao Son, and Gabriele Kern-Isberner, editors, Proceedings of the Twentieth International Conference on Principles of Knowledge Representation and Reasoning (KR 2023) , pag...

    2023

  54. [62]

    Propositional logic -- deduction and algorithms , volume 48 of Cambridge tracts in theoretical computer science

    Hans Kleine B \" u ning and Theodor Lettmann. Propositional logic -- deduction and algorithms , volume 48 of Cambridge tracts in theoretical computer science . Cambridge University Press, 1999

    1999

  55. [63]

    Proceedings of the Thirty-Third International Conference on Automated Planning and Scheduling (ICAPS 2023)

    Sven Koenig, Roni Stern, and Mauro Vallati, editors. Proceedings of the Thirty-Third International Conference on Automated Planning and Scheduling (ICAPS 2023) . AAAI Press, 2023

    2023

  56. [64]

    Learning pruning rules for heuristic search planning

    Michal Krajnansk \' y , J \" o rg Hoffmann, Olivier Buffet, and Alan Fern. Learning pruning rules for heuristic search planning. In Torsten Schaub, Gerhard Friedrich, and Barry O'Sullivan, editors, Proceedings of the 21st European Conference on Artificial Intelligence ( ECAI 2...

    2014

  57. [65]

    Benjamin Krarup, Senka Krivic, Daniele Magazzeni, Derek Long, Michael Cashmore, and David E. Smith. Contrastive explanations of plans through model restrictions. Journal of Artificial Intelligence Research , 72:533--612, 2021

    2021

  58. [66]

    An improved decision- DNNF compiler

    Jean - Marie Lagniez and Pierre Marquis. An improved decision- DNNF compiler. In Carles Sierra, editor, Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI 2017) , pages 667--673. IJCAI, 2017

    2017

  59. [67]

    Meel, and Roland H

    Yong Lai, Kuldeep S. Meel, and Roland H. C. Yap. The power of literal equivalence in model counting. In Kevin Leyton-Brown and Mausam, editors, Proceedings of the Thirty-Fifth AAAI Conference on Artificial Intelligence ( AAAI 2021) , pages 3851--3859. AAAI Press, 2021

    2021

  60. [68]

    Towards automated modeling assistance: An efficient approach for repairing flawed planning domains

    Songtuan Lin, Alban Grastien, and Pascal Bercher. Towards automated modeling assistance: An efficient approach for repairing flawed planning domains. In Yiling Chen and Jennifer Neville, editors, Proceedings of the Thirty-Seventh AAAI Conference on Artificial Intelligence ( AA...

    2023

  61. [69]

    Proceedings of Twenty-Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT 2023) , volume 271

    Meena Mahajan and Friedrich Slivovsky, editors. Proceedings of Twenty-Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT 2023) , volume 271. Schloss Dagstuhl -- Leibniz-Zentrum f \"u r Informatik, 2023

    2023

  62. [70]

    On CNF conversion for disjoint SAT enumeration

    Gabriele Masina, Giuseppe Spallitta, and Roberto Sebastiani. On CNF conversion for disjoint SAT enumeration. In Mahajan and Slivovsky sat2023 , pages 15:1--15:16

  63. [71]

    Reuth Mirsky, Sarah Keren, and Christopher W. Geib. Introduction to Symbolic Plan and Goal Recognition . Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan & Claypool Publishers, 2021

    2021

  64. [72]

    Planning.Domains

    Christian Muise. Planning.Domains . In ICAPS 2016 System Demonstrations and Exhibits , 2016

    2016

  65. [73]

    Papadimitriou and Mihalis Yannakakis

    Christos H. Papadimitriou and Mihalis Yannakakis. The complexity of facets (and some facets of complexity). In Harry R. Lewis, Barbara B. Simons, Walter A. Burkhard, and Lawrence H. Landweber, editors, Proceedings of the Fourteenth Annual ACM Symposium on the Theory of Computi...

    1982

  66. [74]

    Papadimitriou

    Christos H. Papadimitriou. Computational Complexity . Addison-Wesley, 1994

    1994

  67. [75]

    Benton, and Christian Muise

    Alison Paredes, Jeremy Frank, J. Benton, and Christian Muise. Planning bias: Planning as a source of sampling bias. In ICAPS Workshop on Reliable Data-Driven Planning and Scheduling (RDDPS) , 2024

    2024

  68. [76]

    On the extraction, ordering, and usage of landmarks in planning

    Julie Porteous, Laura Sebastia, and J \"o rg Hoffmann. On the extraction, ordering, and usage of landmarks in planning. In Amedeo Cesta and Daniel Borrajo, editors, Proceedings of the Sixth European Conference on Planning ( ECP 2001) , pages 174--182. AAAI Press, 2001

    2001

  69. [77]

    Landmarks revisited

    Silvia Richter, Malte Helmert, and Matthias Westphal. Landmarks revisited. In Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence ( AAAI 2008) , pages 975--982. AAAI Press, 2008

    2008

  70. [78]

    Madagascar: Scalable planning with SAT

    Jussi Rintanen. Madagascar: Scalable planning with SAT . In IPC 2011 Planner Abstracts , pages 61--64, 2011

    2011

  71. [79]

    Planning as satisfiability: Heuristics

    Jussi Rintanen. Planning as satisfiability: Heuristics. Artificial Intelligence , 193:45--86, 2012

    2012

  72. [80]

    Madagascar: Scalable planning with SAT

    Jussi Rintanen. Madagascar: Scalable planning with SAT . In Eighth I nternational P lanning C ompetition ( IPC -8): Planner Abstracts , pages 66--70, 2014

    2014

  73. [81]

    Handbook of Automated Reasoning (in 2 volumes)

    John Alan Robinson and Andrei Voronkov, editors. Handbook of Automated Reasoning (in 2 volumes) . Elsevier and MIT Press, 2001

    2001

  74. [82]

    Dominik Rusovac, Markus Hecher, Martin Gebser, Sarah Alice Gaggl, and Johannes K. Fichte. Navigating and Querying Answer Sets: How Hard Is It Really and Why? In Magdalena Ortiz and Maurice Pagnucco, editors, Proceedings of the Twentieth International Conference on Principles o...

    2024

  75. [83]

    Artificial I ntelligence --- A Modern Approach

    Stuart Russell and Peter Norvig. Artificial I ntelligence --- A Modern Approach . Prentice Hall, 1995

    1995

  76. [84]

    Learning domain-independent planning heuristics with hypergraph networks

    William Shen, Felipe Trevizan, and Sylvie Thi \'e baux. Learning domain-independent planning heuristics with hypergraph networks. In J. Christopher Beck, Erez Karpas, and Shirin Sohrabi, editors, Proceedings of the Thirtieth International Conference on Automated Planning and S...

    2020

  77. [85]

    David E. Smith. Choosing objectives in over-subscription planning. In Shlomo Zilberstein, Jana Koehler, and Sven Koenig, editors, Proceedings of the Fourteenth International Conference on Automated Planning and Scheduling ( ICAPS 2004) , pages 393--401. AAAI Press, 2004

    2004

  78. [86]

    Riabov, Michael Katz, and Octavian Udrea

    Shirin Sohrabi, Anton V. Riabov, Michael Katz, and Octavian Udrea. An AI planning solution to scenario generation for enterprise risk management. In Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence ( AAAI 2018) , pages 160--167. AAAI Press, 2018

    2018

  79. [87]

    Disjoint partial enumeration without blocking clauses

    Giuseppe Spallitta, Roberto Sebastiani, and Armin Biere. Disjoint partial enumeration without blocking clauses. In Dy and Natarajan aaai2024

  80. [88]

    Symbolic top-k planning

    David Speck, Robert Mattm \"u ller, and Bernhard Nebel. Symbolic top-k planning. In Conitzer and Sha aaai2020 , pages 9967--9974

  81. [89]

    Fichte, and Augusto B

    David Speck, Markus Hecher, Daniel Gnad , Johannes K. Fichte, and Augusto B. Corr \^e a. Code, benchmarks and data for the aaai 2025 paper `` Counting and Reasoning with Plans ''. Zenodo, 2024

    2025

  82. [90]

    Stockmeyer and Albert R

    Larry J. Stockmeyer and Albert R. Meyer. Word problems requiring exponential time. In Alfred V. Aho, Allan Borodin, Robert L. Constable, Robert W. Floyd, Michael A. Harrison, Richard M. Karp, and H. Raymond Strong, editors, Proceedings of the 5th Annual ACM Symposium on the Th...

    1973

  83. [91]

    Stockmeyer

    Larry J. Stockmeyer. The polynomial-time hierarchy. Theoretical Computer Science , 3(1):1--22, 1976

    1976

  84. [92]

    Reusing d- DNNFs for efficient feature-model counting

    Chico Sundermann, Heiko Raab, Tobias Hess, Thomas Th \" u m, and Ina Schaefer. Reusing d- DNNFs for efficient feature-model counting. ACM Trans. Softw. Eng. Methodol , 2024

    2024

  85. [93]

    The 2023 International Planning Competition

    Ayal Taitler, Ron Alford, Joan Espasa, Gregor Behnke, Daniel Fi s er, Michael Gimelfarb, Florian Pommerening, Scott Sanner, Enrico Scala, Dominik Schreiber, Javier Segovia-Aguas, and Jendrik Seipp. The 2023 International Planning Competition . AI Magazine , pages 1--17, 2024

    2023

  86. [94]

    Proceedings of the Thirty-Second International Conference on Automated Planning and Scheduling (ICAPS 2022)

    Sylvie Thi \'e baux and William Yeoh, editors. Proceedings of the Thirty-Second International Conference on Automated Planning and Scheduling (ICAPS 2022) . AAAI Press, 2022

    2022

  87. [95]

    Efficient symbolic search for cost-optimal planning

    \'A lvaro Torralba, Vidal Alc\' a zar, Peter Kissmann, and Stefan Edelkamp. Efficient symbolic search for cost-optimal planning. Artificial Intelligence , 242:52--79, 2017

    2017

  88. [96]

    Understanding Inconsistency -- A Contribution to the Field of Non-monotonic Reasoning

    Markus Ulbricht. Understanding Inconsistency -- A Contribution to the Field of Non-monotonic Reasoning. PhD thesis, Universit \"a t Leipzig, 2019

    2019

  89. [97]

    Leslie G. Valiant. The complexity of computing the permanent. Theoretical Computer Science , 8:189--201, 1979

    1979

  90. [98]

    Loopless top-k planning

    Julian von Tschammer , Robert Mattm \"u ller, and David Speck. Loopless top-k planning. In Thi \'e baux and Yeoh icaps2022 , pages 380--384

  91. [99]

    Complete sets and the polynomial-time hierarchy

    Celia Wrathall. Complete sets and the polynomial-time hierarchy. Theoretical Computer Science , 3(1):23--33, 1976

    1976

  92. [100]

    Landmark extraction via planning graph propagation

    Lin Zhu and Robert Givan. Landmark extraction via planning graph propagation. In ICAPS 2003 Doctoral Consortium , pages 156--160, 2003

    2003

Pith tools

Reviewed August 9, 2026 · model on record in the stance chip above.