Pith. sign in

REVIEW 3 major objections 5 minor 66 references

Counting Answer Sets of Disjunctive Answer Set Programs

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

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

Pith's one-line read Counting the answer sets of a disjunctive logic program reduces to two propositional model-counting queries, with only polynomial growth in formula size.

desk verdict A solid, useful reduction for counting answer sets of disjunctive programs, with the main correctness lemma proved informally and a couple of experimental overclaims that should be tightened before publication. read the letter →

arxiv 2507.11655 v1 pith:MTAO5A5R submitted 2025-07-15 cs.LO cs.AI

Mohimenul Kabir , Supratik Chakraborty , Kuldeep S Meel This is my paper · ORCID
classification cs.LOcs.AI
keywords answersetcountingdisjunctivelogicprogramsprojectedmodelsubtractivereductionClarkcompletionloopatomsprogramming
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

This paper claims that counting answer sets of disjunctive logic programs—programs whose rules may put several atoms in the head—can be carried out by two calls to a propositional model counter, with no exponential blow-up in the formulas. The first call counts the models of the Clark completion, which overcounts the answer sets. The second call counts the surplus with a projected model count over a formula that renames the loop-atom rules into two fresh copies. Because the surplus is exact, subtracting it recovers the true answer-set count. If the reduction is correct, a counting problem previously considered beyond practical reach inherits the speed of modern projected model counters, and the paper's experiments report large gains on programs with very many answer sets.

What carries the argument

The load-bearing object is the copy operation $\mathrm{Copy}(P)$: for each loop atom $x$ it introduces a fresh variable $x'$, adds the implication $x' \to x$, and for every rule whose head contains a loop atom it rewrites the rule with loop atoms replaced by their copies. Lemma 2 states that after unit propagation under an interpretation $\tau_M$, the implications left in $\mathrm{Copy}(P)|_{\tau_M}$ coincide with the implications of the Gelfond-Lifschitz reduct $P^M$ restricted to loop atoms, up to renaming loop atoms by copy variables. This equivalence is what makes the surplus count exact, and it is why the reduction stays polynomial: only loop atoms, not the whole program, need duplicated rules.

What would settle it

Enumerate all interpretations $M$ with $\tau_M \models \mathrm{Comp}(P)$ for a nontrivial disjunctive program, compute both sides of Lemma 2's equivalence, and check for a mismatch; a single model where the satisfiability of $\mathrm{Copy}(P)|_{\tau_M} \wedge \bigvee_{x} \neg x'$ differs from the reduct's 'some loop atom unjustified' formula refutes Theorem 1.

Watch

Extended reading notes

Core claim

The central claim is Theorem 1: for every disjunctive logic program $P$, the number of answer sets is $|AS(P)| = \#\varphi_1 - \#\exists X\, \varphi_2$, where $\varphi_1 = \mathrm{Comp}(P)$ is the Clark completion, $\varphi_2$ is the formula in Equation (3) built from the completion plus two independent copy programs over the loop atoms, and $X$ is the set of all copy variables; both formulas are polynomial in $|P|$. The supporting characterization is Lemma 3: if an interpretation $M$ satisfies the completion, then $M$ is an answer set exactly when $\mathrm{Copy}(P)|_{\tau_M}$ together with the demand that some true loop atom has a false copy is unsatisfiable. This reduces the minimality check of answer-set semantics to a satisfiability test over a formula whose size does not depend on enumerating answer sets.

Load-bearing premise

The count is exact only if, for every interpretation satisfying the completion, the copied program and the reduct leave the same implications after simplification, and if the underlying projected counter returns exact counts.

Editorial extensions

If this is right

  • Every disjunctive answer-set count becomes an ordinary model count minus a projected model count, so advances in projected model counting translate directly into faster answer-set counting.
  • Programs with enormous answer-set counts become tractable: the reported experiments count instances with up to $2^{127}$ answer sets, where enumeration-based counters time out near $2^{30}$.
  • A hybrid that enumerates up to $10^4$ answer sets and then switches to the subtractive counter solves 918 of 1125 benchmark instances, versus 708 for pure enumeration.
  • The construction realizes a $\#\cdot\mathrm{coNP}$ counting problem through a $\#\mathrm{NP}$ projected-counting oracle, matching the known equality of these counting classes.

