# exact_asp_counting_with_compact_encodings__d5ec3ce7.pdf

Exact ASP Counting with Compact Encodings*

Mohimenul Kabir1, Supratik Chakraborty2, Kuldeep S Meel3

1National University of Singapore 2Indian Institute of Technology Bombay 3University of Toronto

Answer Set Programming (ASP) has emerged as a promising paradigm in knowledge representation and automated reasoning owing to its ability to model hard combinatorial problems from diverse domains in a natural way. Building on advances in propositional SAT solving, the past two decades have witnessed the emergence of well-engineered systems for solving the answer set satisfiability problem, i.e., finding models or answer sets for a given answer set program. In recent years, there has been growing interest in problems beyond satisfiability, such as model counting, in the context of ASP. Akin to the early days of propositional model counting, state-ofthe-art exact answer set counters do not scale well beyond small instances. Exact ASP counters struggle with handling larger input formulas. The primary contribution of this paper is a new ASP counting framework, called sharp ASP, which counts answer sets avoiding larger input formulas. This relies on an alternative way of defining answer sets that allows for the lifting of key techniques developed in the context of propositional model counting. Our extensive empirical analysis over 1470 benchmarks demonstrates significant performance gain over current state-of-the-art exact answer set counters. Specifically, by using sharp ASP, we were able to solve 1062 benchmarks with PAR2 score of 3082 whereas using prior state-of-the-art, we could only solve 895 benchmarks with a PAR2 score of 4205, all other experimental conditions being the same.

1 Introduction Answer Set Programming (ASP) (Marek and Truszczy nski 1999) is a declarative problem-solving approach with a wide variety of applications ranging from planning, diagnosis, scheduling, and product configuration checking (Nouman et al. 2016; Brik and Remmel 2015; Tiihonen et al. 2003). An ASP program consists of a set of rules defined over propositional atoms, where each rule logically expresses an implication relation. An assignment to the propositional atoms satisfying the ASP semantic is called an answer set. In this paper, we focus on an important class of ASP programs called normal logic programs that have been used in diverse applications (see for example (Dodaro and Maratea 2017; Brooks et al. 2007)), and present a new technique to

*The ar Xiv version: https://arxiv.org/abs/2312.11936 Copyright 2024, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

count answer sets of such programs, while scaling much beyond state-of-the-art exact answer set counters. In general, given a set of constraints in a theory, model counting seeks to determine the number of models (or solutions) to the set of constraints. From a computational complexity perspective, this can be significantly harder than deciding whether there exists any solution to the set of constraints, i.e. the satisfiability problem. Yet, in the context of propositional reasoning, compelling applications have fuelled significant practical advances in propositional model counting, also referred to as #SAT (Thurley 2006), over the past decade. This, in turn, has ushered in new applications in quantified information flow (Biondi et al. 2018), neural network verification (Baluta et al. 2019), computational biology, and the like. The success of practical propositional model counting in diverse application domains have naturally led researchers to ask if practically efficient counting algorithms can be devised for constraints beyond propositional logic. In particular, there has been growing interest in answer set counting, motivated by applications in probabilistic reasoning and network reliability (Kabir and Meel 2023; Aziz et al. 2015). Early efforts to build answer set counters sought to work by enumerating answer sets of a given ASP program (Fichte et al. 2017; Gebser et al. 2007). While this works extremely well for answer set counts upto a certain threshold, enumeration doesn t scale well for problem instances with too many answer sets. Therefore, subsequent approaches to answer set counting sought to leverage the significant progress made in #SAT techniques. Specifically, Aziz et al. (Aziz et al. 2015) integrated a component-caching based propositional model counting technique with unfounded set detection to yield an answer set counter, called ASProblog. In another line of work, dynamic programming on a tree decomposition of the input problem instance has been proposed to achieve scalability for ASP instances with low treewidth (Fichte et al. 2017; Fichte and Hecher 2019). Yet another approach has been to translate a given normal logic program P into a propositional formula F, such that there is a one-to-one correspondence between answer sets of P and models of F (Janhunen and Niemel a 2011; Bomanson 2017; Janhunen 2006). Answer sets of P can then be counted by invoking an off-the-shelf propositional model counter (Sharma et al. 2019) on F. Though promising in principle, a naive appli-

The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)

cation of this approach doesn t scale well in practice owing to a blowup in the size of the resulting formula F when the implications between propositional atoms encoded in the program P give rise to circular dependencies (Lifschitz and Razborov 2006), which is a common occurrence when modeling numerous real-world applications. To address this, researchers have proposed techniques to transform the program to effectively break such circular dependencies and then use a treewidth-aware translation of the transformed program to a propositional formula (see, for example (Eiter, Hecher, and Kiesel 2021)). However, breaking such circular dependencies can increase the treewidth of the resulting transformed problem instance, which in turn can adversely affect the performance of answer set counting. Thus, despite significant advances, state-of-the-art exact answer set counters are stymied by scalability bottlenecks, limiting their practical applicability. Within this context, we ask the question: Can we design a scalable answer set counter, accompanied by a substantial reduction in the size of the transformed input program, particularly when addressing circular dependencies? The principal contribution of this paper addresses the aforementioned question by introducing an alternative approach to exact answer set counting, called sharp ASP, while alleviating key bottlenecks faced by earlier approaches. While a mere reduction in translation size does not inherently establish a scalable ASP counting solution for general scenarios, sharp ASP allows us to solve larger and more instances of exact answer set counting than was feasible earlier. Similar to ASProblog, sharp ASP lifts componentcaching based propositional model counting algorithms to ASP counting. The key idea that makes this possible is an alternative yet correlated perspective on defining answer sets. This alternative definition makes it possible to lift core ideas like decomposability and determinism in propositional model counters to facilitate answer set counting. Viewed differently, transforming propositional model counters into our proposed ASP counting framework requires minimal adjustments. Our experimental analysis demonstrates that sharp ASP, built using this approach, significantly outperforms the performance of state-of-the-art techniques across instances from diverse domains. This serves to underscore the effectiveness of our approach over the combined might of earlier state-of-the-art exact answer set counters. The remainder of this paper is organized as follows. We present some preliminaries and notations in Section 2. Section 3 presents an alternative way of defining the answer set of an ASP instance, which allows us to propose the answer set counting algorithm of sharp ASP in Section 4, where we also present correctness arguments for our algorithm. Section 5 presents our experimental evaluation of the proposed answer set counting algorithm. Finally, we conclude our paper in Section 6.

