Neural Decision-Propagation for Answer Set Programming

1 Introduction

Neuro-symbolic AI aims to develop systems that bring together robust learning in neural networks with reasoning via symbolic representations [d'Avila Garcez and Lamb, 2023; Wang et al., 2025]. There has been a growing interest in using logic programming as a general symbolic reasoning framework for such integrated systems [Evans and Grefenstette, 2018; Yang et al., 2020; Manhaeve et al., 2021]. Answer Set Programming (ASP), a declarative programming paradigm widely used for knowledge representation and reasoning tasks [Lifschitz, 2008; Brewka et al., 2011], is used in such systems. Neuro-symbolic integration in ASP has been attempted in various domains such as Visual Question Answering [Eiter et al., 2022], compliance checking [Barbara et al., 2023] and many more [Borroto et al., 2025].

One prominent approach to accomplishing neuro-symbolic integration with ASP is to train neural networks with symbolic knowledge expressed with ASP. NeurASP [Yang et al., 2020] integrates neural atoms into ASP programs, allowing neural network outputs to be directly incorporated into symbolic reasoning and learning. SLASH [Skryagin et al., 2023] extends this line of work with neural-probabilistic predicates and removes low-probability predicate outcomes before ASP solving, thereby reducing the number of stable models that must be considered. However, these approaches largely follow a hybrid design in which neural components and symbolic ASP solvers remain separated by an interface: continuous neural predictions must be translated into symbolic atoms/literals, constraints, or probabilistic facts before reasoning can be performed. This introduces a combinatorial grounding problem, as the system must reason over multiple candidate associations between perceptual entities and symbolic objects before being processed by an ASP solver.

To connect neural outputs and symbolic representations smoothly, it would be desirable to compute answer sets in continuous domains. Then, to make this connection easily, we first propose a novel method for computing stable models called decision-propagation (DProp). A DProp run iteratively alternates between the following two phases: (i) decision, which selects undecided atoms to commit to false nondeterministically, and (ii) propagation, which updates the current partial assignment by deriving consequences of the program under the current assumptions. We then prove that successful DProp computations (runs that end without contradictions) capture the stable model semantics.

Subsequently, we propose Neural DProp (NDProp), a differentiable extension of DProp. NDProp uses neural networks for falsity decisions and fuzzy logic operators for propagations. As NDProp is identical to DProp in the crisp case, it is able to prove stability when the outputs are binary under a certain condition, making it easy to train in an unsupervised manner. These make the integration of NDProp into neuro-symbolic systems seamless, while still preserving a clear connection to classical stable model semantics. Furthermore, the learned decision steps and parallel capabilities via GPUs make this approach significantly more scalable.

To demonstrate the effectiveness of NDProp, we conduct three kinds of experiments: (1) random ASP solving to determine whether NDProp can learn the solving dynamics for given ASP problems, (2) neuro-symbolic integration to determine whether using NDProp has merits over existing approaches that use classical solvers, and (3) fuzzy reasoning to determine whether NDProp can reason and find stable models given fuzzy values as input. The results show that NDProp performs better than the respective baselines; it is superior with respect to accuracy, and has much higher inference speed than existing ASP-based neuro-symbolic approaches.

In summary, our contributions are:

• We introduce a novel method for computing stable models called DProp, and prove that a successful DProp computation captures stable model semantics.
• We develop NDProp, a differentiable extension of DProp that uses neural decisions and fuzzy propagations, and show that it coincides with DProp at the crisp case.
• We analyze the capabilities of NDProp in learning the solving dynamics of random ASP problems, and attempt to integrate NDProp into neuro-symbolic frameworks.
• We demonstrate that NDProp performs better than respective baselines, specifically with accuracy and inference speed.

Consequently, we propose a fully-differentiable answer set solver based on novel fixpoint semantics, yielding improved scalability compared to previous neural approaches to ASP. 1

2 Preliminaries

2.1 Answer Set Programming

Answer Set Programming (ASP) is a declarative paradigm based on non-monotonic logic and is widely used for knowledge representation and reasoning [Lifschitz, 2008; Brewka et al., 2011]. A rule r in a (normal logic) program P has the form

where a, bi, and cj are atoms and not denotes default negation. For a rule r of the form (1), the atom a is the head of the rule denoted as H(r), and b1, . . . , bm, not c1, . . . , not cl is the body of the rule denoted as B(r). The sets B+(r) = {b1, . . . , bm} and B-(r) = {c1, . . . , cl} represent the positive and default-negated body atoms of r, respectively. An interpretation I, i.e., a subset of the set A of all atoms, is a model of P if it satisfies each rule r of P, i.e., B+(r) ⊆ I and B-(r) ∩ I = ∅ imply H(r) ∈ I. Furthermore, I is a stable model (answer set) of P if it is the least model of the Gelfond-Lifschitz reduct P I , which is obtained from P by deleting every rule whose negative body intersects I and removing all negative literals from the remaining rules.

Given two interpretations I, J and a normal logic program P , an immediate consequence operator with respect to J [Van Gelder, 1993] is defined as

We define C 0P,J (I) = I and C k+1 P,J (I) = CP,J(C kP,J (I)) for integer k (≥ 0). When P + is a definite program, i.e., a program whose rule contains no default negation (l = 0), for fixed J there is a least fixpoint of CP +,J starting from ∅, which is the least model of P +, denoted as C∞ P +,J (∅) [van Emden and Kowalski, 1976]. Then, the next lemma holds.

1 A full version of this paper with appendices is available as [Eiter et al., 2026]. The code is available at https://github.com/sotam2369/ NDProp.

Proof. Let TP be the immediate consequence operator of a definite program P, and write T ∞ P (∅) for the result of iterating TP from ∅ to its least fixpoint. By definition, S is a stable model of P iff S = T ∞ P S (∅), where P S is the GelfondLifschitz reduct. For normal programs, iterating CP,S from ∅ coincides with iterating TP S , so C∞ P,S (∅) = T ∞ P S(∅). Hence S is stable iff S = C∞ P,S (∅).

2.2 Fuzzy Interpretations

In many real-world settings it is necessary to reason with vague or incomplete information. Fuzzy Answer Set Programming (FASP) extends ASP by interpreting atoms with a truth degree in the interval [0, 1] and evaluating rule bodies, while adopting stable-model-based semantics for fuzzy interpretations [Nieuwenborgh et al., 2006; Alviano and Pe˜naloza, 2013].

Let A be a set of propositional atoms. A fuzzy interpretation is a mapping I : A → [0, 1] assigning each atom a degree of truth. To evaluate rule bodies, FASP fixes a t-norm ⊗ : [0, 1]2 → [0, 1] (fuzzy conjunction), i.e., a commutative, associative and monotone operator with unit 1. Typical t-norms include G¨odel, Product, and Łukasiewicz. Similarly, t-conorm ⊕ : [0, 1]2 → [0, 1] represents fuzzy disjunction.

For a rule r of the form (1), the degree to which the body is satisfied under I is

where default negation is interpreted using strong negation I(not c) = 1 - I(c).

3 Decision-Propagation for ASP

In this section, we describe DProp computations, and show that successful DProp computations capture stable model semantics. DProp uses a forward chaining approach similar to [Lef`evre et al., 2017; Dal Pal`u et al., 2009], with the biggest difference being that the decisions are made at an atom and not at a rule level, making the differentiable extension much simpler.

Formally, DProp operates on an atom set A of P , with each state splitting A into disjoint true, false, and undecided sets T , F , and U = A\ (T ∪F ), respectively. With initial sets T 0 = C∞ P,A(∅), F 0 = ∅, and U 0 = A \ (T 0 ∪ F 0 ), a run in DProp performs the following iterations (k ≥ 1) until termination:

1. Decision. Select an undecided atom a ∈ U k-1 (via some policy), then update F k = F k-1 ∪ {a}.
2. Propagation. With F k fixed, compute T k = C∞ P,A\F k(T k-1 ) and set U k = U k-1 \ (T k ∪ F k ).
3. Termination. If U k = ∅, stop and return T k ; otherwise continue to the next decision.

When a run terminates, we write k = ∞, obtaining T ∞, F ∞, and U ∞. Here, both T and F increase monotonically because Propagation and Decision never remove atoms from them.

Lemma 2. A DProp run always terminates for a finite atom set A.

Proof. Decisions always remove an atom a from U k at every iteration. Thus, the number of DProp iterations is finite, if the atom set A is finite.

Definition 1 (Successful DProp computation). A successful DProp computation is a DProp run that terminates with U ∞ = ∅ and T ∞ ∩ F ∞ = ∅.

The following properties of the operator CP,I(J) are not hard to see.

Proof. Let J = A \ F and J ′ = A \ F ′ . Since F ⊆ F ′ , we have J ′ ⊆ J. If a rule satisfies B-(r) ∩ J = ∅, then also B-(r) ∩ J ′ = ∅. As the reducts P J and P J ′ are obtained by removing rules whose negative body intersects J and J ′ respectively, and removing negative literals from the remaining rules, P J ⊆ P J ′ . By standard properties of definite programs, their least models are monotone with respect to program inclusion, yielding T ∞ P J (∅) = C∞ P,A\F (∅) ⊆ T ∞ P J′ (∅) = C∞ P,A\F ′ (∅).

Proof. By assumption, T k-1 ⊆ C∞ P,A\F k(∅). Since CP,A\F k is monotone and C∞ P,A\F k(∅) is its fixpoint, for every n ≥ 0 we have C n P,A\F k(∅) ⊆ C n P,A\F k(T k-1 ) ⊆ C∞ P,A\F k(∅). Since A is finite, there exists m such that C m P,A\F k(∅) = C∞ P,A\F k(∅). Hence, C∞ P,A\F k(∅) ⊆ C m P,A\F k(T k-1 ) ⊆ C∞ P,A\F k(∅), so C m P,A\F k(T k-1 ) =

Theorem 1. Let P be a finite program and S ⊆ AP , where AP is the set of atoms occurring in P. Then S is a stable model of P if and only if S is the final true set of a successful DProp computation.

Proof. (⇒) Let S be a stable model of P, and F k-1 , T k-1 and U k-1 be the sets of atoms that are true, false and undefined at the beginning of the k-th iteration, where k = ∞ is the final iteration. Consider a run of DProp that at each step decides the falsity of an atom a ∈ (A \ S) ∩ U k-1 . The propagation step then yields T k = C∞ P,AP \F k (T k-1 ), which by Lemma 4 equals C∞ P,AP\F k(∅). Because F k ⊆ AP \ S, we have S ⊆ AP \ F k and hence, by Lemma 3, C∞ P,AP\F k(∅) ⊆ C∞ P,S (∅). By Lemma 1, C∞ P,S (∅) = S, so T k ⊆ S and T k ∩F k = ∅ for all k. At termination, U ∞ = ∅, so T ∞ = C∞ P,AP \F ∞(∅) = C∞ P,T ∞(∅) hence T ∞ = S from Lemma 1. From Lemma 2, the computation will terminate as the given program P is finite.

(⇐) Let S be the final true set of a successful DProp computation, and T ∞-1 and F ∞ be the true and false sets before the final propagation step. As the propagation step does not modify F ∞, from Definition 1, S = A \ F ∞ so S = C∞ P,A\F ∞(T ∞-1 ) = C∞ P,S (T ∞-1 ). From Lemma 4, C∞ P,S (T ∞-1 ) = C∞ P,S (∅), and Lemma 1 implies that S is a stable model of P .

Remark 1 (Batch decisions). The proof only relies on the fact that F grows monotonically and is held fixed during propagation. Hence any variant that, in a single decision step, adds a set E ⊆ U to F (i.e., F ← F ∪ E) satisfies the same invariants and therefore admits the same characterization: every DProp computation of such a variant yields a stable model.

4 Neural Decision-Propagation

We now instantiate DProp with differentiable operators, yielding a neural solver NDProp that is an extension of DProp. The overview of the NDProp pipeline is shown in the middle section of Figure 2. Corresponding to the true and false sets T and F, we consider true and false degrees (τ, ϕ) ∈ [0, 1]n × [0, 1]n . Furthermore, decisions are implemented via neural decision modules that gradually increase falsity.

4.1 Neural Extensions of DProp

Each atom ai carries a true and false degree τi and ϕi. Literal evaluations are done with the val operator, which outputs for positive and negative literals

respectively. Regarding (τi, ϕi), values near (0, 0) indicate undecided atoms, (1, 0) denotes derived truth, (0, 1) denotes explicit falsity, and (1, 1) encodes contradiction. For NDProp, we combine these into a single membership score

which serves as the atom's soft truth value indicating whether the atom should be included in the answer set or not. Importantly, this becomes binary iff (τi, ϕi) is (1, 0) or (0, 1), meaning that if the variable is either undecided (0, 0) or (1, 1) contradictory, the score will never become binary. We denote by (τ t , ϕt ) the degrees at iteration t.

Decision Phase

Decisions update only ϕ while holding τ fixed, as in DProp. Given a t-norm ⊗ and t-conorm ⊕, the undecided degree µi for atom ai is defined as

We then produce decisions via a neural decision module, which in this case is a Recurrent Neural Network (RNN) that takes the current input and hidden state st-1 and yields the decision logits dt and updated hidden state st as follows:

where ∥ denotes the concatenation operation. RNNs retain historical information with the hidden states st , making it suitable for our approach that requires producing decisions over multiple steps. We then apply a sigmoid function σ : R → (0, 1) on the decision logits to yield the decision scores:

The falsity degrees move toward these selections via

with ⊙ denoting elementwise multiplication. Note that ϕt+1 remains in [0, 1], since µt ≤ 1 - ϕt and δt ∈ (0, 1). Because µt becomes zero for already decided atoms, this additive rule directly mirrors the discrete falsity decision (F t = F t-1 ∪ E cf. Remark 1) when (τ t , ϕt ) and δt are binary.

Propagation Phase

Propagation updates only τ while holding ϕ fixed, as in DProp. Given a t-norm ⊗ and t-conorm ⊕, for each rule rj, its rule body contributes support

Each head atom ai aggregates these supports via the soft immediate consequence operator

Given ϕt+1 , we update τ from the current state τ t by iterating CP,ϕt+1 until convergence:

In practice, we stop the iteration early when the maximum change between successive applications of CP,ϕt+1 falls below a fixed convergence threshold, or the iteration reaches a given pre-defined value.

Crisp Case Recovers DProp

We give the proof that DProp can be emulated with a specific constraint on NDProp, showing that NDProp is a differentiable extension of DProp.

Definition 2 (Set induced by ψ). Let ψ ∈ [0, 1]n be a real valued vector with the i-th value ψi corresponding to atom ai. The set induced by ψ is defined as

In the crisp case, the operator CP,ϕ makes the same atoms true as CP,A\F , that is:

Proof. With binary (τ, ϕ), a positive literal evaluates to τi ∈ {0, 1} and a default-negated literal evaluates to ϕi ∈ {0, 1} for atom ai. Thus each rule rj's support ρj(τ, ϕ) is 1 exactly when B+(rj) ⊆ [τ] and B-(rj) ⊆ [ϕ]. Aggregating supports via t-conorm ⊕ yields exactly the heads derived by CP,A\F (T), so the induced true set coincides.

Then we obtain the following property:

Proposition 1 (Crisp Case). Let (τ, ϕ) ∈ {0, 1}n × {0, 1}n , δ ∈ {0, 1}n , and propagation compute the fixpoint of CP,ϕ. Then, one update of NDProp coincides with one iteration of DProp.

Proof. With binary (τ, ϕ), the set induced by undecided degree µ = (1 - τ ) ⊗ (1 - ϕ) corresponds to U = A \ (T ∪ F ) when T = [τ ] and F = [ϕ]. Thus, the update ϕ′ = ϕ+(µ⊙δ) coincides with F ′ = F ∪ (U ∩ [δ]). From Remark 1, deciding falsity of a set of atoms is fine, thus this exactly coincides with the decision step of DProp when the falsity of a set of atoms U ∩ [δ] is decided.

Since (τ, ϕ′ ) ∈ {0, 1}n × {0, 1}n , from Lemma 5 [CP,ϕ′(τ)] = CP,A\F ′(T). When CP,ϕ′(τ) is applied until a fixpoint, this exactly coincides with the propagation step of DProp. Furthermore, when µ, δ is binary, τ and ϕ are guaranteed to be binary as well.

4.2 Loss Alignment

We prove that enforcing NDProp to output binary values is equivalent to enforcing stability. Here, ψ′ ≤ ψ is equivalent to ∀i (ψ′i ≤ ψi) and 0 and 1 are n-dimensional vectors of all 0s and all 1s, respectively.

Proof. For fixed τ, negative literals evaluate as val(not ai) = ϕi. Since the t-norm ⊗ and t-conorm ⊕ are monotone in each argument, ϕ ≤ ϕ′ implies each rule support ρ(τ, ϕ) ≤ ρ(τ, ϕ′ ), hence CP,ϕ(τ) ≤ CP,ϕ′(τ). Because CP,ϕ ≤ CP,ϕ′ pointwise, iterating from 0 yields C kP,ϕ (0) ≤ C kP,ϕ′(0) for all k, and taking the limit gives C∞ P,ϕ (0) ≤ C∞ P,ϕ′ (0).

Proof. The operator CP,ϕt is monotone in τ by monotonicity of ⊗ and ⊕. Since τ t-1 ≤ C∞ P,ϕt (0) and C∞ P,ϕt (0) is a fixpoint of CP,ϕt , for every n ≥ 0 we have C n P,ϕt (0) ≤ C n P,ϕt (τ t-1 ) ≤ C∞ P,ϕt(0). Taking limits yields C∞ P,ϕt (τ t-1 ) = C∞ P,ϕt (0).

Theorem 2 (Binary terminal state yields stability). Let P be a finite program and S ⊆ AP , where AP is the set of atoms occurring in P. Then S is a stable model of P if and only if propagation is applied until convergence with the resulting membership score pi ∈ {0, 1} and S = [p].

Proof. (⇐) Let p ∈ {0, 1}n be the membership score obtained from (τ ∞, ϕ∞), and let T = [τ] and F = [ϕ]. Since pi = 12 (τi + 1 - ϕi) and τ ∞ i , ϕ∞i ∈ [0, 1], pi ∈ {0, 1} implies (τ ∞ i , ϕ∞i ) ∈ {(1, 0), (0, 1)}, and thus T ∩ F = ∅, T ∪ F = A and T = [p]. ϕ increases monotonically as there are no negatives in Equation (2). As propagation is applied until convergence τ ∞ = C∞ P,ϕ∞(τ ∞-1 ), and from Lemmas 6 and 7, τ ∞ = C∞ P,ϕ∞(0). Since [0] = ∅, from Lemma 5, [τ ∞] = [C∞ P,ϕ∞(0)] = C∞ P,A\F (∅) = C∞ P,T (∅). From Lemma 1, [p] = [τ ∞] is thus a stable model of P.

(⇒) Let τ ∞ and ϕ∞ be the true and false degrees after the final iteration. From Proposition 1, if we set the decision scores to be binary and make the propagation phase compute until a fixpoint of CP,ϕ, the iteration coincides with a DProp iteration. From Theorem 1, there exists a successful DProp computation that ends with the stable model S, and since τ, ϕ is binary, T ∩F = [τ ∞] ∩ [ϕ∞] = ∅ and U = ∅, (τ ∞, ϕ∞) ∈ {(1, 0), (0, 1)} and thus p is binary and [p] = S.

From Theorem 2, we can conclude that when the output p of NDProp is trained with a loss function that enforces binary outputs, it inherently forces the NDProp to learn to output stable models, given that the final propagation is done until convergence. This holds even with a single iteration, since the decision step can falsify a set of atoms at once, c.f. Remark 1.

5 Experiments

In this section, we perform experiments to answer the following three questions:

• (Q1) Can NDProp learn to solve ASP problems?
• (Q2) Can NDProp compete with existing ASP-based neuro-symbolic frameworks?
• (Q3) What are novel settings in explicit need of NDProp?

5.1 RandomLogic Programs

To assess NDProp's behavior on unstructured problems, we first evaluate it on randomly generated logic programs. Random instances are utilized to evaluate neural approaches to symbolic solving, e.g., in Boolean Satisfiability [Selsam et al., 2019], where they are used to evaluate whether learned models can learn to solve problems that are generally difficult to find heuristics for.

We follow the linear model L(N2, c1, c2) for random negative two-literal (N2L) programs [Wang et al., 2015]. For n atoms, each pure rule a ← not b (with a ̸= b) appears independently with probability c1/n and each contradiction rule a ← not a appears with probability c2/n. Random N2L programs are attractive for an experimental setting as they are easy to produce, while being considerably difficult, as it includes NP-complete instances. The same setting has been used in other work that attempted to apply GNNs to Answer Set Computation [Ielo and Ricca, 2021].

As supported models of N2L programs are known to be stable models as well, we look at problems that are not in this regard. Specifically, we look at the k-LP(N,L) generator that has been studied for phase transitions in ASP [Zhao and Lin, 2003]. We use the 3-LP generator, which has been shown to be hard around L/N = 5, where L and N correspond to the number of rules and atoms respectively.

Setup

We focus on having three datasets per generator (N2L, and 3-LP) with different number n of atoms. Specifically, we use easy (5-10), medium (11-50), and hard (51-100). We specifically use the hard set to determine whether the model is able to generalize to bigger problems. Each dataset consists of 1000 training and 100 validating instances and 100 testing instances. As the baseline, we implement RDProp, which is DProp with random decisions. We test RDProp with 1, 10, and 100 restarts, denoted as RDProp-1, RDProp-10, and RDProp-100 respectively. We compare NDProp with RDProp to see whether NDProp is able to learn the decision making process to outperform random decisions.

For NDProp, we train for 1000 epochs, with the setup of an iteration of 10 (50 at test time), a hidden dimension of 32, a logical dimension of 32, a learning rate of 1 × 10-3 , and the G¨odel t-norm. The logical dimension means the model maintains multiple logical states at once, and we select the state whose output is closest to binary at the end. For the loss function, we use the smallest Binary Cross Entropy (BCE) loss over all stable models as the objective function.

Results

Table 2 provides the percentage of problems in each test set solved. The results show that NDProp is effectively learning the decision dynamics for solving random problems. Specifically, NDProp is shown to completely outperform RDProp in the 1-shot setting, with performance on medium and easy training datasets exceeding that of 100-shot RDProp. This empirically supports our claim that NDProp is an extension of DProp, and that it can learn the decision heuristics for finding stable models for logic programs.

5.2 Neuro-Symbolic Tasks

As NDProp can approximate answer sets differentiably, it is natural to combine with existing neural networks based architectures to perform neuro-symbolic inference. In all settings, the input consists of one or more MNIST images, and supervision is provided only through arithmetic relations between the underlying concepts, rather than through perimage labels [Manhaeve et al., 2021; Gaunt et al., 2017; Tsamoura et al., 2021]. The goal is therefore to jointly learn perception using symbolic reasoning from weak, relational supervision. This will allow us to evaluate the merits of using an end-to-end differentiable system, as opposed to a system that relies on separate training of the perception module and the reasoning module.

ASP Encodings. In contrast to prior neuro-symbolic ASP systems that use neural predicates to interface with perception modules [Yang et al., 2020], we adopt a different strategy. We embed the output of neural models as fuzzy facts into a fixed ASP program that encodes the arithmetic constraints (Figure 2). While this may seem to force NDProp to perform as a FASP solver, the objective is to produce binary outputs, explicitly forcing the backbone perception model to predict binary values as well.

Setup

In this experiment, we perform evaluations on six variants of the MNIST-based arithmetic reasoning tasks that are commonly used as neuro-symbolic benchmarks [Yang et al., 2020; Manhaeve et al., 2021]: 1 and 2 digit addition, Add2x2, Apply2x2 (with handwritten operator images) and 3 and 5 digit membership. For NDProp, we use the setup with iteration of 1, hidden dimension of 8, logical dimension of 2, learning rate of 1 × 10-3 , and product t-norm.

We compare the performance of NDProp with ASP-based neuro-symbolic systems: NeurASP [Yang et al., 2020] and SLASH [Skryagin et al., 2023]. Experiments are conducted with a maximum of 10 epochs for all approaches, with a timeout set to 3000 seconds; the training is cut off when the budget is reached, and accuracy is checked at the end of the epoch. The training setup used is identical to those given in the original papers.

Results

Table 1 reports recognition accuracy, inference accuracy (accuracy of final output), and runtime (seconds) for both training and testing splits, averaged over 3 runs. Across six neurosymbolic tasks, NDProp achieves higher digit and inference accuracy than NeurASP and SLASH for five, with the exception of the Addition2 task, where SLASH has a slightly higher recognition and inference accuracy. Empirically, this shows the benefits of using end-to-end trainable systems: jointly optimizing perception and reasoning leads to more cohesive and consistent outputs, leading to performance similar to or better than systems that rely on symbolic solvers. This is similar to findings in prior works that use differentiable computation of supported models [Takemura and Inoue, 2024], yielding faster training time and higher accuracy in certain setups.

Furthermore, the training time for NDProp is significantly faster than NeurASP and SLASH. Specifically, for the Member5 task, both NeurASP and SLASH fail to train even one epoch within the time budget, leading to very low accuracy. On the other hand, NDProp has a longer training time for Apply2x2; this is thought to be because there are extremely many grounded atoms in this task, which have to be processed at once for the forward pass of NDProp, leading to a much higher computational cost.

The difference is more prominent in the testing speed, where NDProp is an average of 41.8 times faster than NeurASP, and 6.8 times faster than SLASH. This is mainly due to the GPU capabilities of NDProp; GPUs allow for higher parallelization, allowing our model to process multiple instances with one forward pass, even during testing. In comparison, NeurASP can only process one instance at a time, while SLASH can process multiple instances only at training time.

5.3 Reasoning with Incomplete Data

In this experiment, we look at settings where data is incomplete. Given the predicted outputs of models with incomplete training, NDProp can add a layer of reasoning on top, yielding a solution that is both correct in terms of the given requirements and is able to account for the information given by the incomplete data.

Setup

Visual sudoku is a task where each cell has an image corresponding to a number, and the goal is to find the correct solution for the given grid, with MNIST being the most common image used. In this experiment, we hypothesize a setting where the neural network is fixed; we pretrain the model on MNIST images, and reason on its predictions to find the solution to the task. By having models that are trained on less data, we can simulate a situation in which the given predictions are not correct 100% of the time.

We specifically focus on the 4x4 setting with each cell containing an image with a number between 0-4 (0 for empty cell). We vary the amount of labeled training data for the MNIST predictor (100%, 50%, 10%, 5% and 1%) with 500 steps of training, to test whether the framework can perform under imperfect settings. We compare against two baselines that use the same predictions:

• ASP: Give the current predictions other than 0 as a fact, and solve the ASP program.
• Neural: Train a neural classifier that takes as input the predicted values of each cell (0 for empty cells), and predict the digit in each cell. This is trained until convergence.

In this setting, our framework is used in a separate way to the neuro-symbolic tasks. As the input facts are not trained to become binary, we use the facts only as a heuristic to guide NDProp to a solution. This is provided through the RNN's initial hidden states s0 for each atom, which is computed by a single-layer MLP. We train for 100 epochs (which is sufficient for the model to converge) using NDProp with iterations of 3, hidden dimension of 8, logical dimension of 2, learning rate of 1×10-3 , and G¨odel t-norm.

Results

Table 3 shows the percentage of problems where all digits for each cell were given correctly over 3 runs. In every setup, we can see that NDProp performs the best, with constant gains against the second best method. An interesting trend that can be observed is that when the amount of data goes up, the ASP baseline performs much better. This is because when the predictions are correct, a complete reasoning mechanism will always get the correct solution.

On the other hand, while increasing the performance of the digit classifier does not have too dramatic of an impact for the neural method, we can see that the deterioration in performance is much smaller. This shows that neural models in general are very strong with imperfect inputs, showing merits over classical methods that completely plummet at 1%. NDProp is able to achieve the best of both worlds: when the predictions are accurate, NDProp can properly reason on them to get the correct solution, and when the predictions are less accurate, it uses the information to find a solution that is most compatible with the predictions.

6 RelatedWork

6.1 ASP Solvers

Classical ASP systems such as smodels [Niemel¨a and Simons, 1997] and DLV [Leone et al., 2006] perform 2valued branching search by first examining the true case and then the false case (or vice-versa). Later systems such as clingo [Gebser et al., 2016] and WASP [Alviano et al., 2013] adopt CDCL-inspired architectures that combine deterministic propagation with branching decisions, allowing for more efficient search and learning from conflicts.

DProp differs from these systems in that it focuses on deciding only the falsity of atoms and propagating the true atoms. Furthermore, this design treats stability as a result of computation: when the solution is contradiction-free, stability is guaranteed (Theorem 1). These features enable a differentiable extension by NDProp, whose crisp case provably retains the same theoretical properties as DProp. Such differentiable extensions are not easily achievable with existing ASP solvers.

Fuzzy answer set programming is an extension of ASP to handle degrees of truth using fuzzy logic [Nieuwenborgh et al., 2006; Alviano and Pe˜naloza, 2013]. These approaches adapt the stable model semantics to allow the use of fuzzy truth values, often employing t-norms to define rule satisfaction and model construction.

6.2 Fixpoint Semantics

A wide range of fixpoint semantics for ASP have been proposed in the literature. Earlier works formalized nondeterministic fixpoint computation in various ways. For example, Sacc`a and Zaniolo [1990] incorporate a backtracking mechanism into bottom-up search, and Inoue and Sakama [1996] characterize a parallel procedure to compute stable models [Inoue et al., 1992; Shirai and Hasegawa, 2004] by a fixpoint operator with case splitting and constraints. Efficient search strategies to limit the number of case splitting during fixpoint computation could be learned by machine learning techniques, but there has been no such attempt yet.

Fages [1991] shows a non-contradictory strategy for justification-based derivation like truth maintenance system yields a stable model at a fixpoint. Similarly, the notion of persistent computation by Liu et al. [2010] selects applicable rules to compute stable models, and the idea leads to ASP solvers GASP [Dal Pal`u et al., 2009] and ASPeRiX [Lef`evre et al., 2017]. Such a selection strategy is similar to DProp, which captures stable models as computations of iterations using propagation and choice. The main difference is that in GASP and ASPeRix, the choice is performed on all negative body literals of a chosen rule, while DProp performs decisions on any undecided atom; the latter eases extension into the continuous domain.

Several works characterize stable models via alternating fixpoints and approximation operators [Fitting, 2002]. The alternating fixpoint theory [Przymusinski, 1991] defines stable models as fixpoints of an operator that alternates between deriving positive and negative information. Denecker et al. [2000] develop an approximation theory that captures various non-monotonic semantics including stable models, through the use of approximating operators and their fixpoints. These frameworks yield stable models in different ways than DProp, which directly produces stable models through propagation-decision steps.

6.3 Neural Answer Set Solving

Neurosymbolic integration of ASP is a field being actively explored. NeurASP [Yang et al., 2020] finds stable models of programs that contain neural atoms using symbolic solvers, and uses the results to train the neural perception model. SLASH [Skryagin et al., 2023] extends this system to support joint distributions, richer queries, and scalable inference.

In contrast to works that use classical ASP solvers, several works have explored the use of differentiable approaches for solving ASP problems. One approach to accomplish this is by using deep learning with discrete solvers such as clingo. Differentiable ASP/SAT [Nickles, 2018] compute stable models with ASP solvers utilizing derivatives of a cost function, and Dodaro et al. [2022] explore the use of deep learning to generate domain-specific solvers for WASP.

Another differentiable approach is to directly compute supported or stable models in vector spaces. Aspis et al. [2020] use a matrix representation of logic programs to compute supported models, and solve a root-finding problem using Newton's method. Takemura and Inoue [2022] propose another matricized method by defining a cost function that yields a supported model when the cost is minimized to be zero. Sato et al. [2026] extend such matricized methods by encoding loop formulas in vector spaces, so that stable models can be obtained by minimizing a single objective. Ielo and Ricca [2021] use GNNs to solve negative two literal programs, which are known to have the property that all supported models are stable models. GNNs have been used in Boolean constraint solvers other than ASP, such as Boolean Satisfiability [Selsam et al., 2019] and Maximum Satisfiability [Moriyama and Inoue, 2025], with the latter specifically showing that t-norms are beneficial for developing differentiable solvers. Our approach is classified as a differentiable approach as well, with the main differences being how the solutions are being computed: prior works use the cost function to optimize the variable assignments, while NDProp uses a propagation-decision process to search for stable models, with the decision heuristics being learned. Additionally, our work requires only binarization to get stable models rather than supported models, while prior works require the use of loop formulas or do not consider it at all.

7 Conclusion

We have presented decision-propagation (DProp), a novel method for computing stable models. DProp alternates between falsity decisions and truth propagations, and a successful DProp computation is shown to capture the stable model semantics. We then proposed NDProp, a differentiable extension of DProp that uses neural decisions and fuzzy propagations, and show that it coincides with DProp at the binary limit. Experiments on random logic programs and neurosymbolic benchmarks show that NDProp is able to learn to solve ASP problems, and can be combined with neural models to train end-to-end. Compared to existing approaches that use symbolic reasoning, our approach incorporates learning in the reasoning step as well, resulting in a higher accuracy. The results display the power of a differentiable and learnable solver in pipelines where reasoning is required.

Throughout the experiments, we have noticed that some tnorms work better than others in each setting. An extensive study of t-norms in particular settings is left out for future work, as each t-norm has different properties that are beneficial in different settings [Eiter et al., 2025]. Another direction to explore is whether the semantics of NDProp aligns with FASP. At the moment, NDProp is aimed at normal logic programs, but with modifications, it could be used to solve fuzzy variants. Finally, extending the framework to support often used constructs such as constraints, choices and aggregates is left for future work. This would allow for use in more complex neuro-symbolic tasks, and would be an important step towards applying the framework to real-world scenarios.

Acknowledgements

This work has been supported by JSPS KAKENHI Grant Number JP25K03190, JST CREST Grant Number JPMJCR22D3 and Grant-in-Aid for JSPS Fellows Grant Number JP26KJ1236, Japan. This research was funded in whole or in part by the Austrian Science Fund (FWF) 10.55776/COE12. The authors thank colleagues in the KBS Group at TU Wien for helpful discussions.