Conflict Extraction in Probabilistic Datalog Analyses

Conflict Extraction in Probabilistic Datalog Analyses SIYU CHEN, Purdue University, USA CHUNGHA SUNG∗ , Amazon, Inc., USA XUYANG LI, Purdue University, USA JINGBO WANG, Purdue University, USA Probabilistic extensions of Datalog enable static analyses such as pointer analysis, data race detection, and side-channel analysis to rank alarms by likelihood, but this added expressiveness also introduces a new challenge absent from deterministic analyses: the final output may contain alarms that are individually plausible yet mutually inconsistent, because marginal probabilities do not guarantee joint satisfiability. As a result, developers may spend effort investigating combinations of alarms that can never co-occur in any possible world. We address this problem by formalizing such

arXiv:2608.10755v1 [cs.SE] 11 Aug 2026

inconsistencies as minimal unsatisfiable subsets (MUSes) and introducing PPProbe, a conflict extractor specialized for probabilistic Datalog analyses. Rather than improving MUS enumeration in general, PPProbe exploits the structure of Datalog derivation graphs to guide the search toward likely conflicts and prune the search space through bottom-up UNSAT inference. We evaluate PPProbe on 70 benchmarks from power side-channel analysis, data race detection, semantic diffing, and Bayesian-network inference. The results show that PPProbe achieves 2.5–24× higher throughput than state-of-the-art MUS enumerators, and that the conflicts it identifies yield a conservative estimate of false-positive reduction, filtering out an average of 47.7% of mutually inconsistent alarms. CCS Concepts: • Software and its engineering → Automated static analysis; Software verification. Additional Key Words and Phrases: probabilistic Datalog, program analysis, minimal unsatisfiable subsets

1

Introduction

While classical logic programming languages such as Datalog [11, 50] and Prolog are widely applied to domains like graph analysis [40, 41, 47], bioinformatics [33, 39], and program analysis [10, 22, 23, 30, 34, 36, 43, 45, 55–57, 59, 60], probabilistic extensions like ProbLog [13], Bingo [36], Praline [54] and Scallop [25] enhance expressiveness by modeling uncertainty for ranking and risk prioritization—such as in side-channel detection, where leakage probability yields more actionable insights than binary detection [19, 37, 48]. However, probabilistic reasoning fundamentally changes inference interpretation; unlike deterministic Datalog, which assumes a single world of facts, probabilistic languages consider exponentially many possible worlds. In this setting, two output facts may be valid in different worlds but mutually exclusive if no single world satisfies both–causing fundamentally incompatible outputs to appear simultaneously. This lack of ∗ The work is not related to the author’s position in the affiliation.

Authors’ Contact Information: Siyu Chen, Purdue University, West Lafayette, USA, chen5216@purdue.edu; Chungha Sung, Amazon, Inc., Seattle, USA, chunghs@amazon.com; Xuyang Li, Purdue University, West Lafayette, USA, li5274@purdue.edu; Jingbo Wang, Purdue University, West Lafayette, USA, wang6203@purdue.edu.

1

2

Chen et al.

Pre-processing

Probabilistic Datalog Program 𝑃

Probabilistic Dependencies & Datalog Derivations

Generating MUSes Derivative Sampling G, Φ

1

Prioritize Search Space

MUS Set 𝑆

Bottom-up UNSAT Inference

Probabilistic Encoding 2

Prune Search Space

Fig. 1. PPProbe– Overview of generating MUSes from the probabilistic Datalog program 𝑃.

visibility hinders tasks like program analysis, where developers must decide which alarms to investigate and trace to root cause. To systematically capture and explain these conflicts, we represent them as minimal unsatisfiable subsets (MUSes)—minimal sets of output facts whose conjunction is unsatisfiable (UNSAT) while every proper subset is satisfiable—thereby isolating the exact sources of inconsistency. Despite extensive study, MUS generation remains challenging because of its exponential search space. To improve scalability, prior work has proposed both domain-agnostic [6, 7, 9, 26–28] and domain-aware [5, 12, 16, 17, 51] techniques. Domain-agnostic methods iteratively manage blocking constraints to prune infeasible candidates and perform well on Boolean satisfiability benchmarks, but they do not scale well to probabilistic Datalog because they ignore the structural and statistical dependencies in Datalog derivation graphs. Domain-aware methods use specialized knowledge to guide the search more effectively, but they are often tightly coupled to specific settings and harder to adapt to the reasoning and application constraints of probabilistic models. To address these gaps, we propose PPProbe1 , a sound and efficient MUS generator for probabilistic Datalog programs. By sound, we mean that every MUS produced by PPProbe corresponds to a genuine conflict: the identified facts are mutually exclusive because their derivations rely on fundamentally incompatible conditions, and therefore cannot hold simultaneously in any valid interpretation. Figure 1 provides an overview of the approach. Given a probabilistic Datalog program 𝑃, PPProbe first invokes a standard solver to preprocess 𝑃, producing the queried output facts and the associated derivation graph G. These artifacts are then used to construct a constraint set Φ that encodes the probabilistic semantics of 𝑃, over which PPProbe identifies a collection of MUSes, each corresponding to a minimal subset of output facts whose conjunction is unsatisfiable under Φ. To address the exponential cost of checking candidate subsets for unsatisfiability and minimality, PPProbe employs two complementary techniques. The first, derivation-aware sampling, prioritizes the search by exploiting negative structural and statistical dependencies in the derivation graph G. By favoring relations 1 Abbreviation of Probabilistic Paradox Probe.

Conflict Extraction in Probabilistic Datalog Analyses

3

that depend on shared inputs in opposite ways, the sampler steers candidate generation toward highconflict regions that are more likely to be UNSAT. In addition, PPProbe performs static analysis to partition independent output facts into disjoint sets and restricts sampling within each set, further increasing the chance of discovering unsatisfiable candidates. Our second technique, bottom-up MUS inference, aggressively prunes the search space by deriving new conflicts from previously detected ones. Through a process of logical replacement, PPProbe traverses the derivation graph to systematically replace facts in a known MUS with their derivation ancestors. This mechanism allows the framework to synthesize additional MUSes without the overhead of SAT solver invocations, substantially reducing the total number of calls and accelerating the enumeration process. We implemented these techniques in PPProbe and evaluated them on 70 benchmarks spanning sidechannel (SC) vulnerability detection [54, 58], data race (DR) analysis [24, 36], semantic diffing (SD) [45], and Bayesian network inference [1]. We compare PPProbe against three state-of-the-art MUS enumerators: MARCO [26], ReMUS [9], and TOME [6]. Under a 30-minute time budget, PPProbe discovers substantially more MUSes than these baselines, including average improvements of 6.6× and 5.9× over MARCO, and 18× and 65× over ReMUS, on SC and DR, respectively. To demonstrate practical utility, we further apply PPProbe to three program analysis tasks (SC, DR, and SD) and use the detected MUSes to filter logically inconsistent critical queries. This MUS-based filtering significantly reduces the diagnostic search space, with average reductions of 61% in DR and 69% in SC. Contributions. In summary, this paper makes the following contributions: • We propose a sound and efficient MUS generator, PPProbe, tailored for extracting conflicts from probabilistic Datalog programs. • We develop a derivation-aware sampling technique that utilizes negative structural and statistical dependencies in the derivation graph to prioritize candidate generation. • We present a bottom-up MUS inference technique that proactively derives additional MUSes via logical replacement, pruning the exponential search space without additional solver overhead. • We demonstrate the effectiveness of our approach on 70 real-world benchmarks, achieving average throughput improvements of up to 65× over state-of-the-art tools, while indicating a potential 47.7% average reduction in false alarms. The remainder of this paper is organized as follows. Section 2 motivates our work with illustrative examples. Section 3 introduces the necessary preliminaries and background. Section 4 provides an overview of our approach. Sections 5 and 6 describe our techniques for prioritizing and pruning the search space. We present experimental results in Section 7, discuss related work in Section 8, and conclude in Section 9. 2

Motivation

We illustrate the challenges of detecting logical conflicts in probabilistic Datalog using power side-channel analysis—a foundational approach for evaluating software security [20, 24, 36, 54]. By adapting a simplified

4

Chen et al.

side-channel detection framework [58], we demonstrate how probabilistic reasoning introduces subtle, hidden conflicts that are easily overlooked in large-scale analyses.

1 2

% Datalog facts (input): user-provided input type annotations 1.0::inRand(r1). 1.0::inRand(r2). 1.0::inRand(r3). 1.0::inKey(k).

3 4 5 6

% Datalog facts (input): program semantics 1.0::and(c5,c3,r3). 1.0::and(c2,k,c1). 1.0::and(c3,c2,r2). 1.0::and(c4,c1,c2). 1.0::xor(c1,k,r1). 1.0::noIntersect(c2,r2).

7 8 9 10 11 12 13

% Datalog rules for inferring output types (rand, sid, key) 0.9::leak(OP1) :- inKey(OP1). % Rule 1 0.8::rand(OP1) :- inRand(OP1). % Rule 2 1.0::rand(O) :- inKey(OP1), inRand(OP2), xor(O,OP1,OP2). % Rule 3 0.7::leak(O) :- leak(OP1), rand(OP2), and(O,OP1,OP2). % Rule 4 0.8::sid(O) :- ¬leak(OP1), rand(OP2), and(O,OP1,OP2), noIntersect(OP1,OP2). % Rule 5

14 15 16 17

% Datalog queries query(leak(_)). % leak(c2)=0.63, leak(c3)=0.35, ... query(sid(_)). % sid(c3) =0.064

Fig. 2. Side-channel analysis in probabilistic Datalog.