2 Preliminaries

Before delving into the details, we introduce some notation and preliminaries from propositional satisfiability and answer set programming.

Propositional Satisfiability. A propositional variable v takes one of two values: 0 (denoting false) or 1 (denoting true). A literal ℓis either a variable (positive literal) or its negation (negated literal), and a clause C is a disjunction of literals. For convenience of exposition, we sometimes represent a clause as a set of literals, with the implicit understanding that all literals in the set are disjoined in the clause. A clause with a single literal is also called a unit clause. In general, the constraint represented by a clause C ( v1 . . . vk vk+1 . . . vk+m) can be expressed as a logical implication: (v1 . . . vk) (vk+1 . . . vk+m). If k = 0, the antecedent of the above implication is true, and if m = 0, the consequent is false. A conjunctive normal form (CNF) formula φ is a conjuction of clauses. When there is no confusion, a CNF formula is also sometimes represented as a set of clauses, with the implicit understanding that all clauses in the set are conjoined to give the formula. We denote the set of variables in φ as Var(φ). An assignment of a set X of propositional variables is a mapping τ : X {0, 1}. For a variable v X, we define τ( v) = 1 τ(v). Given a CNF formula φ (as a set of clauses) and an assignment τ : X {0, 1}, where X Var(φ), the unit propagation of τ on φ, denoted φ|τ, is recursively defined as follows:

1 if φ 1 φ |τ if C φ s.t. φ = φ \ {C}, ℓ C and τ(ℓ) = 1 φ |τ {C } if C φ s.t. φ = φ \ {C}, ℓ C,C = C \ { ℓ} and (τ(ℓ) = 1 or {l} φ) Note that φ|τ always reaches a fixpoint. We say that τ unit propagates to literal ℓin φ if {ℓ} φ|τ, i.e. if φ|τ has a unit clause with the literal ℓ.

Answer Set Programming. An answer set program P expresses logical constraints between a set of propositional variables. In the context of answer set programming, such variables are also called atoms, and the set of atoms appearing in P is denoted atoms(P). For notational convenience, we will henceforth use the terms variable and atom interchangeably. A normal (logic) program is a set of rules of the following form:

Rule r: a b1, . . . , bm, c1, . . . , cn (1)

In the above rule, denotes default negation, signifying failure to prove (Clark 1978). For rule r shown above, atom a is called the head of r and is denoted Head(r). Similarly, the set of literals {b1, . . . , bm, c1, . . . , cn} is called the body of r. Specifically, {b1, . . . , bm} are the positive body atoms, denoted Body(r)+, and {c1, . . . , cn} are the negative body atoms, denoted Body(r) . For purposes of the following discussion, we use Body(r) to denote the conjunction b1 . . . bm c1 . . . cn. Atoms that appear in the head of a rule (like a in rule r above) have also been called founded variables/atoms in the literature (Aziz et al. 2015). In answer set programming, an interpretation M atoms(P) lists the true atoms, i.e., an atom a is true iff a M. An assignment M satisfies Body(r), denoted M |=

The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)

Body(r), iff Body(r)+ M and Body(r) M = , where is interpreted classically, i.e., M |= ci iff M |= ci. The rule r (see Equation (1)) specifies that if all atoms in Body(r)+ hold and no atom in Body(r) holds, then Head(r) also holds. The assignment M satisfies rule r, denoted M |= r, if and only if whenever M |= Body(r), then Head(r) M. Let Rules(P) denote the set of all rules in a normal program P. Then, we say that an assignment M satisfies P, denoted M |= P, if and only if M |= r for each r Rules(P). Given an assignment (or set of atoms) M, the Gelfond Lifschitz (GL) reduct of a program P w.r.t. M is defined as P M = {Head(r) Body(r)+ | r Rules(P), Body(r) M = } (Gelfond and Lifschitz 1988). A set of atoms M is an answer set of P if and only if M |= P M, but N |= P M for every proper subset N of M. The set of all answer sets of program P is denoted by AS(P), and the answer set counting problem is to compute |AS(P)|, which is denoted by Cnt AS(P). Clark s completion (Clark 1978) or program completion is a technique for obtaining a translation of a normal program P into a related, but not semantically equivalent, propositional formula Comp(P). Specifically, for each atom a atoms(P), we do the following:

1. Let r1, . . . , rk Rules(P) such that Head(r1) = . . . = Head(rk) = a, then we add the propositional formula (a (Body(r1) . . . Body(rk))) to Comp(P). 2. Otherwise, we add the literal a to Comp(P).

Finally, Comp(P) is obtained as the logical conjunction of all constraints added above. It has been shown in the literature that an answer set of P satisfies Comp(P) but not vice versa (Lin and Zhao 2004). To overcome the above problem, the idea of loop formula was introduced in (Lin and Zhao 2004). We outline the construction of a loop formula below. Given a normal program P, we start by defining the positive dependency graph DG(P) of P as follows. The vertices of DG(P) are simply atoms(P). For a, b atoms(P), there exists an edge from b to a in DG(P) if there is a rule r Rules(P) such that a Body(r) and b = Head(r). A set of atoms L atoms(P) constitutes a loop in P if for every two atoms x, y L there is a path from x to y in DG(P) such that all atoms (nodes) on the path are in L. An atom a is called a loop atom of P if there is a loop L in P such that a L. We use Loops(P) and LA(P) to denote the set of all loops and the set of all loop atoms of P, respectively. A program P is called tight if there is no loop in P; otherwise, P is called non-tight. Lin and Zhao (Lin and Zhao 2004) showed that atoms in a loop cannot be asserted true by themselves; instead they must be asserted by some atoms external to the loop. Specifically, a rule r is an external support of a loop L in P if Head(r) L and Body(r)+ L = . Let Ext Rule(L) denote the set of all external supports of loop L in P. The loop formula LF(L, P) (Lee and Lifschitz 2003) of a loop L in program P can now be defined as follows:

LF(L, P) = (

r Ext Rule(L) Body(r)

Finally, the loop formula LF(P) of program P is defined as the conjunction of loop formulas for all loops L in P, i.e. V L Loops(P ) LF(L, P). Let M atoms(P) be a subset of atoms of P. We use τ M : atoms(P) {0, 1} to denote the assignment corresponding to M, i.e. τ M(v) = 1 if v M and τ M(v) = 0 otherwise, for all v atoms(P). Then M is an answer set of P if and only if τ M satisfies the propositional formula Comp(P) LF(P) (Lin and Zhao 2004).

2.1 Related Work The decision version of normal logic programs is NPcomplete; therefore, the ASP counting for normal logic programs is #P-complete (Valiant 1979). Given the #Pcompleteness, a prominent line of work focused on ASP counting relies on translations from the ASP program to the CNF formula (Lin and Zhao 2004; Janhunen 2004, 2006; Janhunen and Niemel a 2011). Such translations often result in a large number of CNF clauses and thereby limit practical scalability for non-tight ASP programs. Eiter et al. (2021) introduced TP-unfolding to break cycles and produce a tight program. They proposed an ASP counter called aspmc, that performs a treewidth-aware Clark completion from a cycle-free program to the CNF formula. Jakl, Pichler, and Woltran (2009) extended the tree decomposition based approach for #SAT due to Samer and Szeider (2007) to Answer Set Programming and proposed a fixed-parameter tractable (FPT) algorithm for ASP counting. Fichte et al. (2017; 2019) revisited the FPT algorithm due to Jakl et al. and developed an exact model counter, called Dyn ASP, that performs well on instances with low treewidth. Aziz et al. (2015) extended a propositional model counter to an answer set counter by integrating unfounded set detection. Kabir et al. (2022) focused on lifting hashing-based techniques to ASP counting, resulting in an approximate counter, called Approx ASP, with (ε, δ)-guarantees.

3 An Alternative Definition of Answer Set Our algorithm for answer set counting crucially relies on an alternative way of defining the answer sets of a normal program P. We first introduce an operation called Copy() that plays a central role in this alternative definition. Our Copy() operation is related to, but not the same as, a similar operation used in ASProblog. Specifically, founded variables (i.e. variables appearing at the head of a rule) were the focus of the copy operation used in ASProblog. In contrast, loop atoms in the program P are the focus of the Copy() operation in our approach. We elaborate more on this below.

3.1 The Copy Operation Given a normal program P, for every loop atom/variable v in LA(P), let v be a fresh variable not present in atoms(P). We refer to v as the copy variable of v. For X LA(P), we denote the set of copy variables corresponding to atoms in X as X . The Copy() operation, when applied to a normal program P, returns a set of (implicitly conjoined) implications, defined as follows: 1. (type 1) for every v LA(P), the implication v v is in Copy(P).

The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)

2. (type 2) for every rule x a1, . . . ak, b1, . . . bm, c1, . . . cn in P, where x LA(P), {a1, . . . ak} LA(P) and {b1, . . . bm} LA(P) = , the implication a1 . . . ak b1 . . . bm c1 . . . cn x is in Copy(P). 3. No other implication is in Copy(P). Note that in implications of type 2, copy variables are used exclusively for positive loop atoms in the body of the rule and for the loop atom in the head of the rule. Specifically, if the head of a rule is not a loop atom, we don t add any implication of type 2 for that rule. As an extreme case, if P is a tight program or LA(P) = , then Copy(P) is empty.

An Alternative Definition of Answer Set We now present a key observation that provides the basis for an alternative definition of answer sets. Akin to the existing definitions of answer set (Janhunen 2006; Giunchiglia, Lierler, and Maratea 2006; Lifschitz 2010), our definition seeks justification for atoms within an answer set. However, our definition seeks to justify only loop atoms belonging to an answer set, while the existing definitions, to the best of our knowledge, aim to justify each atom in an answer set. The alternative definition derives from the observation that under Clark s completion of a program, if the loop atoms of an answer set are justified, then the remaining atoms of the answer set are also justified. Thus, under Clark s completion, it suffices to seek justifications for loop atoms. Unlike existing definitions of answer sets, our definition of answer sets operates exclusively within the realm of Boolean formulas and employs unit propagation as a tool to decide whether an atom is justified or not. Recall from Section 2 the definition of φ|τ, i.e. unit propagation of an assignment τ on a CNF formula φ. Recall also that a CNF formula can be viewed as a set of clauses, where each clause can be interpreted as an implication. Therefore, the set of implications Copy(P) can be thought of as representing a CNF formula. For an assignment τ : X {0, 1} where X atoms(P), we use the notation Copy(P)|τ to denote the (implicitly conjoined) set of implications that remain after unit propagating τ on the CNF formula represented by Copy(P). Specifically, we say that Copy(P)|τ = if τ unit propagates to only unit clauses on copy variables in the CNF formula represented by Copy(P). Theorem 1. For a normal program P, let X atoms(P) and let τ : X 7 {0, 1} be an assignment. Let M τ denote the set of atoms of P that are assigned 1 by τ. Then M τ AS(P) if and only if τ |= Comp(P) and Copy(P)|τ= .

Proof. (i) (proof of if part ) Proof By Contradiction. Assume that τ |= Comp(P) and Copy(P)|τ= , but M τ AS(P). Since M τ AS(P) and τ |= Comp(P), it implies that τ |= LF(P). Thus, there is a loop L in P such that τ |= LF(L, P). Assume that L is comprised of the set of loop atoms { x1, . . . , xk }. Then τ |= x1 . . . xk W

r Ext Rule(L) Body(r). In other words, even if τ is augmented by setting x1 = . . . = xk = 1, the formula W r Ext Rule(L) Body(r) evaluates to 0 under the augmented assignment. Now recall that τ itself is an assignment to a subset of atoms(P), and it does not assign any truth value

to x1 , . . . , xk . Therefore, there must be at least one type 2 implication in Copy(P)|τ, specifically one arising from a rule r Ext Rule(L), that does not unit propagate to a unit clause or to 1 under τ. This contradicts the premise that Copy(P)|τ= . (ii) (proof of only if part ) Proof By Contradiction. Suppose M τ AS(P). We know that this implies τ |= Comp(P) LF(P). We now show that in this case, we must also have Copy(P)|τ= . Suppose, if possible, Copy(P)|τ = . We ask if an implication of type 1, say v v, can stay back in Copy(P)|τ. If v M τ, then τ(v) = 1, and clearly the implication v v doesn t stay back in Copy(P)|τ. If v M τ, then τ(v) = 0, and in this case τ unit propagates to { v }, and hence the implication doesn t stay back in Copy(P)|τ either. Therefore, no implication of type 1 can stay back in Copy(P)|τ. Next, we ask if any implication of type 2 can stay back in Copy(P)|τ. Suppose this is possible. Note that for every v atoms(P), either v M τ or v M τ. Therefore, τ(v) is either 0 or 1 for all v atoms(P). Therefore, if Copy(P)|τ = , there must be some x1 Var(Copy(P)|τ) and there must a (potentially simplified) implication x2 C1 x1 in Copy(P)|τ, where C1 is either true or a conjunction of copy variables. The existence of copy variable x2 in Copy(P)|τ implies the existence of another implication: x3 C2 x2 in Copy(P)|τ. Continuing this argument, we find that there are two cases to handle: (i) there are an unbounded number of copy variables in Copy(P)|τ, which contradicts the fact that there can be at most |Var(P)| copy variables. (ii) otherwise, there exists i, j such that xi = xj and i < j, which implies that the set of variables { xi, . . . xj 1 } constitutes an unfounded set. However, this contradicts the fact that M τ AS(P). In either case, we reach a contradiction, thereby proving that Copy(P)|τ is empty. This completes the proof.