Reading between the lines

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

  • Beyond the paper, the same overcount-then-subtract pattern may apply to other $\#\cdot\mathrm{coNP}$ counting problems that admit a completion-style over-approximation and a cyclic reason for the surplus.
  • Because the formula size grows with the number of loop atoms rather than total atoms, I expect the practical bottleneck to shift to the projected counter; preprocessing that removes or breaks loops should therefore improve the method's reach.
  • The paper's benchmark table suggests performance degrades sharply when loop-atom counts exceed roughly 1000; a direct test would be to run the counter on programs whose loop-atom counts are artificially inflated without changing the answer-set count.
  • A formalized version of Lemma 2 would amount to a constructive membership proof for answer-set counting in $\#\mathrm{NP}$, making the complexity-theoretic soundness of the reduction fully syntactic.
Share X Bluesky LinkedIn Reddit HN

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 presents sharpASP-SR, a counter for disjunctive answer set programs based on a subtractive reduction to projected propositional model counting. The central theoretical result (Theorem 1) states that |AS(P)| = #Comp(P) − #∃(CV′∪CV⋆) φ2, where φ2 is built from two copies of the loop-atom copy program together with constraints that select exactly the surplus models of the Clark completion. The proof proceeds through an alternative characterization of answer sets (Lemma 3) that reduces answer-set checking to the unsatisfiability of a copy-formula over loop atoms. The paper also reports an implementation using GANAK and experiments on 1125 non-tight disjunctive instances, where sharpASP-SR solves 825 instances and a clingo-initialized hybrid solves 918, compared to 708 for clingo alone.

Significance. If the technical claims are correct, the paper makes a useful contribution: it gives a polynomial-size reduction from counting answer sets of disjunctive programs to two projected model-counting calls, thereby bringing the practical progress in #SAT to bear on a class that is harder than normal ASP counting. The availability of an implementation, benchmark suite, and a hybrid enumeration/counting scheme is a concrete strength. However, the correctness of the reduction rests on a proof of Lemma 2 that is only sketched informally, and the experimental pipeline leaves unspecified the exact CNF encoding used for the non-clausal Clark-completion formulas. These points need to be resolved before the contribution is fully secured.

major comments (3)
  1. [Section 5, Lemma 4] The proof of Lemma 4 only establishes that every model of φ2 projects to an interpretation M that is not an answer set. It does not establish the converse: for every M with τM |= Comp(P) and M ∉ AS(P), there exists at least one assignment to CV′ ∪ CV⋆ such that (M, assignment) |= φ2. This direction is needed for the equality #∃X φ2 = surplus. A construction exists (take the x′ assignment witnessing Lemma 3 and set x⋆ = 1 for x ∈ LA(P) with x ∈ M and x⋆ = 0 otherwise, using the fact that M |= P to satisfy Copy(P)⋆), but it should be stated explicitly.
  2. [Appendix B, Lemma 2] The proof of Lemma 2 is the load-bearing step for Theorem 1, but it is an informal fixed-point argument. The sentence 'Straightforwardly, the formula Copy(P)|τM is the conjuction of a set of unit clauses and implications...' skips the case analysis needed to establish the claimed renaming correspondence. In particular, the proof should cover rules whose heads contain both loop and non-loop atoms, rules whose head contains loop atoms that are false in M, type-1 implications x′→x interacting with type-2 copies of positive body occurrences, and rules with Head(r)∩LA(P)=∅ that are nevertheless relevant to the reduct P^M. Since Lemma 3 and Theorem 1 rest on this lemma, the proof should be a formal induction on unit propagation or at least a complete case analysis; alternatively, the authors should provide an exhaustive machine-checked verification over all small programs.
  3. [Section 5, Eq. (2)–(3), and Section 6] The paper does not specify how the formulas φ1 and φ2 are converted to the CNF input required by GANAK. Group 3 of Comp(P) is a disjunction of conjunctions for each atom a, so a direct CNF conversion can be exponential, while a Tseitin encoding with auxiliary variables changes the model count unless the auxiliary variables are projected away. The theorem's polynomial-size claim is for the non-CNF formulas; the implementation's actual encoding and the exact projection sets used for the GANAK calls (including whether auxiliary variables are projected out for φ1) are not described. This is necessary both for the correctness of the reported counts and for reproducibility. The authors should also state whether GANAK was run in an exact mode and what parameters were used, since the paper claims exact counting.