Example Program and Encoding. Figure 3 (left) depicts a code fragment, compute(), which utilizes a secret input k and three random variables r1–r3 to produce a masked output through intermediate values c1–c5. Despite the masking, the implementation contains inherent side-channel risks. To evaluate these, we represent the program logic in a probabilistic Datalog model (Fig 2) that tracks information flow through three relations: leak(var) indicates a potential information leak, rand(var) denotes a variable masked by pure randomness, and sid(var) indicates statistical independence from the secret. The encoding has three parts. First, the input facts (lines 2–6) define variable types and statement semantics, including type annotations such as inKey(k) and instruction semantics such as xor(c1,k,r1), which corresponds to line 1 of the original program in Figure 3 (left). All input facts are prefixed with 1.0::, indicating deterministic program semantics. Second, the inference rules (lines 9–13) propagate these properties. Each rule is assigned a probability based on empirical domain knowledge about data dependencies [36, 54]. For example, Rule 4 assigns a 70% probability that an AND operation on a leaky variable (OP1) and a random variable (OP2) also leaks secret information. Finally, the queries (lines 16–17) identify variables that are either leaking or independent. To produce these results, a solver repeatedly applies these rules to the input facts until reaching a fixed point. Throughout this process, the system constructs a derivation graph to track the provenance of each fact and the computation of associated probabilities. Derivation Graph and Conflicts. Figure 3 (right) shows the derivation graphs for sid(c3) and leak(c5). White nodes denote input facts, while gray and red nodes denote intermediate or output relations.

Conflict Extraction in Probabilistic Datalog Analyses 1 2 3 4 5 6 7 8 9

bool compute(bool k, Rule 5 sid(c3) bool r1, r2, r3) { bool c1, c2 . . . ; ¬leak(c2) rand(r2) and(c3,c2,r2) c1 = k ⊕ r1 ; c2 = k ∧ c1; Rule 4 c3 = c2 ∧ r2; leak(k) rand(c1) and(c2,k,c1) c4 = c1 ∧ c2 ; Rule 1 Rule 3 c5 = c4 ∧ r3; inKey(k) inRand(r1) xor(c1,k,r1) ... }

5 Conflict

leak(c5) Rule 4

noIntersect (c2,r2)

leak(c4)

rand(r3)

and(c5,c4,c3)

Rule 4 leak(c2)

rand(c1)

...

...

and(c4,c2,c1)

Fig. 3. Left: an example program adapted from [58]. Right: its derivation graph, where white nodes are input facts and gray nodes are derived facts. The red highlights show a conflict: one branch requires ¬leak(c2), while the other requires leak(c2), so sid(c3) and leak(c5) cannot hold together. Rule numbers refer to Fig. 2.

These two outputs are logically inconsistent: sid(c3) can be derived only if leak(c2) is false (Rule 5), whereas leak(c5) requires leak(c2) to be true (Rule 4). Probabilistic Datalog, however, uses possible-worlds semantics where uncertain facts like leak(c2) are assigned marginal probabilities instead of binary truth values. Because leak(c2) may be true in some possible worlds and false in others, both sid(c3) and leak(c5) can appear simultaneously in query results. Standard solvers typically report these probabilities independently without signaling logical incompatibility, which can be misleading in security-critical contexts where mutually exclusive results represent fundamentally different program behaviors. Impact and Summary. Without conflict awareness, developers must inspect many spurious alarms, often spending effort on combinations that cannot occur in the same execution, such as sid(c3) and leak(c5) being true together. This problem becomes especially severe in large-scale quantitative analyses, where the output volume makes manual conflict detection impractical. Although probabilistic Datalog is effective for modeling uncertainty [20, 24, 36, 54], it does not explicitly expose internal logical inconsistencies, which can lead to misleading results. Our work addresses this gap with a sound and efficient MUS generator that automatically extracts such conflicts. By exposing these hidden inconsistencies, PPProbe helps developers focus on plausible vulnerabilities and improves the precision and usability of probabilistic program analyses. 3

Preliminaries

We introduce the key concepts used throughout this paper. We first define probabilistic Datalog programs and their grounded solutions, then describe how they are represented using derivation graphs, and finally formulate conflicts as MUSes. 3.1

Probabilistic Datalog Programs

A probabilistic Datalog program consists of a set of rules 𝑅, where each rule is a Horn clause annotated with a probability: 𝑝 :: ℎ(𝑥) ® :− ⊙𝑏 1 (𝑦®1 ), . . . , ⊙𝑏𝑛 (𝑦®𝑛 ), where ℎ(𝑥) ® is the head, each 𝑏𝑖 (𝑦®𝑖 ) is a body predicate, and ⊙ denotes an optional negation operator. The probability 𝑝 ∈ [0, 1] specifies how likely the head holds

6

Chen et al.

when the body is satisfied. A probabilistic Datalog program also assumes stratified negations in order to compute the least fix-point within limited time, meaning that recursive negations in rules are not allowed. When the body of a rule is empty, it becomes an input fact declaration, e.g., 1.0::inRand(r1) in Figure 2. A program also contains one or more queries, which specify the output relations of interest. The solution to a program is a set of grounded output facts, obtained by repeatedly applying rules to input facts until reaching a fixed point over the Herbrand universe. For example, in Figure 3, all leak(OP1) relations are grounded by substituting OP1 with concrete variable names (e.g., c2,c5), shown as gray boxes in the figure. Derivation Graph. The grounded solution of a probabilistic Datalog program can be represented as a derivation graph, which captures how each output fact is derived from input facts. Definition 1 (Derivation Graph). A derivation graph for a grounded probabilistic Datalog solution is a hypergraph 𝐺 = (𝑉 , 𝐸) where: • 𝑉 is the set of nodes, each representing a grounded relation (fact). • 𝐸 is the set of directed hyperedges, where each hyperedge is a tuple (𝑝, ℎ, 𝐵 +, 𝐵 − , 𝑟 ) representing a grounded rule 𝑟 with probability 𝑝, head ℎ, positive body 𝐵 + , and negative body 𝐵 − . Each hyperedge represents a fully grounded rule, where every predicate (e.g., ℎ(𝑥)) ® has concrete terms. The source of a hyperedge is its head ℎ, and the targets are the union of body predicates 𝐵 + ∪ 𝐵 − . 𝐵 + denote the set of non-negated body predicates and 𝐵 − the set of negated body predicates. Example 1. In the derivation graph of Figure 3, the hyperedge for inferring sid(c3) has the head ℎ = sid(c3), 𝐵 + = {rand(r2), and(c3,c2,r2), noIntersect(c2,r2)}, 𝐵 − = {leak(c2)}, 𝑝 = 0.8 and rule 𝑟 is noted as Rule 5. Derivation Set of a Node. For a node 𝑣 ∈ 𝑉 , we define its derivation set as: Derv(𝑣) = {𝑒 | 𝑒 ∈ 𝐸, 𝑒 = (𝑝, 𝑣, 𝐵 +, 𝐵 − , 𝑟 )}, consisting of hyperedges. 3.2

Boolean Encoding of the Grounded Solution

To reason about satisfiability, we encode the derivation graph as Boolean constraints. This enables SAT and UNSAT reasoning over sets of grounded facts. Definition 2 (Mapping Rules to Boolean Variables). Given a derivation graph 𝐺 = (𝑉 , 𝐸), each grounded rule 𝑟 is mapped by 𝑆 to a Boolean variable 𝑏𝑟 that follows a Bernoulli distribution, where 𝑃 (𝑏𝑟 = true) = 𝑝 and 𝑝 is the probability associated with 𝑟 . Definition 3 (Mapping Relations to Boolean Variables). Each grounded relation (node 𝑣 ∈ 𝑉 ) is mapped by Γ to a Boolean variable 𝑏 𝑣 , indicating whether the fact 𝑣 holds.

Conflict Extraction in Probabilistic Datalog Analyses

7

Definition 4 (Boolean Interpretation). Given a derivation graph 𝐺 = (𝑉 , 𝐸), a Boolean interpretation is a tuple 𝑇 (𝐺) = (Γ, 𝑆, Φ) where: Γ = {𝑣 ↦→ 𝑏 𝑣 | 𝑣 ∈ 𝑉 , 𝑏 𝑣 ∈ B}, 𝑆 = {𝑟 ↦→ 𝑏𝑟 | (𝑝, ℎ, 𝐵 +, 𝐵 − , 𝑟 ) ∈ 𝐸, 𝑏𝑟 ∈ B}, n Φ = 𝑐 | 𝑣 ∈ 𝑉 , 𝑐 ≜ Γ [𝑣] = 𝐷 𝑣 ,  o Ü Û Û Γ [𝑏 + ] ∧ ¬Γ [𝑏 − ] . 𝐷𝑣 ≜ 𝑆 [𝑟 ] ∧ (𝑝,𝑣,𝐵 + ,𝐵 − ,𝑟 ) ∈ Derv(𝑣)

𝑏 + ∈𝐵 +

𝑏 − ∈𝐵 −

The Boolean encoding Φ follows the possible-world semantics of probabilistic Datalog. For each grounded probabilistic rule instance 𝑟 , the map 𝑆 introduces a fresh Boolean event variable 𝑆 [𝑟 ] indicating whether that rule instance is enabled in a possible world. Thus, a derived fact 𝑣 holds only if at least one of its grounded derivations is enabled: the corresponding rule event 𝑆 [𝑟 ] must be true, all positive body facts must hold, and all negated body facts must fail. This differs from deterministic Datalog, where a satisfied rule body directly entails the head without an additional rule-event variable. In this way, the rule-event variables give Φ an abstraction of the possible-world structure that does not involve the concrete numeric probability weights. This abstraction is sufficient for conflict extraction. The probability annotation 𝑝 in a rule of the form 𝑝 :: 𝑟 (Section 3.1) is needed only for probabilistic inference: it specifies the Bernoulli weight of the rule-event variable 𝑆 [𝑟 ] when computing marginal query probabilities. Conflict extraction, in contrast, asks a purely Boolean question over Φ: whether some assignment to the rule-event and fact variables makes a set of output facts jointly true. Since the numeric weights affect only how likely a satisfiable world is, not whether one exists, conflict extraction loses no information by operating on the abstraction alone. 3.3

Conflicts and MUS Formulation

We now formalize conflicts among output facts using SAT reasoning over the Boolean interpretation of a probabilistic Datalog derivation graph. Definition 5 (Joint Satisfiability). Given a derivation graph 𝐺 = (𝑉 , 𝐸) and its Boolean interpretation 𝑇 = (Γ, 𝑆, Φ), a set of nodes 𝑉 ′ ⊆ 𝑉 is jointly satisfiable if the constraint Û   Û  Ψ(𝑉 ′ ) = 𝜙 ∧ Γ [𝑣] 𝜙 ∈Φ