Example 1. Consider the normal program P given by the rules {r1 = a b. r2 = b a. r3 = c a, b. r4 = c d. r5 = d a. r6 = d b, c. r7 = e a, b}. This program has a single loop L consisting of atoms c and d, i.e. LA(P) = {c, d}. Therefore, Copy(P) consists of the conjunction of implications: { c c, d d, a b c , d c , a d , b c d }. Note that there are no variables a , b , e or constraints involving them in Copy(P). The followings are now easily verified. Consider τ1 that assigns 1 to b and 0 to a, c, d, e. For the corresponding answer set M τ1: { b }, Copy(P)|τ1= Consider τ2 assigns 1 to a, c, d and 0 to b, e. For the corresponding answer set M τ2: { a, c, d }, Copy(P)|τ2= Consider τ3 that assigns 1 to b, c, d and 0 to a, e. For the corresponding non-answer set M τ3: { b, c, d }, Copy(P)|τ3 =

4 Counting Answer Sets In this section, we first show how the alternative definition of answer sets provides a new way to counting all answer sets of a given normal program. Subsequently, we explore how off-the-shelf state-of-the-art propositional model counters can be easily adapted to correctly count answer sets by leveraging the alternative definition.

The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)

It is easy to see from Theorem 1 that the count of answer sets of a normal program P can be obtained simply by counting assignments τ 2|atoms(P )| such that τ |= Comp(P) and Copy(P)|τ= . This motivates us to represent a normal program P using a pair (F, G), where F = Comp(P) and G = Copy(P). Further, we discuss below how key ideas in state-of-the-art propositional model counters can be adapted to work with this pair representation of normal programs to yield exact answer set counters.

4.1 Decomposition Propositional model counters often decompose the input CNF formula into disjoint subformulas to boost up the counting efficiency (Bayardo Jr and Pehoushek 2000) for two formulas φ1 and φ2, if Var(φ1) Var(φ2) = , then φ1 and φ2 are decomposable, i.e., we can count the number of models of φ1 and φ2 separately and multiply these two counts to get the number of models of φ1 φ2. Given a normal program, our proposed definition involves a pair of formulas: F and G. Specifically, we define component decomposition with respect to (F, G) as follows:

Definition 1. (F1 F2, G1 G2) is decomposable to (F1, G1) and (F2, G2) if and only if (Var(F1) Var(G1)) (Var(F2) Var(G2)) = .

Finally, Proposition 1 offers evidence supporting the correctness of our proposed definition of decomposition in computing the number of answer sets.

Proposition 1. Let (F1 . . . Fk, G1 . . . Gk) is decomposed to (F1, G1), . . . , (Fk, Gk) then Cnt AS(F1 . . . Fk, G1 . . . Gk) = Cnt AS(F1, G1) . . . Cnt AS(Fk, Gk)

Proof. By definition of decomposition, we know that (Var(Fi) Var(Gi)) (Var(Fj) Var(Gj)) = , for 1 i < j k. This, in turn, implies that Var(Gi) Var(Gj) = for 1 i < j k. Therefore, no variable (copy variable or otherwise) is common in Gi and Gj, if i = j. Hence, for every assignment τ : atoms(P) {0, 1}, unit propagation of τ on Gi and Gj must happen completely independent of each other, i.e. no unit literal obtained by unit propagation of τ on Gi affects unit propagation of τ on Gj, and vice versa. In other words, Gi|τ Gj|τ= (Gi Gj)|τ. Let F = F1 . . . Fk and G = G1 . . . Gk. In the following, we use the notation τ to denote an assignment atoms(P) {0, 1}, and τi to denote an assignment atoms(P) (Var(Fi) Var(Gi)) {0, 1}, for 1 i k. By virtue of the argument in the previous paragraph, the domains of τi and τj are disjoint for 1 i < j k. We use the notation τ1 . . . τk to denote the assignment atoms(P) {0, 1} defined as follows: if v atoms(P) (Var(Fi) Var(Gi)), then (τ1 . . . τk)(v) = τi(v). The proof now consists of showing the following two claims:

1. Cnt AS(F1, G1) Cnt AS(Fk, Gk) Cnt AS(F, G). 2. Cnt AS(F1, G1) Cnt AS(Fk, Gk) Cnt AS(F, G).

Proof of part 1: Suppose τ AS(F, G). By definition, τ |= F and G|τ= . Since F = F1 . . . Fk, we know that τ |= Fi for 1 i k. By the above definition of

τi, it then follows that τi |= Fi. Similarly, since unit propagation of τ on Gi and Gj happen independently for all i = j, and since unit propagation of τ on G = G1 . . . Gk gives , we have Gi|τi= as well. It follows that τi AS(Fi, Gi) for 1 i k. Therefore, every τ AS(F, G) yields a sequence of τi AS(Fi, Gi), for 1 i k. Since the domains of all τi s are distinct, it follows that Cnt AS(F1, G1) Cnt AS(Fk, Gk) Cnt AS(F, G). Proof of part 2: Suppose τi AS(Fi, Gi) for 1 i k. By definition, τi |= Fi and Gi|τi= . Since the domains of τi and τj are disjoint for all 1 i < j k, it follows that (τ1 . . . τk) |= (F1 . . . Fk) and hence τ |= F. We have also seen that (G1 Gk)|τ= (G1|τ Gk|τ). However, since Var(Gi) is a subset of the domain of τi, we have (G1 Gk)|τ= (G1|τ1 Gk|τk). Since Gi|τi= for 1 i k, it follows that (G1 Gk)|τ= . Therefore G|τ= . Since τ |= F as well, we have τ AS(F, G). Therefore, every distinct sequence of τi, 1 i k such that τi AS(Fi, Gi) yields a distinct τ AS(F, G). It follows that Cnt AS(F1, G1) Cnt AS(Fk, Gk) Cnt AS(F, G). It follows from the above two claims that