minor comments (5)
  1. [Section 6] The sentence 'The evaluation with All counters are sourced from the model counting competition 2024' is ungrammatical and should be rewritten; it is also unclear whether it refers to the baseline solvers or the benchmark instances.
  2. [Section 6] The phrase 'count instances upto 2^127 answer sets' should read 'up to'; there are also inconsistent superscript renderings such as '10 4' for the enumeration cutoff.
  3. [Section 5, comparison with Hecher and Kiesel] The statement that the authors of (Hecher and Kiesel 2023) confirmed by personal communication that they have not implemented the technique is not independently verifiable; it would be better to phrase this as 'no implementation is publicly available' or to cite a public artifact.
  4. [Appendix C] The heading 'Experimentals with Alternative Projected Model Counters' should be 'Experiments'; the same typo appears in 'Experimentals with 16 GB Memory Limit'.
  5. [Table 2] The column header 'clingo (≤ 104) +' is missing a superscript; it should read 'clingo (≤ 10^4) +' to match the description in the text.

Circularity Check

0 steps flagged · score 2.0 of 10

No load-bearing circularity: the subtractive counting theorem is derived in-paper from Lemmas 1-4, with only minor non-load-bearing self-citations and a benchmark-tuned hybrid threshold.

full rationale

The central claim, |AS(P)| = #Comp(P) - #∃Xφ2 (Theorem 1), is derived from Lemmas 1-4 whose proofs are contained in the paper (Section 4 and Appendix B); φ1 and φ2 are not restatements of the target count by construction, and the surplus formula is justified through Lemma 3 rather than assumed. The Copy(P) construction is credited to the authors' earlier normal-program work (Kabir et al. 2024; Kabir 2024), but it is fully re-defined in Section 4.2 and the disjunctive-case correspondence (Lemma 2) is argued in the appendix, not imported as a black-box result; the citations to Fichte and Szeider (2015) and Hecher and Kiesel (2023) are acknowledgments of similarity, not load-bearing dependencies. The weakest step is the informal fixed-point proof of Lemma 2, including the sentence 'Straightforwardly, the formula Copy(P)|τM is the conjunction of a set of unit clauses and implications, where these implications consist of only copy atoms such that their corresponding loop atoms are assigned to true in τM'; this is a rigor gap but not circularity, because the claim is being argued rather than assumed as the theorem's conclusion. The only circularity-adjacent issue is empirical: the hybrid's 10^4 cutoff is introduced after observing 'a noticeable shift was observed on clingo's runtime performance when the number of answer sets exceeds 10^4' on the same 1125 instances, and the hybrid's superiority is then reported on that same suite; this weakens the independence of the speedup claim but does not affect the correctness of the counting reduction. Overall, no derivation step reduces to its inputs by definition, so the circularity score is low.

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

The method adds one tuned engineering parameter (hybrid cutoff) and introduces auxiliary copy variables; it does not fit any physical constants. The main assumptions are standard ASP semantics and the correctness of the external projected counter GANAK.

free parameters (1)
  • hybrid enumeration cutoff = 10^4 answer sets
    The hybrid counter switches from clingo enumeration to sharpASP-SR after enumerating 10^4 answer sets; Section 6.1 says this cutoff was chosen because a noticeable shift in clingo's runtime was observed at that point, i.e., tuned on the evaluation instances.
assumptions (4)
  • domain assumption Answer sets are defined via the Gelfond-Lifschitz reduct and subset-minimality
    Section 2 states this as the standard ASP semantics used throughout.
  • domain assumption Every answer set satisfies the Clark completion, and for tight programs completion models are exactly answer sets
    Invoked in Sections 4 and 5, cited to Lee and Lifschitz 2003.
  • domain assumption The projected model counter GANAK returns exact projected counts
    sharpASP-SR uses GANAK as the backend (Section 6); if GANAK's counts are wrong, the reported answer-set counts inherit the error.
  • standard math Standard properties of unit propagation over implication clauses (fixed-point behavior used in Lemma 2's proof)
    The proof of Lemma 2 in Appendix B assumes that unit propagation removes satisfied clauses and propagates unit literals to a fixed point without producing empty clauses when τM |= Comp(P).
invented entities (1)
  • Copy variables x' and x* for each loop atom
    purpose: Auxiliary variables encoding whether a loop atom can be dropped during the minimality check; they enable the surplus count in φ2.
    These are internal to the reduction and have no observable handle outside the paper; they are legitimate construction devices, not empirically supported entities.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Counting Answer Sets of Disjunctive Answer Set Programs." pith.science (2026). https://pith.science/paper/MTAO5A5R

@misc{pith2026250711655,
  author       = {Pith},
  title        = {Pith review of: Counting Answer Sets of Disjunctive Answer Set Programs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/MTAO5A5R}},
  note         = {Machine review of arXiv:2507.11655}
}
read the original abstract