𝑣 ∈𝑉 ′

is SAT. Otherwise, 𝑉 ′ is jointly unsatisfiable. Definition 5 checks whether the output facts in 𝑉 ′ can co-occur in at least one possible world of the probabilistic Datalog program. The constraint Φ encodes the logical structure of those possible worlds, including the Boolean event variables introduced for probabilistic rule instances. Hence, joint unsatisfiability captures a genuine semantic conflict: no assignment to the probabilistic rule events can make all facts in

8

Chen et al.

𝑉 ′ true simultaneously. Importantly, this notion depends on the structure of the probabilistic derivations, but not on the concrete numeric probabilities assigned to the rule events. The numeric weights affect how likely a satisfiable set of facts is, but they do not affect whether such a set is logically realizable. Example 2. In the derivation graph of Figure 3, we use 𝑟 5 and 𝑟 4 to denote Rule 5 and Rule 4, respectively. The set Φ includes the following constraints: 𝜙1 :

sid(c3)

= 𝑆 (𝑟 5 ) ∧ ¬leak(c2) ∧ rand(r2) ∧ and(c3, c2, r2), ∧ noIntersect(c2, r2)

𝜙2 :

leak(c5)

= 𝑆 (𝑟 4 ) ∧ leak(c4) ∧ rand(r3) ∧ and(c5, c4, c3),

𝜙3 :

leak(c4)

= 𝑆 (𝑟 4′ ) ∧ leak(c2) ∧ rand(c1) ∧ and(c4, c2, c1).

For 𝑉 ′ = {sid(c3), leak(c5)}, the constraint Ψ(𝑉 ′ ) is encoded as 𝜙 1 ∧ 𝜙 2 ∧ 𝜙 3 ∧ sid(c3) ∧ leak(c5). For brevity, we omit the remaining constraints in Φ. As shown above, Ψ({sid(c3), leak(c5)}) is UNSAT, since both leak(c2)and ¬leak(c2) appear in the conjunction. Hence, {sid(c3), leak(c5)} is jointly UNSAT. Definition 6 (Minimal Unsatisfiable Subset). A set of nodes 𝑉 ′ ⊆ 𝑉 is a Minimal Unsatisfiable Subset (MUS) if: (1) Ψ(𝑉 ′ ) is UNSAT, and (2) for every strict subset 𝑉 ′′ ⊊ 𝑉 ′ , Ψ(𝑉 ′′ ) is SAT. The set {sid(c3), leak(c5)} is also a minimal unsatisfiable subset, since each of its strict subsets, {sid(c3)} and {leak(c5)}, is SAT. An MUS represents the smallest group of grounded facts that cannot all be true simultaneously. Identifying MUSes allows us to pinpoint minimal conflicts within the program’s probabilistic reasoning. Given a derivation graph 𝐺 = (𝑉 , 𝐸), our goal is to enumerate all MUSes 𝑉 ′ ⊆ 𝑉 that satisfy Definition 6, thereby revealing all minimal conflicts in the grounded solution. 4

Overview of PPProbe

We present a high-level overview of PPProbe, a framework for enumerating minimal unsatisfiable subsets (MUSes) in probabilistic Datalog programs (Algorithm 1). Unlike generic MUS enumeration methods, PPProbe exploits the derivation graph to capture recursive and probabilistic dependencies among facts. At a high level, it repeatedly finds an UNSAT candidate set 𝐶 of output facts and shrinks it to a MUS. Given a probabilistic Datalog program P, we first invoke a standard solver (e.g., ProbLog [13]) to obtain the queried output facts O and derivation graph G. PPProbe then encodes G as Boolean constraints Φ (Line 3) and initializes the search space Unexp (Unexplored) as the power set of O. PPProbe is designed to leverage the structural and statistical information in the derivation graph G to both prioritize candidate exploration (⋆1 , Line 7) and aggressively prune the search space (⋆2 , Line 11). This leads to two main contributions.

Conflict Extraction in Probabilistic Datalog Analyses

9

Algorithm 1: Overview of PPProbe Input: Queried output facts O and the derivation graph G Output: All minimal unsatisfiable subsets (MUSes) 1 begin 2 S←∅; 3 Φ ← Encode( G) ; 4 Unexp ← Powersets( O, G) 5 quota ← | O | 6 while Unexp ≠ ∅ do 7 C ← DerivativeSampling(Unexplored, quota, O, G) ; 8

9 10

S ← S ∪ InferMUS( M, Unexp, S)

12

// ⋆2 : Bottom-up inference (Sec 6) quota ← ReduceOrMaintainQuota(quota) // Half or maintain the quota

14 15 16

// ⋆1 : Get unexplored cases (Sec 5)

if CheckSat( C, Φ) = UNSAT then // Check if the combination C is UNSAT (Def 5) M ← Shrink( C) Unexp ← Unexp \ (Supersets( M ) ∪ Subsets( M ) )

11

13

// S: the set of MUSes // Generate the encoding of G (Def 4)

else Unexp ← Unexp \ Subsets( C); quota ← IncreaseQuota(quota) ;

// Double the quota

return S

First, PPProbe identifies negative statistical dependencies in the derivation graph (Section 5) and prioritizes combinations of such nodes during candidate generation. Intuitively, combining negatively dependent derivations is more likely to expose inconsistencies and produce UNSAT candidates. This idea is realized by DerivativeSampling (Line 7). Second, once an MUS 𝑀 is found, InferMUS (Section 6) exploits the recursive structure of Datalog derivations to infer additional UNSAT candidates in a bottom-up manner. By propagating conflicts through the derivation graph, PPProbe guides the search toward promising regions and prunes likely SAT candidates. PPProbe also includes several mechanisms to improve efficiency. Since MUSes are often much smaller than the full query set |O|, PPProbe dynamically adjusts the sampling quota2 based on satisfiability outcomes (Lines 12 and 15). If a sampled candidate C is satisfiable under Φ (Line 8), the quota is increased, and all subsets of C are pruned from Unexp. If a candidate 𝐶 is unsatisfiable, PPProbe shrinks it to a MUS 𝑀 [26]; then, by Definition 6, both subsets and supersets of 𝑀 are pruned from Unexp. Overall, PPProbe tightly integrates MUS enumeration with probabilistic Datalog semantics by exploiting derivation-graph structure and probabilistic dependencies for both candidate generation and pruning. Sections 5 and 6 present these two main ideas.

2 The quota is the number of facts selected in each invocation of DerivativeSampling.

10

Chen et al.