Cnt AS(F1, G1) Cnt AS(Fk, Gk) = Cnt AS(F, G).

One of the drawbacks of the definition is its comparative weakness in relation to the conventional definition of decomposition. When dealing with a hard-to-decompose program (F, G), then the process of counting answer sets regresses to enumerating the answer sets of the program.

4.2 Determinism Propositional model counters utilize determinism (Darwiche 2002), which involves assigning one of the variables in a formula to either false or true. The number of models of φ is then determined as the sum of the number of models in which a variable x Var(φ) is assigned to false and true. A similar idea can be used for answer set counting using our pair representation as well. To establish the correctness of the determinism employed in our approach, we first introduce two helper propositions: Proposition 2 and 3.

Proposition 2. For partial assignment τ and program P represented as (Comp(P), Copy(P)), if Comp(P)|τ= and Var(Copy(P)|τ) Copy Var(P), then L Loops(P) s.t. L M τ and τ |= LF(L, P).

Proof. Since Var(Copy(P)|τ) Copy Var(P), there exists a copy variable xi1 Var(Copy(P)|τ) and an implication (simplified after unit propagation) of type 2 of the form C1 xi1 in Copy(P)|τ, where C1 is a nonempty conjunction of copy variables. Let xi2 Var(C1), then there must also exist another implication (simplified after unit propagation) C2 xi2 in Copy(P)|τ, where C2 is again a conjunction of copy variables. Accordingly, for xi3 Var(C2)\Var(C1), we have another implication of the form C3 xi3 in Copy(P)|τ. Since the number of atoms is bounded, it must be the case that there exists ik such that there is an implication (simplified) of type 2 Ck xk such that Ck \ (C1 C2 . . . Ck 1) = .

The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)

Now, observation Ck \ (C1 C2 . . . Ck 1) = implies existence of an atom set L = {xi1, xi2, . . . xij} {xi1, xi2, . . . xik} that forms a loop in DG(P). Given that Var(Copy(P)|τ) Copy Var(P), we also know that τ assigns a value to every x Var(Copy(P)) atoms(P). Furthermore, each of the atoms xi1, . . . xik must have been assigned 1 by τ. Otherwise, if any xil was assigned 0 by τ, then τ would have unit propagated on Copy(P)|τ to x il, which contradicts the observation that the copy variables x i1, . . . x ik stayed backed in antecedents of implications of type 2 in Copy(P)|τ. It follows that atoms in loop L form a subset of atoms assigned 1 by τ. We have shown above that {xi1, xi2, . . . xij} constitutes a loop in the positive dependency graph. We now show by contradiction that τ |= W r Ext Rule(L) Body(r). Indeed, if τ |= W r Ext Rule(L) Body(r), let xit be Head(r) for a rule r such that τ |= Body(r). In this case, τ must have unit propagated to {x it} in Copy(P)|τ. This contradicts the fact that the copy variables x i1, . . . x ik stayed backed in antecedents of implications of type 2 in Copy(P)|τ. Therefore τ |= xi1 . . . xij but τ |= W r Ext Rule(L) Body(r). This shows that τ |= LF(L, P).

Proposition 3. For partial assignment τ and program P represented as (Comp(P), Copy(P)), suppose τ |= LF(L, P), where L = {x1, . . . , xk}. Then there exists τ + such that {x1 , . . . , xk } Var(Copy(P)|τ +), Comp(P)|τ += and τ τ +.

Proof. As τ |= LF(L, P), we have xi L, τ(xi) = 1 and r Ext Rule(L), τ |= Body(r). Let us denote by r an implication of type 2 corresponding to a rule r Ext Rule(L). Then we have r |τ = ; moreover, if Head(r) = xi, then xi Var(r|τ). Since the above observation holds for all r Ext Rule(L) and for xi L, therefore, {x1 , . . . , xk } Var(Copy(P)|τ). Observe that for every extension τ of τ that does not assign values to variables in {x1 , . . . , xk }, it must be the case that {x1 , . . . , xk } Var(Copy(P)|τ ). Furthermore, since the set of variables in Comp(P) does not contain a variable from the set {x1 , . . . , xk }, therefore, there exists an extension, τ +, of τ such that Comp(P)|τ += and {x1 , . . . , xk } Var(Copy(P)|τ ).

We are now ready to state and prove the correctness of determinism employed in our ASP counter:

Proposition 4. Let program P be represented as (F, G). Then

Cnt AS(F, G) = Cnt AS(F| x, G| x) + Cnt AS(F|x, G|x), for all x atoms(P) (2) Cnt AS( , G) = 0 (3)

Cnt AS( , G) = 1 if G = 0 if Var(G) Copy Var(P) (4)

Note that if Comp(P) = then either G = or Var(G) Copy Var(P).

Proof. The proof comprises the following three parts:

Equation (2) applies determinism by partitioning all answer sets of (F, G) into two parts the answer sets where x is 0 and 1, respectively. Observe that performing unit propagation on (F, G) is valid since τ AS(F|σ, G|σ) if and only if σ τ AS(F, G), where σ 2|X|, τ 2|atoms(P )\X|, where X atoms(P). The proof of the first base case eq. (3) is trivial. Each answer set of P conforms to the completion of the program Comp(P), where, according to the alternative definition of answer sets, F = Comp(P). We utilize the helper propositions proved earlier to demonstrate the correctness of the second base case, as outlined in eq. (4), which appropriately selects answer sets from the models of completion. First, we show that if there is a copy variable in Copy(P)|τ, where Comp(P)|τ= , then one of the loop formulas of the program is not satisfied by τ. The claim is proved in Proposition 2. Thus, τ cannot be extended to an answer set. Second, we demonstrate that if there is an unsatisfied loop formula under a partial assignment τ1, then there exists τ + 1 such that some copy variables are not propagated in Copy(P)|τ + 1 , where Comp(P)|τ + 1 = and τ1 τ + 1 . The claim is established in Proposition 3. Thus, through the method of contradiction, we can infer that, for an assignment τ, if Copy(P)|τ= , then τ can be extended to an answer set.