Answer Set Programming (ASP) provides a powerful declarative paradigm for knowledge representation and reasoning. Recently, counting answer sets has emerged as an important computational problem with applications in probabilistic reasoning, network reliability analysis, and other domains. This has motivated significant research into designing efficient ASP counters. While substantial progress has been made for normal logic programs, the development of practical counters for disjunctive logic programs remains challenging. We present SharpASP-SR, a novel framework for counting answer sets of disjunctive logic programs based on subtractive reduction to projected propositional model counting. Our approach introduces an alternative characterization of answer sets that enables efficient reduction while ensuring that intermediate representations remain of polynomial size. This allows SharpASP-SR to leverage recent advances in projected model counting technology. Through extensive experimental evaluation on diverse benchmarks, we demonstrate that SharpASP-SR significantly outperforms existing counters on instances with large answer set counts. Building on these results, we develop a hybrid counting approach that combines enumeration techniques with SharpASP-SR to achieve state-of-the-art performance across the full spectrum of disjunctive programs.

Figures

Figures reproduced from arXiv: 2507.11655 by the authors.

Figure 1
Figure 1. The high-level architecture of sharpASP-SR for a program P. Lemma 3 For a given program P and each interpretation M ⊆ at(P) such that τM |= Comp(P), M ∈ AS(P) if and only if the formula Copy(P)|τM ∧ W x∈τ + M∧x∈LA(P ) ¬x ′ is UNSAT. The proof follows directly from the correctness of Lemma 2, and from the definition of answer sets based on the Gelfond-Lifschitz reduct P M (see Section 2). Our alternative definition o… view at source ↗
Figure 2
Figure 2. The runtime performance of sharpASP-SR vis-a-vis other ASP counters. Given clingo’s superior performance on instances with few answer sets, we developed a hybrid counter integrating the strengths of clingo’s enumeration and other counting techniques, following the experimental evaluation of (Kabir et al. 2024). This hybrid approach first employs clingo enumeration (maximum 104 answer sets) and switches to alternativ… view at source ↗
Figure 3
Figure 3. The performance comparison of sharpASP-SR in terms of the number of answer sets. The x and y-axis indicate the number of instances and answer set count (in 2-base log scale), respectively. To analyze sharpASP-SR’s performance relative to |LA(P)|, we compared different ASP counters across varying ranges of loop atoms. The results in the [PITH_FULL_IMAGE:figures/full_fig_p014_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

66 extracted references · 65 canonical work pages

  1. [1]

    write newline

    " write newline "" before.all 'output.state := FUNCTION fin.entry add.period write newline FUNCTION new.block output.state before.all = 'skip after.block 'output.state := if FUNCTION new.sentence output.state after.block = 'skip output.state before.all = 'skip after.sentence 'output.state := if if FUNCTION not #0 #1 if FUNCTION and 'skip pop #0 if FUNCTIO...

  2. [2]

    , Amendola, G

    Alviano, M. , Amendola, G. , Dodaro, C. , Leone, N. , Maratea, M. , and Ricca, F. Evaluation of disjunctive programs in W asp. In LPNMR 2019, pp. 241--255. Springer

    work page 2019

  3. [3]

    , Dodaro, C

    Alviano, M. , Dodaro, C. , Leone, N. , and Ricca, F. Advances in W asp. In LPNMR 2015, pp. 40--54. Springer

    work page 2015

  4. [4]

    , Ricca, F

    Amendola, G. , Ricca, F. , and Truszczynski, M. Generating hard random boolean formulas and disjunctive logic programs. In IJCAI 2017, pp. 532--538

    work page 2017

  5. [5]

    Aziz, R. A. , Chu, G. , Muise, C. , and Stuckey, P. \# SAT : Projected model counting. In SAT 2015a, pp. 121--137. Springer

    work page

  6. [6]

    Aziz, R. A. , Chu, G. , Muise, C. , and Stuckey, P. J. Stable model counting and its application in probabilistic logic programming. In AAAI 2015b

    work page

  7. [7]

    , Heule, M

    Balyo, T. , Heule, M. J. , and J \"a rvisalo, M. SAT competition 2017--solver and benchmark descriptions. pp. 14--15 2017

    work page 2017

  8. [8]

    and Dechter, R

    Ben-Eliyahu, R. and Dechter, R. Propositional semantics for disjunctive logic programs. Annals of Mathematics and Artificial intelligence , 12:53--87 1994

    work page 1994

Show all 66 references
  1. [9]

    , Angiulli, F

    Ben-Eliyahu-Zohary, R. , Angiulli, F. , Fassetti, F. , and Palopoli, L. Modular construction of minimal models. In LPNMR 2017, pp. 43--48. Springer

    2017

  2. [10]

    and Meel, K

    Bend \' k, J. and Meel, K. S. Counting minimal unsatisfiable subsets. In CAV 2021, pp. 313--336. Springer

    2021

  3. [11]

    , Lagniez, J.-M

    Capelli, F. , Lagniez, J.-M. , Plank, A. , and Seidl, M. A top-down tree model counter for quantified boolean formulas. IJCAI 2024

    2024

  4. [12]

    Clark, K. L. Negation as failure. Logic and data bases , pp. 293--322 1978

    1978

  5. [13]

    , Hermann, M

    Durand, A. , Hermann, M. , and Kolaitis, P. G. Subtractive reductions and complete problems for counting complexity classes. Theoretical Computer Science , 340(3):496--513 2005

    2005

  6. [14]

    , Eiter, T

    Egly, U. , Eiter, T. , Tompits, H. , and Woltran, S. Solving advanced reasoning tasks using quantified boolean formulas. In AAAI/IAAI 2000, pp. 417--422

    2000

  7. [15]

    , Fink, M

    Eiter, T. , Fink, M. , Tompits, H. , and Woltran, S. On eliminating disjunctions in stable logic programming. KR , 4:447--458 2004

    2004

  8. [16]

    and Gottlob, G

    Eiter, T. and Gottlob, G. On the computational cost of disjunctive logic programming: Propositional case. Annals of Mathematics and Artificial Intelligence , 15:289--323 1995

    1995

  9. [17]

    , Hecher, M

    Eiter, T. , Hecher, M. , and Kiesel, R. Treewidth-aware cycle breaking for algebraic answer set counting. In KR 2021, pp. 269--279

    2021

  10. [18]

    , Hecher, M

    Eiter, T. , Hecher, M. , and Kiesel, R. aspmc: New frontiers of algebraic answer set counting. Artificial Intelligence , 330:104109 2024

    2024

  11. [19]

    Consistency of C lark's completion and existence of stable models

    Fages, F. Consistency of C lark's completion and existence of stable models. Journal of Methods of logic in computer science , 1(1):51--60 1994

    1994

  12. [20]

    and Schulz, C

    Fandinno, J. and Schulz, C. Answering the “why” in answer set programming--a survey of explanation approaches. TPLP , 19(2):114--203 2019

    2019

  13. [21]

    Fichte, J. K. , Gaggl, S. A. , Hecher, M. , and Rusovac, D. IASCAR : Incremental answer set counting by anytime refinement. TPLP , 24(3):505--532 2024

    2024

  14. [22]

    Fichte, J. K. , Gaggl, S. A. , and Rusovac, D. Rushing and strolling among answer sets--navigation made easy. In AAAI 2022, volume 36, pp. 5651--5659

    2022

  15. [23]

    Fichte, J. K. and Hecher, M. Treewidth and counting projected answer sets. In LPNMR 2019, pp. 105--119. Springer

    2019

  16. [24]

    Fichte, J. K. , Hecher, M. , Morak, M. , and Woltran, S. Answer set solving with bounded treewidth revisited. In LPNMR 2017, pp. 132--145

    2017

  17. [25]

    Fichte, J. K. and Szeider, S. Backdoors to normality for disjunctive logic programs. TOCL , 17(1):1--23 2015

    2015

  18. [26]

    Gaggl, S. A. , Manthey, N. , Ronca, A. , Wallner, J. P. , and Woltran, S. Improved answer set programming encodings for abstract argumentation. TPLP , 15(4-5):434--448 2015

    2015

  19. [27]

    , Kaufmann, B

    Gebser, M. , Kaufmann, B. , and Schaub, T. Conflict-driven answer set solving: From theory to practice. Artificial Intelligence , 187:52--89 2012

    2012

  20. [28]

    , Maratea, M

    Gebser, M. , Maratea, M. , and Ricca, F. The seventh answer set programming competition: Design and results. TPLP , 20(2):176--204 2020

    2020

  21. [29]

    , Schaub, T

    Gebser, M. , Schaub, T. , Thiele, S. , Usadel, B. , and Veber, P. Detecting inconsistencies in large biological networks with answer set programming. In ICLP 2008, pp. 130--144. Springer

    2008

  22. [30]

    and Lifschitz, V

    Gelfond, M. and Lifschitz, V. The stable model semantics for logic programming. In ICLP/SLP 1988, volume 88, pp. 1070--1080

    1988

  23. [31]

    and Lifschitz, V

    Gelfond, M. and Lifschitz, V. Classical negation in logic programs and disjunctive databases. New generation computing , 9:365--385 1991

    1991

  24. [32]

    Treewidth-aware reductions of normal ASP to SAT --is normal ASP harder than SAT after all? Artificial Intelligence , 304:103651 2022

    Hecher, M. Treewidth-aware reductions of normal ASP to SAT --is normal ASP harder than SAT after all? Artificial Intelligence , 304:103651 2022

    2022

  25. [33]

    and Kiesel, R

    Hecher, M. and Kiesel, R. The impact of structure in answer set counting: fighting cycles and its limits. In KR 2023, pp. 344--354

    2023

  26. [34]

    Hemaspaandra, L. A. and Vollmer, H. The satanic notations: counting classes beyond \# P and other definitional adventures. ACM SIGACT News , 26(1):2--13 1995

    1995

  27. [35]

    Some (in) translatability results for normal logic programs and propositional theories

    Janhunen, T. Some (in) translatability results for normal logic programs and propositional theories. Journal of Applied Non-Classical Logics , 16(1-2):35--86 2006

    2006

  28. [36]

    and Niemel \"a , I

    Janhunen, T. and Niemel \"a , I. 2011. Compact Translations of Non-disjunctive Answer Set Programs to Propositional Clauses , pp. 111--130

    2011

  29. [37]

    , Niemel \"a , I

    Janhunen, T. , Niemel \"a , I. , Seipel, D. , Simons, P. , and You, J.-H. Unfolding partiality and disjunctions in stable model semantics. TOCL , 7(1):1--37 2006

    2006

  30. [38]

    , Wan, H

    Ji, J. , Wan, H. , Wang, K. , Wang, Z. , Zhang, C. , and Xu, J. Eliminating disjunctions in answer set programming by restricted unfolding. In IJCAI 2016, pp. 1130--1137

    2016

  31. [39]

    Minimal model counting via knowledge compilation

    Kabir, M. Minimal model counting via knowledge compilation. arXiv preprint arXiv:2409.10170 2024

    2024 arXiv

  32. [40]

    , Chakraborty, S

    Kabir, M. , Chakraborty, S. , and Meel, K. S. Exact ASP counting with compact encodings. In AAAI 2024, volume 38, pp. 10571--10580

    2024

  33. [41]

    , Everardo, F

    Kabir, M. , Everardo, F. O. , Shukla, A. K. , Hecher, M. , Fichte, J. K. , and Meel, K. S. ApproxASP --a scalable approximate answer set counter. In AAAI 2022, pp. 5755--5764

    2022

  34. [42]

    and Meel, K

    Kabir, M. and Meel, K. S. A fast and accurate ASP counting based network reliability estimator. In LPAR 2023, pp. 270--287

    2023

  35. [43]

    and Meel, K

    Kabir, M. and Meel, K. S. On lower bounding minimal model count. TPLP , 24(4):586--605 2024

    2024

  36. [44]

    and Meel, K

    Kabir, M. and Meel, K. S. An ASP -based framework for MUS es. arXiv preprint arXiv:2507.03929 2025

    2025

  37. [45]

    , Trinh, V.-G

    Kabir, M. , Trinh, V.-G. , Pastva, S. , and Meel, K. S. Scalable counting of minimal trap spaces and fixed points in boolean networks. arXiv preprint arXiv:2506.06013 2025

    2025 arXiv

  38. [46]

    and Stuckey, P

    Kanchanasut, K. and Stuckey, P. J. Transforming normal logic programs to constraint logic programs. TCS , 105(1):27--56 1992

    1992

  39. [47]

    and Marquis, P

    Lagniez, J.-M. and Marquis, P. An improved decision- DNNF compiler. In IJCAI 2017, volume 17, pp. 667--673

    2017

  40. [48]

    and Marquis, P

    Lagniez, J.-M. and Marquis, P. A recursive algorithm for projected model counting. In AAAI 2019, volume 33, pp. 1536--1543

    2019

  41. [49]

    and Lifschitz, V

    Lee, J. and Lifschitz, V. Loop formulas for disjunctive logic programs. In ICLP 2003, pp. 451--465. Springer

    2003

  42. [50]

    , Talsania, S

    Lee, J. , Talsania, S. , and Wang, Y. Computing LPMLN using ASP and MLN solvers. Theory and Practice of Logic Programming , 17(5-6):942--960 2017

    2017

  43. [51]

    and Ricca, F

    Leone, N. and Ricca, F. Answer set programming: A tour from the basics to advanced development tools and industrial applications. In Reasoning web international summer school 2015, pp. 308--326. Springer

    2015

  44. [52]

    Cmodels -- SAT -based disjunctive answer set solver

    Lierler, Y. Cmodels -- SAT -based disjunctive answer set solver. In LPNMR 2005, pp. 447--451. Springer

    2005

  45. [53]

    Thirteen definitions of a stable model

    Lifschitz, V. Thirteen definitions of a stable model. Fields of logic and computation , pp. 488--503 2010

    2010

  46. [54]

    and Razborov, A

    Lifschitz, V. and Razborov, A. Why are there so many loop formulas? TOCL , 7(2):261--268 2006

    2006

  47. [55]

    Marek, V. W. and Truszczy \'n ski, M. Stable models and an alternative logic programming paradigm. In The Logic Programming Paradigm 1999, pp. 375--398. Springer

    1999

  48. [56]

    and Truszczy \'n ski, M

    Marek, W. and Truszczy \'n ski, M. Autoepistemic logic. Journal of the ACM (JACM) , 38(3):587--618 1991

    1991

  49. [57]

    , Balduccini, M

    Nogueira, M. , Balduccini, M. , Gelfond, M. , Watson, R. , and Barry, M. An A - P rolog decision support system for the space shuttle. In PADL 2001, pp. 169--183. Springer

    2001

  50. [58]

    , Son, T

    Pontelli, E. , Son, T. C. , and Elkhatib, O. Justifications for logic programs under answer set semantics. TPLP , 9(1):1--56 2009

    2009

  51. [59]

    , Hecher, M

    Rusovac, D. , Hecher, M. , Gebser, M. , Gaggl, S. A. , and Fichte, J. K. Navigating and querying answer sets: how hard is it really and why? In KR 2024, volume 21, pp. 642--653

    2024

  52. [60]

    , Roy, S

    Sharma, S. , Roy, S. , Soos, M. , and Meel, K. S. GANAK : A scalable probabilistic exact model counter. In IJCAI 2019, volume 19, pp. 1169--1176

    2019

  53. [61]

    , M \"o hle, S

    Shukla, A. , M \"o hle, S. , Kauers, M. , and Seidl, M. Outercount: A first-level solution-counter for quantified boolean formulas. In CICM 2022, pp. 272--284. Springer

    2022

  54. [62]

    , Hashimoto, K

    Suzuki, R. , Hashimoto, K. , and Sakai, M. 2017. Improvement of projected model-counting solver with component decomposition using sat solving in components. Technical report, JSAI

    2017

  55. [63]

    , Benhamou, B

    Trinh, G. , Benhamou, B. , Pastva, S. , and Soliman, S. Scalable enumeration of trap spaces in boolean networks via answer set programming. In AAAI 2024, volume 38, pp. 10714--10722

    2024

  56. [64]

    Valiant, L. G. The complexity of enumeration and reliability problems. SIAM Journal on Computing , 8(3):410--421 1979

    1979

  57. [65]

    From disjunctive to normal logic programs via unfolding and shifting

    Zhou, Y. From disjunctive to normal logic programs via unfolding and shifting. In ECAI 2014 2014, pp. 1139--1140. IOS Press

    2014

  58. [66]

    write newline

    " write newline "" before.all 'output.state := FUNCTION fin.entry add.period write newline FUNCTION new.block output.state before.all = 'skip after.block 'output.state := if FUNCTION new.sentence output.state after.block = 'skip output.state before.all = 'skip after.sentence '...

Pith tools

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