Algorithm 2: DerivativeSampling Input: Search space of unexplored combinations U Input: Derivation graph G = (𝑉 , 𝐸 ), queried output facts O Input: Budget 𝑞 (max #visited nodes) Output: A sampled combination C 2

Visited ← ∅; Roots ← RandSelect( O );

3

G ′ ← NegEdgeOnly(G) ;

1

(𝑉 , 𝐸 ) ← G ′ ; repeat 6 Frontier ← Roots \ Visited; 7 while Frontier ≠ ∅ and |Visited| < 𝑞 do 8 Visited ← Visited ∪ Frontier; 9 Next ← {𝑣 | ∃𝑢 ∈ Frontier.(𝑢 → 𝑣) ∈ 𝐸 ∧ 𝑣 ∉ Visited}; 10 Frontier ← Takemin(𝑞−|Visited|,|Next|) (Next); 4 5

if |Visited| < 𝑞 then 𝑆 ′ ← NegNode(LastRoot(Roots), Visited, G) ;

11 12

if 𝑆 ′ ∉ Visited then Roots ← Roots ∪ {𝑆 ′ };

13 14

until Visited unchanged or |Visited| ≥ 𝑞; Pol ← {𝑟 : True | 𝑟 ∈ Visited} ∪ {𝑟 : False | 𝑟 ∉ Visited}; 17 C ← Solve(U, Pol); 18 return C; 15 16

5

Derivative Sampling: Prioritizing Search

This section presents our first optimization for efficient MUS generation: derivative sampling. The key idea is to exploit structural and statistical information in the derivation graph to guide exploration toward candidates more likely to be UNSAT, thereby accelerating MUS discovery. 5.1

Overview

MUS enumeration is an iterative process of sampling and checking candidate combinations. Its efficiency depends on the quality of sampled sets; while an UNSAT combination contains at least one MUS, a SAT result does not directly advance enumeration. We observe that SAT solving performance degrades as the size of the input formula grows, while MUSes in probabilistic Datalog programs are typically small. This suggests that sampling small combinations with a high likelihood of being UNSAT is essential for efficiency. Guided by this observation, Derivative Sampling (Algorithm 2) exploits the structure of the derivation graph and negative dependencies to achieve three goals: (1) prioritize negation by identifying relations that are structurally likely to conflict (via NegEdgeOnly in Line 3); (2) limit formula size by maintaining a small sampling quota 𝑞 that bounds each candidate; and (3) target exploration by restricting sampling to relations with shared negative (statistical) dependencies (via NegNode in Line 12).

Conflict Extraction in Probabilistic Datalog Analyses

11

As shown in Algorithm 2, the procedure constructs a sampled combination C by strategically traversing the derivation graph G. It begins by initializing the set of visited nodes Visited and selecting an initial root Root from the queried output facts O using RandSelect. To emphasize relations that are more likely to induce conflicts, the algorithm applies NegEdgeOnly (Algorithm 3) to transform G into a pruned graph G ′ . This transformation retains only edges corresponding to negative dependencies. Concretely, for a grounded derivation such as 0.6 :: ℎ : -¬𝑏, 𝑏 1 , the original hyperedge (0.6, ℎ, {𝑏 1 }, {𝑏}, 𝑟 ) in G yields a single negative edge (ℎ → 𝑏) in G ′ . Given the negative-edge-only graph G ′ , the algorithm performs a BFS within a repeat-until loop under a node budget 𝑞. Nodes in the current frontier are added to Visited, and the next frontier is computed by following edges in G ′ . If the frontier becomes empty before reaching 𝑞, the algorithm invokes NegNode (Algorithm 4) to select a new node negatively related to the current search path, increasing the chance of generating an UNSAT candidate. Finally, the algorithm assigns polarities Pol based on membership in Visited. Relations in Visited are more likely to participate in conflicts (MUS), so their polarity is set to true to prioritize them during sampling, while relations with polarity false are excluded. These polarity assignments, together with the unexplored search space U, are passed to the solver to generate an unexplored candidate combination C for satisfiability checking. 5.2

Sampling via Negative Dependencies

In the overview (Algorithm 2), derivative sampling uses two forms of negative dependency—structural and statistical—to guide candidate selection. This section describes the corresponding procedures: NegEdgeOnly and NegNode .

Algorithm 3: NegEdgeOnly Input: G Output: G ′ 1 (𝑉 , 𝐸 ) ← G; ′ + − − 2 𝐸 ← { (ℎ → 𝑏 ) | (_, ℎ, 𝐵 , 𝐵 , _) ∈ 𝐸 ∧ 𝑏 ∈ 𝐵 }; ′ 3 return (𝑉 , 𝐸 );

Algorithm 4: NegNode Input: Root, Visited, G Output: Root′ 𝑆 + ← { 𝑟 | CalDep(𝑟, G, +) ∩ CalDep(Root, G, −) ≠ ∅ }; − 2 𝑆 ← { 𝑟 | CalDep(𝑟, G, −) ∩ CalDep(Root, G, +) ≠ ∅ }; ′ + − 3 Root ← (𝑆 ∪ 𝑆 ) \ Visited; ′ 4 return Root ; 1

12

Chen et al. NegEdgeOnly. The NegEdgeOnly procedure extracts immediate negative dependencies from the deriva-

tion graph G. Consider a hyperedge (_, ℎ, 𝐵 +, 𝐵 − , _) ∈ G, where ℎ is the head of a grounded rule and 𝐵 + and 𝐵 − denote its positive and negative body literals, respectively. In the filtered graph, we retain only the flattened negative edges (ℎ → 𝑏) for each 𝑏 ∈ 𝐵 − . Intuitively, such a negative derivation indicates that the truth of ℎ depends on the falsity of 𝑏, which increases the likelihood of inconsistency when both are selected. As a result, NegEdgeOnly encourages sampling combinations that include both ℎ and 𝑏. Algorithm 5: CalDep Input: 𝑟 , G, ⊙ ∈ {+, − } Output: o 1 o ← ∅; 2 if 𝑟 is an input fact then ( {𝑟 }, if ⊙ = +, ; 3 o← ∅, otherwise 4 5 6 7

else for (_, 𝑟, 𝐵 + , 𝐵 − , _) ∈ G do for 𝑏 ∈ 𝐵 +( do o ∪ CalDep(𝑏, G, +), o← o ∪ CalDep(𝑏, G, −), for 𝑏 ∈ 𝐵 −( do o ∪ CalDep(𝑏, G, −), o← o ∪ CalDep(𝑏, G, +),

8 9

10

if ⊙ = +, ; otherwise

if ⊙ = +, ; otherwise

return o;

NegNode. While NegEdgeOnly captures local, edge-level negation, many conflicts in probabilistic Datalog arise from recursive negative dependencies that span multiple derivation steps. The NegNode procedure addresses this by analyzing negative (statistical) dependencies induced by the full derivation structure. At a high level, two relations can only conflict if they depend on shared input facts in opposite ways. To formalize this intuition, we associate each relation 𝑣 with two dependency sets: • Dep+ (𝑣): input facts supporting 𝑣 being true (positive deps); • Dep− (𝑣): input facts supporting 𝑣 being false (negative deps). From a probabilistic perspective, these sets capture statistical influence: if 𝑢 ∈ Dep+ (𝑣), then Pr(𝑣 | 𝑢) > Pr(𝑣); if 𝑢 ∈ Dep− (𝑣), then Pr(𝑣 | 𝑢) < Pr(𝑣). Algorithm 5 computes Dep⊙ (𝑟 ) for a relation 𝑟 and polarity ⊙ ∈ {+, −} by recursively traversing the derivation graph. Specifically, for a grounded rule with positive body 𝐵 + and negative body 𝐵 − , the dependencies propagate as follows: Ø Ø Dep⊙ (𝑟 ) = Dep⊙ (𝑏) ∪ Dep⊙ (𝑏), 𝑏 ∈𝐵 +

𝑏 ∈𝐵 −

(1)

Conflict Extraction in Probabilistic Datalog Analyses

13

where ⊙ denotes the opposite polarity. To avoid infinite recursion due to cyclic derivations, we iteratively update Dep+ and Dep− until reaching fix-point. Using these dependency sets, we define two relations 𝑣 1 and 𝑣 2 to be statistically negatively dependent if (Dep+ (𝑣 1 ) ∩ Dep− (𝑣 2 ) ≠ ∅) ∨ (Dep+ (𝑣 2 ) ∩ Dep− (𝑣 1 ) ≠ ∅). Theorem 1. If two relations 𝑣 1 and 𝑣 2 are not statistically negatively dependent, then 𝑣 1 ∧ 𝑣 2 is always SAT. Proof. Since 𝑣 1 and 𝑣 2 are not statistically negatively dependent, we have (Dep+ (𝑣 1 ) ∩ Dep− (𝑣 2 ) = ∅) ∧ (Dep+ (𝑣 2 ) ∩ Dep− (𝑣 1 ) = ∅). Thus, no shared input fact appears with opposite polarity in 𝑣 1 and 𝑣 2 . If they do not share input facts, assignments for 𝑣 1 and 𝑣 2 can be combined, so 𝑣 1 ∧ 𝑣 2 is SAT. If they do share input facts, the condition above ensures that every shared fact has the same polarity in both relations, so their satisfying assignments can still be made consistent on the shared inputs. Hence, there exists a joint assignment satisfying both 𝑣 1 and 𝑣 2 , and therefore 𝑣 1 ∧ 𝑣 2 is SAT.

□

Theorem 1 motivates NegNode . Given the current root Root, the sampler prioritizes a new root Root′ that is statistically negatively dependent on Root (Algorithm 4). This connects derivation trees with conflicting sources, guiding the search toward combinations more likely to be UNSAT and form MUSes.

O1

O2

O3

O1

O4 I1

I2

O1

O3

O2

I1

O3

O4

O4

𝒢

O2

I2

I1

𝒢′

I2

𝒢′

Fig. 4. Sampling example showing the application of NegNode, which selects O3 as the next root from the current root O2. The corresponding procedure is shown in Algorithm 2. Dep+(O2) = {I2}

Dep-(O3) = {I2} Dep+(O2)∩Dep-(O3)≠∅

Example 3. Consider the following grounded derivations: O1 :− I1.

O2 :− I1, ¬O4.

O4 :− ¬I2.

O3 :− ¬I2.

The corresponding derivation graph G is shown in Figure 4. From the graph structure, O2 inherits the negative dependency of O4. Concretely, Dep+ (O2) = Dep+ (I1) ∪ Dep− (O4) = Dep+ (I1) ∪ Dep+ (I2) = {I1, I2},

14

Chen et al.

and therefore Dep+ (O2) = {I1, I2}. Similarly, Dep− (O3) = {I2}. Since Dep+ (O2) ∩ Dep− (O3) = {I2},

(2)

O2 and O3 are statistically negatively dependent, and sampling them together is likely to expose a conflict. We illustrate DerivativeSampling (Algorithm 2) on Example 3 in Figure 4, using quota 𝑞 = 3. (1) Initial selection (Line 2). The sampler begins by randomly selecting a queried relation, for example O2. The visited set is initialized as Visited = {O2}. (2) Negation traversal (Line 7). The algorithm performs a BFS over negation edges to identify structurally induced conflicts. As indicated by the red arrow in the figure, O2 depends on ¬O4. Consequently, O4 is added to the frontier and included in the visited set, yielding Visited = {O2, O4}. These relations correspond to the nodes highlighted in the orange box. (3) Conflict-based jump. The BFS frontier becomes empty because O4 has no further negative dependencies, even though the quota is still unmet (|Visited| = 2 < 3). The algorithm therefore jumps to a new relation outside the current derivation subtree, i.e., beyond the orange box. (4) Extension via negative dependency (Line 12). The algorithm invokes NegNode to find a relation that is statistically negatively dependent on the current visited set. Comparing O3 (in the purple box) with O2, we observe a shared dependency on input fact I2 (Eq. 2), indicating a potential conflict. Therefore, O3 is added to Visited, yielding {O2, O4, O3}. (5) Finalization. Once the quota is reached, the sampler assigns positive polarities to relations in Visited. These are passed to the SAT solver as soft constraints to guide generation of an unexplored candidate for satisfiability checking. 5.3

Dynamic Sampling Quota Control

This subsection explains the dynamic quota mechanism used in Algorithm 1 in conjunction with DerivativeSampling (Algorithm 2). Figure 5 illustrates a representative execution trace, showing how the sampling quota (Y-axis) evolves across successive iterations (X-axis) to balance exploration efficiency against formula complexity. In the initial iterations (1–3), the algorithm typically starts with a relatively large quota, which is then reduced exponentially. As long as the sampled combinations remain UNSAT (solid markers), the algorithm invokes ReduceOrMaintainQuota (Line 12) to aggressively shrink the sample size. This strategy aims to identify the smallest combination that still preserves unsatisfiability, thereby reducing the cost of subsequent SAT checks. A key transition occurs at iteration 4, where the solver returns a SAT result (hollow marker). This outcome indicates that the current quota (size 2) is too small to expose a conflict. In response, the algorithm triggers IncreaseQuota (Line 15) to incrementally enlarge the sampling budget. As a result, the sampler stabilizes around a low but sufficient quota, as observed in iterations 5–7, where the quota remains at size 4 while

Conflict Extraction in Probabilistic Datalog Analyses

15

UNSAT SAT

L12

16

L12

L12

8 L12

L12

L12

4 2

L15 L15

1

2

3

4

5

6

7

8

Fig. 5. Evolution of the sampling quota (𝑦-axis) across successive iterations (𝑥-axis). Solid markers denote UNSAT combinations verified by the SAT solver, whereas hollow markers represent SAT combinations.

the solver continues to find UNSAT combinations. By maintaining small candidate sizes whenever possible, the algorithm keeps the induced Boolean formulas compact, which significantly improves SAT-solving performance. 6

Bottom-Up MUS Inference: Search Pruning

To reduce SAT solver calls, we leverage the derivation graph to infer additional MUSes from known conflicts (i.e., previously detected MUSes). Algorithm 6 propagates these conflicts bottom-up through the recursive derivation structure by replacing facts in an existing MUS with their ancestors, a process we call logical replacement. Algorithm 6: InferMUS Input: A known MUS 𝑀, unexplored combinations U, MUS set S Output: Updated MUS set S 1 foreach 𝑣 ∈ 𝑀 do 2 N ← relations exclusively dependent on 𝑣; 3 foreach 𝑛 ∈ N do 4 𝐶 ← (𝑀 \ {𝑣 } ) ∪ {𝑛} ; 5 6 7 8 9 10 11 12

S ← MineMUS(𝐶, U, S); N ′ ← relations with two derivations {𝑑 1 , 𝑑 2 } where 𝑣 ∈ 𝑑 1 ; foreach 𝑛 ′ ∈ N ′ do {𝑑 1 , 𝑑 2 } ← Derivations(𝑛 ′ ); foreach literal 𝑙 in 𝑑 2 do 𝑣 ′ ← Atom(𝑙 ); if IsNegative(𝑙 ) then 𝐶 ← (𝑀 \ {𝑣 } ) ∪ {𝑛 ′ , 𝑣 ′ } ; S ← MineMUS(𝐶, U, S);

13

else

14

Sconflict ← {𝑀𝑎𝑙𝑡 ∈ S | 𝑣 ′ ∈ 𝑀𝑎𝑙𝑡 }; foreach 𝑀𝑎𝑙𝑡 ∈ Sconflict do 𝐶 ← (𝑀 \ {𝑣 } ) ∪ (𝑀𝑎𝑙𝑡 \ {𝑣 ′ } ) ∪ {𝑛 ′ } ;

15 16 17

S ← MineMUS(𝐶, U, S);

18

19

return S;

16

Chen et al.

Algorithm 7: MineMUS Input: A candidate 𝐶, unexplored combinations U, MUS set S Output: Updated MUS set S 1 if IsUnexplored(𝐶 ) then 2 𝑀 ← Shrink(𝐶 ); 3 U ← U \ (Supersets(𝑀 ) ∪ Subsets(𝑀 ) ); 4 S ← S ∪ {𝑀 } ∪ InferMUS(𝑀, U, S); 5

return S;

Logical Replacement. The complexity of logical replacement depends on the number of derivation paths available to that ancestor. An Exclusive Dependency occurs when a relation 𝑛 depends solely on a relation 𝑣 already known to be part of an MUS 𝑀 (lines 3–6). In this scenario, 𝑛 acts as a direct proxy for 𝑣, and the set (𝑀 \ {𝑣 }) ∪ {𝑛} is guaranteed to be UNSAT (line 4). Conversely, if a relation 𝑛 ′ is derived by two derivations {𝑑 1, 𝑑 2 } where 𝑣 ∈ 𝑑 1 , replacing 𝑣 with 𝑛 ′ is insufficient to maintain unsatisfiability because 𝑛 ′ could still be satisfied via the alternative path 𝑑 2 . To maintain the conflict, the algorithm blocks the alternative derivation 𝑑 2 by targeting its literals at line 10. If 𝑑 2 depends on a negative literal ¬𝑣 ′ , the algorithm unions the current set with the atom 𝑣 ′ at line 12. This forces 𝑣 ′ to be true, which directly invalidates the alternative path 𝑑 2 . If 𝑑 2 depends on a Positive Literal 𝑣 ′ , the algorithm locates an external blocking set by searching the existing MUS pool S for a conflict 𝑀𝑎𝑙𝑡 that contains 𝑣 ′ (line 16). By substituting 𝑣 ′ with the remaining members of 𝑀𝑎𝑙𝑡 , the algorithm ensures that 𝑣 ′ cannot hold, thereby successfully blocking the alternative path 𝑑 2 at line 17 to guarantee a new UNSAT result. For example, consider MUSes 𝑀 = {𝑂1, 𝑂2} and 𝑀𝑎𝑙𝑡 = {𝑂3, 𝑂4} with rules 𝑂5 :− 𝑂1 and 𝑂5 :− 𝑂3. Replacing 𝑂1 with 𝑂5 in 𝑀 yields the satisfiable set {𝑂5, 𝑂2} because 𝑂5 remains true via 𝑂3 . By incorporating 𝑀𝑎𝑙𝑡 , the algorithm refines this to the UNSAT set {𝑂5, 𝑂4, 𝑂2} at line 17, where 𝑂4 acts as a blocking agent for the 𝑂3 path. The Mining Procedure. This replacement logic is orchestrated by the MineMUS (Algorithm 7), which serves as the primary engine for conflict discovery. When provided with an UNSAT candidate 𝐶, it first applies Shrink[26]–a standard deletion-based minimization procedure–to yield a minimal MUS 𝑀 satisfying Definition 6. After identifying a new MUS 𝑀, the algorithm prunes the search space U by removing all supersets of 𝑀 (which are non-minimal) and all subsets of 𝑀 (which are guaranteed to be SAT) at line 4. Finally, it invokes InferMUS to expand the conflict through the derivation graph, generating new candidates for mining without additional solver overhead. 7

Evaluation

We implemented our approach in a prototype tool called PPProbe, developed in C++. The tool extends the Soufflé Datalog engine [21] by instrumenting its resolution procedure to extract a complete derivation

Conflict Extraction in Probabilistic Datalog Analyses

(a) Side-channel Analysis (SC)

(b) Semantic Diffing (SD)

17

(c) Data Race Analysis (DR)

(d) Bayes

Fig. 6. Normalized MUS count of PPProbe and its ablated variants relative to the strongest baseline.

graph for the input probabilistic Datalog program. For satisfiability checking, PPProbe integrates with the CVC5 SMT solver [3]. Our experimental evaluation was conducted on a Linux-based system powered by an AMD EPYC 7R13 processor (32 physical cores, 64 logical threads) and 242 GB of RAM, operating within a KVM-based virtualization environment. We assigned a 30-minute time limit (T/O) to each benchmark execution. The evaluation is designed to address the following research questions: • RQ1: How efficient and scalable is our method in generating MUSes compared to state-of-the-art baseline approaches? • RQ2: What is the quality of the MUSes generated by our method, in terms of both the total number of identified conflicts and the resulting coverage of Datalog relations? • RQ3: How helpful are the generated MUSes compared to the baselines in assisting real-world Datalogbased program analysis tasks? 7.1

Applications, Benchmarks, and Baselines

We evaluate PPProbe on 70 benchmarks drawn from four distinct domains, as summarized in Table 1. Table 1. Benchmark Statistics Average Max Median #nodes #edges #nodes #edges #nodes #edges SC [54, 58] 29,798 71,267 166,530 389,545 4,294 14,210 DR [24, 36] 59,829 254,279 119,398 722,116 59,874 210,046 SD [45] 8,251 638,252 50,849 5,884,061 2,819 56,339 Bayes [1] 4,309 55,343 4,461 66,188 4,400 55,823

Side-Channel Analysis. The first domain (labeled SC in Table 1) consists of 18 Datalog-based analyses for detecting power side-channel leaks [54, 55, 58]. We include this domain because side-channel risk

18

Chen et al.

assessment requires estimating the likelihood of information leakage rather than checking a purely Boolean property. Recent work [54] has further introduced a probabilistic Datalog formulation for modeling such likelihoods. In this evaluation, the analyses are applied to implementations of widely used cryptographic primitives, including AES, SHA-3, and MAC-Keccak, with queries of the form key_sensitive to identify potential secret leaks for further investigation. Data Race Analysis. The second domain (labeled DR in Table 1) consists of 7 data-race analyses on real-world concurrent applications such as the Apache FTP server, the ETH web crawler and AVR microcontroller simulator. Prior works [36, 59] developed probabilistic Datalog rules to detect data races in those applications that combine thread-escape, may-happen-in-parallel, and lockset analyses in a flow- and context-sensitive manner. In this setting, the input facts are deterministic, while the Datalog rules are probabilistic, capturing the fraction of cases in which a rule may produce an incorrect conclusion from true hypotheses. The queries are alarms of the form race(p1,p2), indicating that program points p1 and p2 may participate in a data race and require further inspection. Semantic Diffing. The third domain (labeled SD in Table 1) consists of 41 semantic-diffing analyses for identifying synchronization differences between evolving multithreaded programs including the Apache HTTP server, the FreeBSD audit subsystem, and the Linux IIO driver. Each application compares two program versions and looks for synchronization, ordering, or data-flow behavior present in one version but not the other. Following prior work [45], these analyses are formulated as Datalog programs that compute differentiating data-flow edges, namely edges permitted by one program but not the other. In this setting, the input facts are deterministic, while the Datalog rules are probabilistic, capturing the uncertainty introduced by approximate inference. The queries correspond to synchronization differences that may indicate unintended behavioral changes and require further inspection. Bayesian Networks (Bayes). The fourth domain includes 4 large-scale Bayesian networks from the bnlearn repository [38]. We focus on Massive Networks (over 1,000 nodes) to test scalability. We convert these networks into probabilistic Datalog by designating source nodes (those without incoming edges) as input facts and all other nodes as output facts. Benchmark Statistics. Table 1 summarizes key statistics for the four benchmark categories. Here, #nodes and #edges denote the numbers of nodes and hyperedges in the corresponding derivation graphs. For each category, we report the average, maximum, and median values across all benchmarks. These statistics indicate the problem scale indirectly. In our encoding, nodes and hyperedges induce fact and rule variables respectively. And probabilistic inference reduces to weighted model counting (WMC), which is #P-hard and worst-case exponential in the number of Boolean random variables determined by #nodes and #edges. Baselines and Experimental Setup. We compare PPProbe against MARCO [26], ReMUS [9], and TOME [6], which are state-of-the-art domain-agnostic MUS enumeration methods. These baselines are designed for propositional formulas in conjunctive normal form and do not natively support the hierarchical and

Conflict Extraction in Probabilistic Datalog Analyses

19

recursive dependencies in Datalog. For a fair comparison, we integrated them into the MUST framework [8] and extended them with our sound encoding (Sec. 3.3). As a result, all baselines share the same grounding and formula construction phases and can process nested conjunctions and disjunctions in probabilistic Datalog. 7.2

Efficiency and Scalability (RQ1)

To evaluate the efficiency of PPProbe, we measured its runtime on all benchmarks under the timeout limit and compared it against three state-of-the-art baselines: MARCO [26], ReMUS [9], and TOME [6]. We also include three ablation variants of PPProbe to isolate the contributions of its core components: • PPProbe-00: PPProbe without either optimization. • PPProbe-10: PPProbe with derivative sampling only (Sec. 5). • PPProbe-01: PPProbe with bottom-up inference only (Sec. 6). • PPProbe-11: Full PPProbe with both optimizations. Table 2. Runtime Statistics for Completed Benchmarks Average

SC

Median

Maximum

P

M

R

T

P

M

R

T

P

M

R

T

0.4

0.5

0.4

2.4

0.0

0.0

0.0

0.0

1.9

3.0

2.4

17.9

Terminated Instances. Eight side-channel analysis benchmarks completed within the time limit. For these instances, Table 2 reports the runtime (in seconds) of the full PPProbe method (PPProbe-11) and three baseline MUS enumerators: MARCO, ReMUS, and TOME, abbreviated as M, R, and T, respectively. The table summarizes the average, median, and maximum runtime across all eight benchmarks. We report only the full PPProbe-11 configuration, since the four ablation variants exhibited nearly identical performance on these terminated instances. The median runtimes of PPProbe-11 and all three baselines (M, R, and T) round to zero because the values are very small. Overall, PPProbe-11 remains competitive with the baseline MUS enumerators: it achieves the best average and maximum runtime among all methods. Timed-Out Instances. For the remaining benchmarks that did not terminate within the T/O limit, we evaluate efficiency by counting the number of MUSes discovered within the 30-minute budget. Figure 6 reports, for each PPProbe variant and each baseline (MARCO, TOME, and ReMUS), the normalized throughput relative to the best baseline in the corresponding application domain; that is, we divide the number of MUSes found by a given method by the number found by the strongest baseline. Because the strongest baseline differs across domains, the normalization is domain-specific. As shown in Figure 6, TOME is the best baseline for Semantic Diffing, whereas MARCO is the best baseline for the other three domains. More specifically, Figure 6(a) reports the average normalized throughput over the 18 side-channel analysis benchmarks. On average, PPProbe-11 discovers 6.62× more MUSes than MARCO, the strongest baseline in this domain, within the same T/O budget. Its gains over TOME and ReMUS are even larger:

20

Chen et al.

PPProbe-11 finds about 24× more MUSes than TOME and about 18× more than ReMUS. A similar trend also appears in the other domains shown in Figure 6(b)–(d). Ablation. Regarding the ablation variants, both PPProbe-10 and PPProbe-01 substantially outperform the unoptimized PPProbe-00, indicating that each optimization contributes meaningfully to performance on its own. Furthermore, their combination in PPProbe-11 leads to a much larger gain. Summary. Overall, these results show that PPProbe-11 consistently achieves the highest throughput, especially on large search spaces, confirming that derivative sampling and MUS inference are complementary and mutually reinforcing. Table 3. Aggregated reduction statistics (in %). Average Δ%

Query

Median Δ%

Maximum Δ% M

R

T

SC

key_sensitive(var)

69.17

54.94

38.53

51.02

87.96

65.11

18.27

47.92

100.00

100.00

100.00

100.00

DR

ultimateRace(p1,p2) racePairs(p1,p2)

60.77

13.64

0.12

1.37

79.25

1.93

0.00

0.40

99.86

59.91

0.72

6.42

SD

mayHb(s1,s2,p)

13.16

12.19

5.22

8.60

12.98

11.60

2.94

8.90

23.08

23.35

20.44

20.44

7.3

P

M

R

T

P

M

R

T

P

Quality of Generated MUSes (RQ2)

While the efficiency of an MUS generator is often evaluated by throughput, the utility of the generated conflicts also depends on their diagnostic diversity. In probabilistic Datalog analysis, discovering a large number of MUSes is useful only if they uncover conflicts spanning a broader range of Datalog relations or facts across different parts of the program logic. To quantify this aspect, we use relation coverage (#Rel), defined as the number of distinct Datalog relations covered by the MUSes discovered within the T/O. Table 4. Quality of MUSes: Relation Coverage Count Average

SC DR SD Bayes

Median

Maximum

P

M

R

T

P

M

R

T

P

M

R

T

4012 6791 1157 1333

1571 1509 711 1054

247 127 171 143

1011 308 333 537

3923 6942 641 1284

1549 1505 571 1026

219 149 174 153

612 381 307 499

7692 9710 3467 1588

3795 2688 2046 1367

441 174 320 173

2224 453 705 715

Table 4 reports #Rel(𝑋 ) for each method 𝑋 . Here, 𝑋 ranges over four methods: PPProbe, MARCO, ReMUS, and TOME, abbreviated as P, M, R, and T, respectively. Each row corresponds to one application domain (SC, DR, SD, and Bayes), and each column summarizes the aggregated results for one method. For each method and domain, we report the average, median, and maximum values of #Rel across all benchmarks. For example, the entry in the SC row and the M column under Average denotes the average value of #Rel(MARCO) over all side-channel benchmarks.

Conflict Extraction in Probabilistic Datalog Analyses

21

Diagnostic Diversity through Coverage. In program analysis tasks such as SC, DR, and SD, higher relation coverage suggests that the discovered MUSes capture a broader range of code statements, variables, and information-flow paths that contribute to side-channel vulnerabilities (SC), data races (DR), and unintended synchronization changes (SD). As shown in Table 4, on side-channel analysis (SC) benchmarks, PPProbe covers, on average, about 16× more relations than ReMUS (i.e., 4012 vs. 247), 4× more than TOME, and 2.5× more than MARCO. Similar trends can also be seen in other program-analysis domains, including DR and SD. Summary. These results suggest that baseline tools such as ReMUS often revisit similar logical paths, whereas PPProbe, guided by structure-aware optimizations such as bottom-up inference, is better able to explore distinct branches of the derivation graph. As a result, within the same time budget, PPProbe covers a larger portion of the program relations (more diverse and diagnostically useful) and gives developers a more complete view of potential inconsistencies in probabilistic Datalog programs. 7.4

Case Study: Reducing False Alarms (RQ3)

To address RQ3, we evaluate the practical utility of PPProbe and the baselines in three real-world static analysis settings: reducing false positives in side-channel analysis (SC), data race analysis (DR), and semantic diffing (SD) for evolving multithreaded programs. In SC, the key queries are key_sensitive(var), which indicate potential secret leakage through program variable var. In DR, the key queries are ultimateRace(p1,p2) and racePairs(p1,p2), which indicate potential data races between program points p1 and p2. In SD, the key queries are mayHb(s1,s2,p), which denote may-happen-before edges in program p and capture execution orders possible under some thread interleavings. Since these analyses are sound but incomplete, they often produce many spurious reports, increasing manual debugging effort and unnecessary mitigation costs. We therefore study whether the MUSes generated by PPProbe can act as an automated filter by identifying and removing logically inconsistent reasoning paths. Methodology. We reconstruct scenarios in which developers use the MUSes generated by PPProbe and baselines (MARCO, ReMUS and TOME) to complement domain knowledge and prune the diagnostic search space that developers must inspect manually. Each MUS is encoded as a hard constraint, together with a small number of developer-provided observations on non-critical queries. The critical queries 𝑆 (e.g., key_sensitive in SC) are encoded as soft constraints. A MaxSAT solver then computes a largest consistent subset 𝑆 ′ ⊆ 𝑆, and we measure the reduction as Δ% = (|𝑆 | − |𝑆 ′ |)/|𝑆 |. Without MUS constraints, all critical queries would remain potentially consistent and no reduction would occur; the MUSes provide the logical conflicts needed for pruning. Because multiple solutions may satisfy the hard constraints, MaxSAT returns one that preserves the largest number of alarms, so Δ% gives a lower bound on the achievable false-positive reduction. A higher reduction rate allows developers to focus on alarms more likely to represent genuine correctness or security issues, lowering the cost of manual triage, unnecessary fixes, and mitigation. Comparison Results. Table 3 summarizes the aggregated reduction rates (AVG, MED, and MAX) achieved by PPProbe (P), MARCO(M), ReMUS(R) and TOME(T) for each application domain across all benchmarks.

22

Chen et al.

Both SC and DR show substantial opportunities for false-positive reduction, with average reductions of 69.17% and 60.77% achieved by PPProbe, which are both higher than the baselines. Notably, for the KS_transition benchmark in SC [4], MUS-based pruning removes all reported leaks (max: 100%), indicating that all detected alarms are false positives. We manually inspected these cases and confirmed that the removed key_sensitive queries are benign. A similar result appears in the weblech benchmark from DR, where the reduction reaches 99.86%. SD achieves a lower average reduction rate (13.16%) by PPProbe, mainly because its MUSes cover fewer relevant relations. This is consistent with Table 4, which shows that SD attains lower relation coverage than SC and DR. In the 41 benchmarks of SD domain, PPProbe achieves the highest false-alarm reduction rate in 35 benchmarks and MARCO wins the rest 6 benchmarks, which explains the reason why PPProbe has a slightly lower maximum reduction rate than MARCO (23.08% vs. 23.35%) but has a higher average (13.16% vs. 12.19%) and median reduction rate (12.98% vs. 11.60%). Summary. Overall, these results show that the MUSes generated by PPProbe can substantially shrink the diagnostic search space and provide a lower bound on the achievable false-positive reduction, and outperforms the baselines on most of the benchmarks. 7.5

Stability Analysis

To assess the randomness of PPProbe brought by derivative sampling in Algorithm 2, we repeat each benchmark three times with distinct random seeds and compute the relative standard deviation (RSD) of the number of MUSes discovered within the fixed timeout. Shown as Table 5, PPProbe exhibits generally stable perTable 5. RSD of #MUSes. Max

formance across seeds: the median RSD ranges from only 3.37% to 7.51% across domains, while the average RSD re-

Domain

Avg Median

SC

7.59%

7.51% 17.32%

DR

3.66%

3.37% 7.41%

SD

7.64%

5.25% 46.00%

25.24% and 22.03%. It’s caused by a single instance, where

Bayes

6.28%

6.51% 9.93%

different seeds trigger inference cascades of substantially

mains below 8% in all cases. The 46.00% RSD is an isolated outlier, as the next two highest RSDs drop substantially to

different sizes before the timeout. Overall, the low domainlevel median and average RSDs demonstrate that PPProbe’s performance is stable across random seeds. 8

Related Work

Datalog for Program Analysis. Datalog is one of the popular techniques in program analysis such as detecting data race [34, 36, 59], detecting side-channel [55, 56], points-to-analysis [10, 30, 43, 57, 60], program diffing [45] and thread-modular analysis [22, 23]. Wang et al. [56] analyzed power side channels using Datalog, focusing on how key information can leak during register allocation in compilation. However, their approach cannot quantify the likelihood of such leaks, limiting its practicality for real-world scenarios. Zhang et al. [60] and Raghothaman et al. [36] incorporated probability into Datalog to address this limitation.

Conflict Extraction in Probabilistic Datalog Analyses

23

However, their approaches overlook potential conflicts in probabilistic Datalog programs, which can restrict the expressiveness of the analysis and lead to redundant or false alarms. Our approach identifies these conflicts, significantly reducing false positives and allowing developers to focus on genuine vulnerabilities. Probabilistic Datalog. A wide range of probabilistic logic programming languages extend Prolog or Datalog with quantitative reasoning, including PRISM [46], LPADs [53], Blog [31], CP-logic [52], PPDL [18], Datalogp [15], ProbLog [13], and Scallop [25]. Most of these systems reduce probabilistic inference to weighted model counting (WMC) and employ symbolic representations such as BDDs for efficiency. While these languages advance the expressiveness and efficiency of probabilistic inference, they overlook conflicting probabilistic outputs. In contrast, our work introduces the first framework for conflict detection in probabilistic Datalog with minimal unsatisfiable subsets. Minimal Unsatisfiable Subsets (MUSes). MUS enumeration has been studied in many domains, including linear programming [12, 17, 51], propositional satisfiability [14, 29, 32, 35], temporal logic [5], and numerical CSPs [16]. Close to our setting, OCE [42] and RCE [49] extract unsatisfiable cores from declarative specifications but assume reducibility to propositional logic, whereas our domain involves recursive Datalog derivations. Domain-agnostic algorithms instantiate black-box SAT/SMT oracles and fall into two families: (1) hitting-set–based methods such as CAMUS [27, 28], DAA [2], and PDDS [44], which exploit the MUS– MCS duality; and (2) seed-shrink methods such as MARCO [26], TOME [6], ReMUS [9], and UNIMUS [7], which iteratively find and minimize unsatisfiable subsets. Among these, MARCO, TOME, and ReMUS are applicable to probabilistic Datalog in principle but ignore derivation-graph structure, scaling poorly on such encodings as our experiments confirm.

9

Conclusion

In this work, we addressed the critical but overlooked challenge of conflicting outputs in probabilistic Datalog, which can undermine the reliability of quantitative program analysis. We introduced PPProbe, the first framework to soundly and efficiently identify these conflicts by representing them as minimal unsatisfiable subsets (MUSes). PPProbe leverages structural and statistical dependencies within Datalog derivation graphs to prioritize and prune search space by derivative sampling and bottom-up UNSAT inference. Our extensive evaluation on 70 real-world benchmarks demonstrated that PPProbe outperforms state-of-the-art baselines. Applied as a post-analysis filter, the extracted MUSes reduce the diagnostic search space by an average of 69% and 61% on side-channel and data-race benchmarks, respectively, providing a conservative lower bound on false-positive elimination.

10

Data Availability Statement

PPProbe, along with the baselines and benchmarks, is available via the artifact link.

24

Chen et al.

References [1] Steen Andreassen, {Finn V.} Jensen, {Stig Kjær} Andersen, B. Falck, U. Kjærulff, M. Woldbye, A.R. Sørensen, A. Rosenfalck, and F. Jensen. 1989. MUNIN: an expert EMG assistant. Pergamon Press, 255–277. [2] James Bailey and Peter J Stuckey. 2005. Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In International Workshop on Practical Aspects of Declarative Languages. Springer, 174–186. doi:10.1007/978-3-540-30557-6_14 [3] Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, et al. 2022. cvc5: A versatile and industrial-strength SMT solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 415–442. doi:10.1007/978-3-030-99524-9_24 [4] Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, and Pierre-Yves Strub. 2015. Verified Proofs of Higher-Order Masking. In Advances in Cryptology – EUROCRYPT 2015, Elisabeth Oswald and Marc Fischlin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 457–485. doi:10.1007/978-3-662-46800-5_18 [5] Jaroslav Bendík. 2017. Consistency checking in requirements analysis. In Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis (Santa Barbara, CA, USA) (ISSTA 2017). Association for Computing Machinery, New York, NY, USA, 408–411. doi:10.1145/3092703.3098239 [6] Jaroslav Bendík, Nikola Benes, Ivana Cerná, and Jirí Barnat. 2016. Tunable Online MUS/MSS Enumeration. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 65), Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 50:1–50:13. doi:10.4230/LIPIcs.FSTTCS.2016.50 [7] Jaroslav Bendík and Ivana Cerná. 2020. Replication-Guided Enumeration of Minimal Unsatisfiable Subsets. In CP (Lecture Notes in Computer Science, Vol. 12333). Springer, 37–54. doi:10.1007/978-3-030-58475-7_3 [8] Jaroslav Bendík and Ivana Černá. 2020. MUST: Minimal Unsatisfiable Subsets Enumeration Tool. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), Armin Biere and David Parker (Eds.). Lecture Notes in Computer Science, Vol. 12078. Springer, 135–152. doi:10.1007/978-3-030-45190-5_8 [9] Jaroslav Bendík, Ivana Černá, and Nikola Beneš. 2018. Recursive Online Enumeration of All Minimal Unsatisfiable Subsets. In Automated Technology for Verification and Analysis (ATVA 2018) (Lecture Notes in Computer Science, Vol. 11138). Springer, Cham, 143–159. doi:10.1007/978-3-030-01090-4_9 [10] Martin Bravenboer and Yannis Smaragdakis. 2009. Strictly declarative specification of sophisticated points-to analyses. In Proceedings of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications. 243–262. doi:10.1145/1639949.1640108 [11] Stefano Ceri, Georg Gottlob, and Letizia Tanca. 1990. Logic Programming and Databases: An Overview. Logic Programming and Databases (1990), 1–15. doi:10.1007/978-3-642-83952-8_1 [12] John W Chinneck and Erik W Dravnieks. 1991. Locating minimal infeasible constraint sets in linear programs. ORSA Journal on Computing 3, 2 (1991), 157–168. doi:10.1287/ijoc.3.2.157 [13] Luc De Raedt, Angelika Kimmig, and Hannu Toivonen. 2007. ProbLog: A probabilistic Prolog and its application in link discovery. In IJCAI 2007, Proceedings of the 20th international joint conference on artificial intelligence. IJCAI-INT JOINT CONF ARTIF INTELL, 2462–2467. [14] Nachum Dershowitz, Ziyad Hanna, and Alexander Nadel. 2006. A scalable algorithm for minimal unsatisfiable core extraction. In International conference on theory and applications of satisfiability testing. Springer, 36–41. doi:10.1007/11814948_5 [15] Norbert Fuhr. 1995. Probabilistic datalog—a logic for powerful retrieval methods. In Proceedings of the 18th annual international ACM SIGIR conference on Research and development in information retrieval. 282–290. doi:10.1145/215206.215372 [16] R. M. Gasca, C. Del Valle, M. T. Gómez-López, and R. Ceballos. 2007. NMUS: Structural Analysis for Improving the Derivation of All MUSes in Overconstrained Numeric CSPs. In Current Topics in Artificial Intelligence: 12th Conference of the Spanish Association for Artificial Intelligence. 160–169. doi:10.1007/978-3-540-75271-4_17

Conflict Extraction in Probabilistic Datalog Analyses

25

[17] John Gleeson and Jennifer Ryan. 1990. Identifying minimally infeasible subsystems of inequalities. ORSA Journal on Computing 2, 1 (1990), 61–63. doi:10.1287/ijoc.2.1.61 [18] Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Peter Lindner. 2022. Generative datalog with continuous distributions. J. ACM 69, 6 (2022), 1–52. doi:10.1145/3559102 [19] Vedad Hadžić, Gaëtan Cassiers, Robert Primas, Stefan Mangard, and Roderick Bloem. 2024. Quantile: Quantifying Information Leakage. IACR Transactions on Cryptographic Hardware and Embedded Systems 2024, 1 (2024), 433–456. doi:10.46586/tches.v2024. i1.433-456 [20] Kihong Heo, Mukund Raghothaman, Xujie Si, and Mayur Naik. 2019. Continuously reasoning about programs using differential bayesian inference. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. 561–575. doi:10.1145/3314221.3314616 [21] Herbert Jordan, Bernhard Scholz, and Pavle Subotić. 2016. Soufflé: On synthesis of program analyzers. In International Conference on Computer Aided Verification. Springer, 422–430. doi:10.1007/978-3-319-41540-6_23 [22] Markus Kusano and Chao Wang. 2016. Flow-sensitive composition of thread-modular abstract interpretation. In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering. 799–809. doi:10.1145/2950290.2950291 [23] Markus Kusano and Chao Wang. 2017. Thread-modular static analysis for relaxed memory models. In Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering. 337–348. doi:10.1145/3106237.3106243 [24] Tianchi Li and Xin Zhang. 2025. Combining Formal and Informal Information in Bayesian Program Analysis via Soft Evidences. Proceedings of the ACM on Programming Languages 9, OOPSLA1 (2025), 1774–1801. doi:10.1145/3720508 [25] Ziyang Li, Jiani Huang, and Mayur Naik. 2023. Scallop: A language for neurosymbolic programming. Proceedings of the ACM on Programming Languages 7, PLDI (2023), 1463–1487. doi:10.1145/3591280 [26] Mark H. Liffiton, Alessandro Previti, Ammar Malik, and Joao Marques-Silva. 2016. Fast, flexible MUS enumeration. Constraints 21, 2 (2016), 223–250. doi:10.1007/s10601-015-9183-0 [27] Mark H. Liffiton and Karem A. Sakallah. 2005. On Finding All Minimally Unsatisfiable Subformulas. In Theory and Applications of Satisfiability Testing, F. Bacchus and T. Walsh (Eds.). Lecture Notes in Computer Science, Vol. 3569. Springer-Verlag Berlin Heidelberg, 173–186. doi:10.1007/11499107_13 [28] Mark H. Liffiton and Karem A. Sakallah. 2008. Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints. Journal of Automated Reasoning 40, 1 (2008), 1–33. doi:10.1007/s10817-007-9084-z [29] Inês Lynce and João Silva. 2004. On Computing Minimum Unsatisfiable Cores, In The Seventh International Conference on Theory and Applications of Satisfiability Testing. LNCS. [30] Magnus Madsen, Ming-Ho Yee, and Ondřej Lhoták. 2016. From datalog to flix: A declarative language for fixed points on lattices. ACM SIGPLAN Notices 51, 6 (2016), 194–208. doi:10.1145/2980983.2908096 [31] Brian Milch, Bhaskara Marthi, Stuart Russell, David Sontag, Daniel L Ong, and Andrey Kolobov. 2007. Blog: Probabilistic models with unknown objects. Statistical relational learning (2007), 373. doi:10.7551/mitpress/7432.003.0015 [32] Maher Mneimneh, Inês Lynce, Zaher Andraus, João Marques-Silva, and Karem Sakallah. 2005. A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas. In International Conference on Theory and Applications of Satisfiability Testing. Springer, 467–474. doi:10.1007/11499107_40 [33] Chris Mungall. 2009. Experiences using logic programming in bioinformatics. In International Conference on Logic Programming. Springer, 1–21. doi:10.1007/978-3-642-02846-5_1 [34] Mayur Naik, Alex Aiken, and John Whaley. 2006. Effective static race detection for Java. In Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation. 308–319. doi:10.1145/1133981.1134018 [35] Yoonna Oh, Maher N Mneimneh, Zaher S Andraus, Karem A Sakallah, and Igor L Markov. 2004. AMUSE: a minimally-unsatisfiable subformula extractor. In Proceedings of the 41st annual design automation conference. 518–523. doi:10.1145/996566.996710 [36] Mukund Raghothaman, Sulekha Kulkarni, Kihong Heo, and Mayur Naik. 2018. User-Guided Program Reasoning Using Bayesian Inference. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (Philadelphia,

26

Chen et al. PA, USA) (PLDI 2018). Association for Computing Machinery, New York, NY, USA, 722–735. doi:10.1145/3192366.3192417

[37] Seemanta Saha, Surendra Ghentiyala, Shihua Lu, Lucas Bang, and Tevfik Bultan. 2023. Obtaining information leakage bounds via approximate model counting. Proceedings of the ACM on Programming Languages 7, PLDI (2023), 1488–1509. doi:10.1145/3591281 [38] Marco Scutari. 2010. Learning Bayesian networks with the bnlearn R package. Journal of statistical software 35 (2010), 1–22. doi:10.18637/jss.v035.i03 [39] Jiwon Seo. 2018. Datalog extensions for bioinformatic data analysis. In 2018 40th Annual International Conference of the IEEE Engineering in Medicine and Biology Society (EMBC). IEEE, 1303–1306. doi:10.1109/EMBC.2018.8512571 [40] Jiwon Seo, Stephen Guo, and Monica S Lam. 2015. SociaLite: An efficient graph query language based on datalog. IEEE Transactions on Knowledge and Data Engineering 27, 7 (2015), 1824–1837. doi:10.1109/TKDE.2015.2405562 [41] Jiwon Seo, Jongsoo Park, Jaeho Shin, and Monica S Lam. 2013. Distributed socialite: A datalog-based language for large-scale graph analysis. Proceedings of the VLDB Endowment 6, 14 (2013), 1906–1917. doi:10.14778/2556549.2556572 [42] Ilya Shlyakhter, Robert Seater, Daniel Jackson, Manu Sridharan, and Mana Taghdiri. 2003. Debugging overconstrained declarative models using unsatisfiable cores. In 18th IEEE International Conference on Automated Software Engineering, 2003. Proceedings. IEEE, 94–105. doi:10.1109/ASE.2003.1240298 [43] Yannis Smaragdakis, George Kastrinis, and George Balatsouras. 2014. Introspective analysis: context-sensitivity, across the board. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. 485–495. doi:10.1145/2594291.2594320 [44] Roni Stern, Meir Kalech, Alexander Feldman, and Gregory Provan. 2012. Exploring the duality in conflict-directed model-based diagnosis. In Proceedings of the AAAI Conference on Artificial Intelligence, Vol. 26. 828–834. doi:10.1609/aaai.v26i1.8231 [45] Chungha Sung, Shuvendu K. Lahiri, Constantin Enea, and Chao Wang. 2018. Datalog-Based Scalable Semantic Diffing of Concurrent Programs. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering (Montpellier, France) (ASE 2018). ACM, New York, NY, USA, 656–666. doi:10.1145/3238147.3238211 [46] SATO Taisuke. 1995. A statistical learning method for logic programs with distribution semantics. In Proceedings of ICLP. 715–729. doi:10.7551/mitpress/4298.003.0069 [47] K Tuncay Tekle, Michael Gorbovitski, and Yanhong A Liu. 2010. Graph queries through datalog optimizations. In Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming. 25–34. doi:10.1145/ 1836089.1836093 [48] Saeid Tizpaz-Niari, Pavol Černỳ, and Ashutosh Trivedi. 2019. Quantitative mitigation of timing side channels. In International conference on computer aided verification. Springer, 140–160. doi:10.1007/978-3-030-25540-4_8 [49] Emina Torlak, Felix Sheng-Ho Chang, and Daniel Jackson. 2008. Finding minimal unsatisfiable cores of declarative specifications. In International symposium on formal methods. Springer, 326–341. doi:10.1007/978-3-540-68237-0_23 [50] Jeffrey D. Ullman. 1988. Principles of Database and Knowledge-Base Systems, Volume I. Principles of Computer Science Series, Vol. 14. Computer Science Press. https://dblp.org/rec/books/cs/Ullman88 [51] JNM Van Loon. 1981. Irreducibly inconsistent systems of linear inequalities. European Journal of Operational Research 8, 3 (1981), 283–288. doi:10.1016/0377-2217(81)90177-6 [52] Joost Vennekens, Marc Denecker, and Maurice Bruynooghe. 2009. CP-logic: A language of causal probabilistic events and its relation to logic programming. Theory and practice of logic programming 9, 3 (2009), 245–308. doi:10.1017/S1471068409003767 [53] Joost Vennekens, Sofie Verbaeten, and Maurice Bruynooghe. 2004. Logic programs with annotated disjunctions. In International Conference on Logic Programming. Springer, 431–445. doi:10.1007/978-3-540-27775-0_30 [54] Jingbo Wang, Shashin Halalingaiah, Weiyi Chen, Chao Wang, and Işil Dillig. 2025. Probabilistic Inference for Datalog with Correlated Inputs. Proceedings of the ACM on Programming Languages OOPSLA2 (2025). doi:10.1145/3763058 [55] Jingbo Wang, Chungha Sung, Mukund Raghothaman, and Chao Wang. 2021. Data-driven synthesis of provably sound side channel analyses. In 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE). IEEE, 810–822. doi:10.1109/ ICSE43902.2021.00079

Conflict Extraction in Probabilistic Datalog Analyses

27

[56] Jingbo Wang, Chungha Sung, and Chao Wang. 2019. Mitigating power side channels during compilation. In Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 590–601. doi:10.1145/3338906.3338913 [57] John Whaley, Dzintars Avots, Michael Carbin, and Monica S Lam. 2005. Using Datalog with binary decision diagrams for program analysis. In Asian Symposium on Programming Languages and Systems. Springer, 97–118. doi:10.1007/11575467_8 [58] Jun Zhang, Pengfei Gao, Fu Song, and Chao Wang. 2018. SCInfer: Refinement-based verification of software countermeasures against side-channel attacks. In International Conference on Computer Aided Verification. Springer, 157–177. doi:10.1007/978-3319-96142-2_12 [59] Xin Zhang, Radu Grigore, Xujie Si, and Mayur Naik. 2017. Effective interactive resolution of static analysis alarms. Proceedings of the ACM on Programming Languages 1, OOPSLA (2017), 1–30. doi:10.1145/3133881 [60] Xin Zhang, Ravi Mangal, Radu Grigore, Mayur Naik, and Hongseok Yang. 2014. On abstraction refinement for program analyses in Datalog. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. 239–248. doi:10.1145/2594291.2594327

Related documents

• A PWK-style Argumentation Framework and Expansion#76585
• Can People Detect an AI Mediator? A Pilot Turing-Test Study of AI-Assisted Conflict Resolution#486107
• Can People Detect an AI Mediator? A Pilot Turing-Test Study of AI-Assisted Conflict Resolution#481165
• Layered change log model: bridging between ontology change representation and pattern mining.#391432
• Strong aggregation of the Markov chains associated with matching models based on the automorphism group of their compatibility graphs#1122853