4.3 Conjoin F and G Until now, we have represented a program P as a pair of formulas F and G. However, in this subsection, we illustrate that rather than considering the pair, we can regard their conjunction F G, and all the subroutines of model counting algorithms work correctly. First, in Proposition 5, we demonstrate that F G uniquely defines a program (F, G) under arbitrary partial assignments. Proposition 5. For two assignments τ1 and τ2, and given a normal program, F|τ1 G|τ1= F|τ2 G|τ2 if and only if F|τ1= F|τ2 and G|τ1= G|τ2

Proof. (i) (proof of if part ) The proof is trivial. (ii) (proof of only if part ) Proof By Contradiction. Assume that there is a clause c F|τ1 and c F|τ2. As F|τ1 G|τ1= F|τ2 G|τ2 clause c G|τ2. As c F|τ1, c has no copy variable. Assume that clause c is derived from the unit propagation of Copy(r), i.e., c = Copy(r)|τ2= a1 . . . ak b1 . . . bm c1 . . . cn x |τ2, where i, ai propagates to 1 and x propagates to 0, which follows that under assignment τ2, the atom x is assigned to 0 and i, ai is assigned to 1. The rule r also belongs to Comp(P) and both F|τ1 and F|τ2 are derived from Comp(P). Thus, under assignment τ2, if x is assigned to 0 and each of the ai s is assigned to 1, then the clause c F|τ2, which must be derived from rule r, so contradiction.

As a result, it is possible to perform unit propagation on F G instead of performing unit propagation on F and G separately. Although both formulas F and G are necessary to check the base cases, we can still check base cases by considering the conjunction F G. Checking the first base case

The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)

(eq. (3)) is trivial because if an assignment τ conflicts on F, then τ conflicts on F G as well. Additionally, calculating Var(F G) suffices to check the second base case (eq. (4)). The component decomposition part also works with their conjunction because the component decomposition condition (Var(F1) Var(G1)) (Var(F2) Var(G2)) = is equivalent to (Var(F1 G1)) (Var(F2 G2)) = . Moreover, as we restrict our decision to atoms(P), the conjunction F G does not introduce new conflicts if a partial assignment τ conflicts on F G, then τ conflicts on F. To summarize, the model counting algorithm correctly computes the answer set count, even when processing the formula F G instead of processing the two formulas F and G separately.

4.4 sharp ASP: Putting It All Together

In this subsection, we aim to extend a propositional model counter to an exact answer set counter by integrating the alternative answer set definition, component decomposition (Proposition 1), and determinism (Equation (2)).

Algorithm 1: sharp ASP(P)

1: function Counter(φ, CV ) modified CNF counter 2: if φ = then return 1 3: else if Var(φ) CV then return 0 4: else if φ then return 0 5: v Pick Non Copy Var(φ) 6: for ℓ {v, v} do 7: Count[ℓ] 1 8: comps Decomposition(φ|ℓ) 9: for each c comps do 10: if c Cache then 11: Count[ℓ] Count[ℓ] Cache[c] 12: else 13: Count[ℓ] Count[ℓ] Counter(c, CV )

14: if Count[ℓ] = 0 then 15: break 16: Cache[φ] Count[v] + Count[ v] 17: return Cache[φ] 18: end function 19: F Comp(P), G Copy(P) Algorithm starts here 20: return Counter(F G, Copy Var(P))

The pseudocode for sharp ASP is presented in Algorithm 1. Given a non-tight program P, sharp ASP initially computes Comp(P) and Copy(P) (Line 19 of Algorithm 1) and then calls the adapted propositional model counter Counter, with Comp(P) Copy(P) as the input formula, and Copy Var(P) as the set of copy variables (Line 20 of Algorithm 1). The model counting algorithm utilizes Copy Var(P) to check the base cases (Equation (3) and (4)) of the Equation (2). The Counter differs from the existing propositional model counters mainly in two ways. Firstly, following eq. (4), the Counter returns 0 if it encounters a component consisting solely of copy variables (Line 3 of Algorithm 1). Secondly, during variable branching, Counter selects variables from

Var(Comp(P)) (Line 5 of Algorithm 1). Apart from that, the subroutines of unit propagation, component decomposition (Line 8 of Algorithm 1), and caching1 (Line 10 of Algorithm 1) within Counter and a propositional model counter remain unchanged. While sharp ASP uses copy variables and copy operations similar to ASProblog, there are notable distinctions between the two approaches. Firstly, sharp ASP aims to justify only loop atoms, whereas the ASProblog algorithm aims to justify all founded variables. Our empirical findings underscore that loop atoms constitute a relatively small subset of the founded variables. Consequently, the copy operation of ASProblog introduces more copy variables and logical implications involving copy variables compared to ours. Secondly, the unit propagation techniques employed in ASProblog differ from those used in sharp ASP. Specifically, ASProblog performs unit propagation by propagating only the justified literals from a program while leaving the unjustified literals in the residual program. In contrast, sharp ASP adheres to the conventional unit propagation technique and employs copy variables to determine whether all atoms are justified.

5 Experimental Evaluation

We developed a prototype2 of sharp ASP on top of the existing state-of-the-art model counters (GANAK, D4, and Sharp SAT-TD) (Korhonen and J arvisalo 2021; Sharma et al. 2019; Lagniez and Marquis 2017). We modified Sharp SATTD by disabling all the preprocessing techniques, as they would no longer preserve answer sets. We use notations sharp ASP(STD), sharp ASP(G), and sharp ASP(D) to represent sharp ASP with underlying propositional model counters Sharp SAT-TD, GANAK, and D4, respectively. We compared the performance of sharp ASP with that of the prior state-of-the-art exact ASP counters: clingo3 (Gebser et al. 2007), ASProblog (Aziz et al. 2015), and Dyn ASP (Fichte et al. 2017). In addition, we utilized two translations from ASP to SAT: (i) lp2sat (Fages 1994; Janhunen and Niemel a 2011; Bomanson 2017) (ii) aspmc (Eiter, Hecher, and Kiesel 2021), followed by invoking offthe-shelf propositional model counters. We use notations lp2sat+X and aspmc+X to denote lp2sat and aspmc followed by propositional model counter X, respectively. Our benchmark suite consists of non-tight programs from the domains of the Hamiltonian cycle and graph reachability problems (Kabir et al. 2022; Aziz et al. 2015). We also considered the benchmark set from (Eiter, Hecher, and Kiesel 2021) (designated as aspben). We gathered a total of 1470 graph instances from the benchmark set of (Kabir et al. 2022; Eiter, Hecher, and Kiesel 2021). The choice/random variables in the hamiltonian cycle and aspmc benchmark pertain to graph edges. While the choice variables are associated with graph nodes for the graph reachability problem.

1Model counter stores the count of previously solved subformulas by a caching mechanism to avoid recounting. 2Available at https://github.com/meelgroup/sharp ASP 3clingo counts answer sets via enumeration.

The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)

We ran experiments on a high-performance computer cluster, where each node consists of AMD EPYC 7713 CPUs running with 128 real cores. The runtime and memory limit were set to 5000 seconds and 8GB, respectively.

5.1 Runtime Performance Comparison

The performance of our considered counters varies across different computational problems. Our evaluation of their performance, considering both total solved instances and PAR2 scores4, for each computational problem is detailed in Table 1. The table demonstrates that sharp ASP either outperforms or achieves performance on par with existing ASP counters, particularly for the Hamiltonian cycle and graph reachability problems. However, on aspben, the clingo enumeration outperforms other answer set counters. We observed that clingo demonstrates superior performance, particularly on instances with a limited number of answer sets. Since this observation applies to all nonenumeration based counters in our repertoire, we devised a hybrid counter that combines the strengths of enumeration based counting with that of translation and propositional SAT based counting. Based on data collected from runs of clingo, there is a shift in the runtime performance of clingo when the count of answer sets exceeds 105 (within our benchmarks). To ensure that our experiments can be replicated on different platforms, we chose to use an answer set count-based threshold instead of a time-based threshold. Hence, our hybrid counter is structured as follows: it initiates enumeration with a maximum of 105 answer sets. In cases where not all answer sets are enumerated, the hybrid counter then employs an ASP counter with a time limit of 5000 t seconds, where t is the time spent in clingo. The performance of the hybrid counters is tabulated in Table 2, demonstrating that the hybrid counter based on sharp ASP clearly outperforms competitors by a handsome margin.

5.2 Ablation Study

We now delve into the internals, and to this end, we form two groups of benchmarks Group 1: instances where sharp ASP(STD) runs faster than lp2sat+STD and aspmc+STD, which highlights the scenarios where the sharp ASP(STD) algorithm is more efficient than lp2sat+STD and aspmc+STD; and Group 2: instances where lp2sat+STD and aspmc+STD run faster than sharp ASP(STD), which shows the opposite scenario of Group 1. Each group consists of 10 instances that had more than 105 answer sets, and therefore clingo could not enumerate all answer sets. By running the instances on all versions of Sharp SAT-TD, we record the time spent on the procedure binary constraint propagation (BCP), number of decisions, and cache hit rate for each counter. Taking each group s average of each quantity provides a clear and concise way to see how sharp ASP compares with others on average across all benchmarks. The statistical findings across all counters are visually summarized in Figure 1.

4PAR2 is a penalized average runtime that penalizes two times the timeout for each unsolved benchmarks.

The strength of sharp ASP lies in its ability to minimize the time spent on binary constraint propagation (BCP) compared to other counters. The significantly large formula size increases the overhead for BCP in the case of lp2sat+STD and aspmc+STD. However, we also observe that sharp ASP suffers from high overhead in the branching phase and high cache misses on Group 2 instances. To find out the reason for a higher number of decisions, we analyze the decomposibility of Group 1 and Group 2 instances. Our investigation has shown that, on all variants of Sharp SAT-TD, most instances of Group 1 start decomposing at nearly the same decision levels. Thus, sharp ASP(STD) outperforms on Group 1 instances due to spending less time on BCP. We observed that several instances of Group 1 took comparatively more decisions to make to count the number of answer sets on sharp ASP(STD). One possible explanation is that aspmc+STD and lp2sat+STD assign auxiliary variables, which have higher activity scores compared to original ASP program variables. Assigning auxiliary variables facilitates lp2sat+STD and aspmc+STD by assigning fewer variables. However, sharp ASP(STD) outperforms others due to structural simplicity and low-cost BCP. Our investigation has also revealed that Group 2 instances are hard-to-decompose on sharp ASP(STD) compared to other counters necessitating more variable assignments to break down an instance into disjoint components. Since sharp ASP(STD) assigns the original set of variables; it necessitates a larger number of decisions to count answer sets on hard-to-decompose instances compared to aspmc and lp2sat based counters. Moreover, the structure of hard-todecompose instances also worsens the cache performance of sharp ASP. However, lp2sat+STD and aspmc+STD effectively decompose the input formula by initially assigning auxiliary variables. In light of these findings, it is evident that the performance of sharp ASP is critically reliant on the decomposability of input instances and the variable branching heuristic employed. Notably, sharp ASP demonstrates superior performance when applied to structurally simpler input instances. If a variable branching heuristic effectively decomposes the input formula by assigning variables within the ASP programs, sharp ASP outperforms alternative ASP counters. Conversely, when the input formula s decomposability is hindered, alternative approaches involving the introduction of auxiliary variables prove to be more advantageous.

6 Conclusion

Our approach, called sharp ASP, lifts the component caching-based propositional model counting to ASP counting without incurring a blowup in the size of the resulting formula. The proposed approach utilizes an alternative definition for answer sets, which enables the natural lifting of decomposability and determinism. Empirical evaluations show that sharp ASP and its corresponding hybrid solver can handle a greater number of instances compared to other techniques. As a future avenue of research, we plan to investigate extensions of our approach in the context of disjunctive programs.

The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)

aspmc lp2sat sharp ASP clingo ASProb Dyn ASP D G STD D G STD D G STD Hamil. (405) 230 0 0 173 197 167 135 164 112 238 261 300

Reach. (600) 318 149 2 187 288 421 317 471 167 293 458 463

aspben (465) 321 39 208 278 285 252 278 193 193 282 273 260

Total (1470) 869 (4285) 188 (8722) 210 (8571) 638 (5829) 770 (5015) 840 (4572) 730 (5282) 668 (5734) 776 (5082) 813 (4514) 992 (3473) 1023 (3372)

Table 1: The performance comparison of sharp ASP vis-a-vis other ASP counters on different problems in terms of number of solved instances and PAR2 scores.

(a) Time spent in BCP (seconds)

(b) Number of decisions (10-base log).

(c) Cache hit (percentage).

Figure 1: The ablation study of sharp ASP(STD), lp2sat+STD, and aspmc+STD on Group 1 and Group 2 benchmarks.

clingo ( 105) +

clingo ASProb aspmc +STD lp2sat +STD sharp ASP (STD)

Hamil. (405) 230 123 167 128 302

Reach. (600) 318 152 418 470 460

aspben (465) 321 278 284 297 300

Total (1470) 869 (4285) 553 (6239) 869 (4310) 895 (4205) 1062 (3082)

Table 2: The performance comparison of hybrid counters in terms of number of solved instances and PAR2 scores. The hybrid counters correspond to last 4 columns that employ clingo enumeration followed by ASP counters. The clingo (2nd column) refers to clingo enumeration for 5000 seconds.

Acknowledgments

This work was supported in part by National Research Foundation Singapore under its NRF Fellowship Programme [NRF-NRFFAI1-2019-0004], Ministry of Education Singapore Tier 2 grant MOE-T2EP20121-0011, and Ministry of Education Singapore Tier 1 Grant [R-252-000-B59-114].

The computational work for this article was performed on resources of the National Supercomputing Centre, Singapore (https://www.nscc.sg).

References Aziz, R. A.; Chu, G.; Muise, C.; and Stuckey, P. J. 2015. Stable model counting and its application in probabilistic logic programming. In AAAI. Baluta, T.; Shen, S.; Shinde, S.; Meel, K. S.; and Saxena, P. 2019. Quantitative verification of neural networks and its security applications. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 1249 1264. Bayardo Jr, R. J.; and Pehoushek, J. D. 2000. Counting models using connected components. In AAAI/IAAI, 157 162. Biondi, F.; Enescu, M. A.; Heuser, A.; Legay, A.; Meel, K. S.; and Quilbeuf, J. 2018. Scalable approximation of quantitative information flow in programs. In VMCAI, 71 93. Springer. Bomanson, J. 2017. lp2normal A Normalization Tool for Extended Logic Programs. In LPNMR, 222 228. Brik, A.; and Remmel, J. 2015. Diagnosing automatic whitelisting for dynamic remarketing ads using hybrid ASP. In LPNMR, 173 185. Springer. Brooks, D. R.; Erdem, E.; Erdo gan, S. T.; Minett, J. W.; and Ringe, D. 2007. Inferring phylogenetic trees using answer

The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)

set programming. Journal of Automated Reasoning, 39(4): 471. Clark, K. L. 1978. Negation as failure. In Logic and data bases, 293 322. Springer. Darwiche, A. 2002. A compiler for deterministic, decomposable negation normal form. In AAAI/IAAI, 627 634. Dodaro, C.; and Maratea, M. 2017. Nurse scheduling via answer set programming. In LPNMR, 301 307. Springer. Eiter, T.; Hecher, M.; and Kiesel, R. 2021. Treewidth-aware cycle breaking for algebraic answer set counting. In KR, volume 18, 269 279. Fages, F. 1994. Consistency of Clark s completion and existence of stable models. Journal of Methods of logic in computer science, 1(1): 51 60. Fichte, J. K.; and Hecher, M. 2019. Treewidth and counting projected answer sets. In LPNMR, 105 119. Springer. Fichte, J. K.; Hecher, M.; Morak, M.; and Woltran, S. 2017. Answer Set Solving with Bounded Treewidth Revisited. In LPNMR, 132 145. Gebser, M.; Kaufmann, B.; Neumann, A.; and Schaub, T. 2007. Conflict-driven Answer Set Enumeration. In LPNMR, volume 4483, 136 148. Gelfond, M.; and Lifschitz, V. 1988. The stable model semantics for logic programming. In ICLP/SLP, volume 88, 1070 1080. Giunchiglia, E.; Lierler, Y.; and Maratea, M. 2006. Answer set programming based on propositional satisfiability. Journal of Automated reasoning, 36(4): 345 377. Jakl, M.; Pichler, R.; and Woltran, S. 2009. Answer-Set Programming with Bounded Treewidth. In IJCAI, volume 9, 816 822. Janhunen, T. 2004. Representing normal programs with clauses. In ECAI, volume 16, 358. Janhunen, T. 2006. Some (in) translatability results for normal logic programs and propositional theories. Journal of Applied Non-Classical Logics, 16(1-2): 35 86. Janhunen, T.; and Niemel a, I. 2011. Compact Translations of Non-disjunctive Answer Set Programs to Propositional Clauses, 111 130. Kabir, M.; Everardo, F. O.; Shukla, A. K.; Hecher, M.; Fichte, J. K.; and Meel, K. S. 2022. Approx ASP a scalable approximate answer set counter. In AAAI, volume 36, 5755 5764. Kabir, M.; and Meel, K. S. 2023. A Fast and Accurate ASP Counting Based Network Reliability Estimator. In LPAR, volume 94, 270 287. Korhonen, T.; and J arvisalo, M. 2021. Integrating tree decompositions into decision heuristics of propositional model counters. In CP. Lagniez, J.-M.; and Marquis, P. 2017. An Improved Decision-DNNF Compiler. In IJCAI, volume 17, 667 673. Lee, J.; and Lifschitz, V. 2003. Loop formulas for disjunctive logic programs. In ICLP, 451 465. Springer. Lifschitz, V. 2010. Thirteen definitions of a stable model. Fields of logic and computation, 488 503.

Lifschitz, V.; and Razborov, A. 2006. Why are there so many loop formulas? ACM Transactions on Computational Logic (TOCL), 7(2): 261 268. Lin, F.; and Zhao, Y. 2004. ASSAT: computing answer sets of a logic program by SAT solvers. Artificial Intelligence, 157(1): 115 137. Marek, V. W.; and Truszczy nski, M. 1999. Stable models and an alternative logic programming paradigm. In The Logic Programming Paradigm, 375 398. Springer. Nouman, A.; Yalciner, I. F.; Erdem, E.; and Patoglu, V. 2016. Experimental evaluation of hybrid conditional planning for service robotics. In International Symposium on Experimental Robotics, 692 702. Springer. Samer, M.; and Szeider, S. 2007. Algorithms for propositional model counting. In LPAR, 484 498. Springer. Sharma, S.; Roy, S.; Soos, M.; and Meel, K. S. 2019. GANAK: A Scalable Probabilistic Exact Model Counter. In IJCAI, volume 19, 1169 1176. Thurley, M. 2006. sharp SAT counting models with advanced component caching and implicit BCP. In SAT, 424 429. Springer. Tiihonen, J.; Soininen, T.; Niemel a, I.; and Sulonen, R. 2003. A practical tool for mass-customising configurable products. In ICED. Valiant, L. G. 1979. The complexity of enumeration and reliability problems. SIAM Journal on Computing, 8(3): 410 421.

The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)