Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
Authors: Jinzhao Li
Nan Jiang
Yexiang Xue
Venue: ICML 2025 poster (2025)
Keywords: Satisfiabilty
Satisfiability Modulo Counting
Uncertainty in AI
Statistical AI
Probability Circuits
Primary area: general_machine_learning
TL;DR: We propose an exact solver for Satisfiability Modulo Counting with probabilistic circuits

Abstract: Satisfiability Modulo Counting (SMC) is a recently proposed general language to reason about problems integrating statistical and symbolic Artificial Intelligence. 
An SMC problem is an extended SAT problem in which the truth values of a few Boolean variables are determined by probabilistic inference. Approximate solvers may return solutions that violate constraints. Directly integrating available SAT solvers and probabilistic inference solvers gives exact solutions but results in slow performance because of many back-and-forth invocations of both solvers. 
We propose KOCO-SMC, an integrated exact SMC solver that efficiently tracks lower and upper bounds in the probabilistic inference process. It enhances computational efficiency by enabling early estimation of probabilistic inference using only partial variable assignments, whereas existing methods require full variable assignments. 
In the experiment, we compare KOCO-SMC with currently available approximate and exact SMC solvers on large-scale datasets and real-world applications. The proposed KOCO-SMC finds exact solutions with much less time.

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
Jinzhao Li Nan Jiang "1
Yexiang Xue
Abstract
100
ROCIMME (war)
Linginng ADDMC
Weong
Cornec
Satisfiability Modulo Counting (SMC) is re- cently proposed general language to reason about problems integrating statistical and symbolic Ar- tificial Intelligence. An SMC problem is an ex- tended SAT problem which the truth values of few Boolean variables are determined by prob- abilistic inference. Approximate solvers may re- turn solutions that violate constraints. Directly in- tegrating available SAT solvers and probabilistic inference solvers gives exact solutions but results in slow performance because of many back-and- forth invocations of both solvers. We propose Koco-SMC, an integrated exact SMC solver that efficiently tracks lower and upper bounds in the probabilistic inference process. It enhances computational efficiency by enabling early estima- tion of probabilistic inference using only partial variable assignments, whereas existing methods require full variable assignments. In the exper- iment, we compare Koco-SMP SMC with currently available approximate and exact SMC solvers on large-scale datasets and real-world applications. The proposed KoCO-SMC finds exact solutions with much less time.
Solved Instances (%%
80
100
Logsing-Hars
Ins Instances (%%
60
Lingiing SID
Lingrlng-D4 U4
75
40
50
20
0-
10
-10 10 10 102 10 10
ROCO.SMC
XOR SMC
Cabbb BP-SAA
SAA
Time Limit (second)
Figure 1. (Left) Compared to exact solvers, our KoCo-SMC solves 45% SMC problems within a 10-second time limit, whereas baselines require up to 3 hours for a similar rate of comple- tion. (Right) Compared with approximate methods, Koco-SMC finds exact solutions for most cases (lower segment), whereas the approximate solvers may handle some hard instances (upper seg- ment) but often yield lower-quality results.
Satisfiability Modulo Counting (SMC) is a recently pro- posed general language to reason about problems integrat- ing statistical and symbolic AI (Fredrikson & Jha, 2014; Li et al., 2024). SMC problem is an extended SAT problem in which the truth values of certain Boolean variables are determined through probabilistic inference, which assesses whether the marginal probability meets the given require- ments. Solving SMC problems poses great challenges since they are NP"P -complete (Park & Darwiche, 2004).
1. Introduction
Symbolic and statistical Artificial Intelligence (AI) foundations with distinct strengths and limitations. Sym- bolic AI, exemplified by SATisfiability (SAT) and constraint programming, excels in constraint satisfaction but cannot handle probability distributions. Statistical AI captures prob- abilistic uncertainty but does not guarantee satisfying sym- bolic constraints. Integrating symbolic and statistical AI remains an open field and has gained much research atten- tion (d' Avila Garcez et al., 2015; Li et al., 2023; Dennis et al., 2023; Sheth & Roy, 2024).
Taking robust supply chain design as an example (Figure 2). manager must choose a route on the road map to ensure sufficient materials for production, while accounting for stochastic events such natural disasters. This problem ne- cessitates both symbolic reasoning to find a satisfiable route and statistical inference to ensure the selected roads are ro- bust to stochastic natural disasters. The SMC formulation is further detailed in Section 3.1. Slightly modified problems can be found in many real-world applications, including vehicle routing (Toth & Vigo, 2002), internet resilience (Is- raeli & Wood, 2002), social influence maximization (Kempe et al., 2005), energy security (Almeida et al., 2019), etc.
Equaa contribution 'Department of Computer Science, Pur- due University, IN, USA. Correspondence to: Jinzhao Li <li4255@purdue.co
Several approximate SMC solvers have been pro- posed (Kleywegt et al., 2002; Li et al., 2024). Among them, Sample Average Approximation (SAA)-based meth- ods (Kleywegt et al., 2002) are the most widely adopted,
Proceedings of the st International Conference Machine Learning. Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
Ensure valid route
Transit center
For Route 1:
b1 = r1
A T2
0.5
0.5
For Route For only one route:
b2 I3
b1 S bg
Demander
Supplier
Ensure sufficient connectivity
0.2
0.8
0.2
Q,8
223
For Route P(b accessible) 2
Route
For Route 2: P(b accessible) 2
Transit center
Route
(a) Pick Route Route 2?
(b) SMC Formulation
(c) Probabilistic circuit for stochastic events
Figure Formulation of the robust supply chain problem into an SMC problem. (a) A road map containing locations and the road between them. The connectivity of each road is denoted by random variable zi, where 2; True indicates the corresponding road is selected. (b) Model the supply routine planning as an SMC problem. (c) The probability of every connectivity situation represented as the Probabilistic Circuit. Each z; node denotes Icaf node that encodes a Bernoulli distribution. The symbols @ and @ represent the sumn and product nodes, respectively. The values next to the edges are weights for the sum nodes.
estimating marginal probabilities using sample means. An- other approach, XOR-SMC (Li et al., 2024) provides a constant-factor approximation guarantee by leveraging XOR-sampling to estimate marginals. Nevertheless, even the solutions found by XOR-SMC may violate fraction of constraints because of the approximate bound. Overall, ap- proximate solvers may be insufficient for certain scenarios where complete constraint satisfaction is essential.
benchmark held between 2010 and 2022. Figure 1 shows the comparison with state-of-the-are solvers. Compared with ex- act solvers, Koco-SMC scales the best. Our Koco-SMC solves 45% of instances within 10 seconds, whereas baseline methods require 3 hours. Given 3-hour runtime, our ap- proach solve 85% of instances. Compared with approx- imate solvers under 10-minute time limit, Koco SMC reliably delivers exact solutions for most cases, whereas approximate solvers solve some problems (including few hard ones that KoCo-SMC cannot) but may return results that do not fully satisfy constraints or cannot be verified.
In the absence of existing exact SMC solvers, an intuitive method to solve SMC problems exactly requires integrating SAT solvers and probabilistic inference solvers. Specifically, the SAT solver first gives a feasible variable assignment for the Satisfiability part, which is then evaluated by prob- abilistic inference solver. This setup leads to excessive back-and-forth communication between the two solvers. A motivating example is in Section 3. For unsatisfiable in- stances, in particular, such exact solvers may exhaustively enumerate all possible assignments before concluding unsat- isfiability, resulting significant computational overhead.
To summarize, our main contributions are:
1. We propose KoCO-SMC, an efficient exact solver for SMC problems, integrating probabilistic circuits with ULW algorithm for effective conflict detection.
2. Experiments on large-scale datasets illustrate Koco- SMC's superior performance compared to state-of-the-an approximate and exact baselines solution quality or time efficiency.
We introduce Koco-SMi SMC, exact and efficient SMC solver, mitigating the extreme slowness typically encoun- tered in unsatisfiable SMC problems. Koco-SMo saves time by detecting the conflict early with partial variable assignments. The proposed Upper Lower Watch (ULW) al- gorithm tracks the upper and lower bounds of probabilistic inference when new variables are assigned. When these bounds violate the satisfaction condition-for example, if the upper bound of the probability falls below the required threshold-ate the conflict is recorded as a learned clause. This clause is then used to prune the search space, preventing redundant exploration in subsequent iterations.
3. In the case study, we also demonstrate the process of formulating real-world problems into SMC problems, and highlight the strong capability of our solver in addressing these problems
2. Preliminaries
Satisfiability Modulo Counting (SMC) provides general language to reason about problems integrating symbolic and statistical constraints (Fredrikson & Jha, 2014; Li et al., 2024). Specifically, the symbolic constraint is character-
In our experiments, we evaluate all existing approximate and exact solvers by creating large-scale dataset contain- ing 1,350 SMC problems-bart based the UAI Competition
Code implementation is available com/ 101111 6/koco--eeee smc
2

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
ized by Boolean formula o, and the statistical constraint is captured by constraints involving marginal probability Eg
The root node of PCs encodes the full joint distribution over all variables.
When equipped with certain structural properties, PC en- ables efficient inference tasks-including computing par- tition functions, marginal probabilities, and MAP esti- mates-that scale polynomially with the graph size (Dar- wiche & Marquis, 2002; Choi et al., 2022).
Let lowercase letters be random variables (i.e., z, V, and b) and let bold symbols (i.e., y, z and b) denote vectors of Boolean variables, e.g., X = (II,...,,NN) All variables take binary values in {False, True).
Given formula e for Boolean constraints and two sets of weighted functions, ررزرزك and {g+] representing discrete probability distributions, the SMC problem is to de- termine if the following formula is satisfiable over Boolean variables x and b:
3. Methodology
3.1. Motivation
We use robust supply chain design as a motivating example to illustrate the limitations of intuitive exact SMC solvers, which we construct as baselines in the absence of existing exact solvers. In Figure 2(a), the task is to deliver suffi- cient materials from suppliers to demanders on a road map. Various random events, such as natural disasters and car accidents, may affect road connectivity. The goal is to pick route with a sufficient road connection probability.
o(x, b), where bj + E,, or b, + E,, y, ((x,),)) En. Ih (x, 2s.)
y, f)(x,85) 2 Dj
(1)
for j = M M
Each function fj (or gk) is unnormalized discrete prob- ability function over Boolean variables x and yj (respec- tively, x and z,.). The summation En and Σ Ik compute the marginal probabilities, where y, and n are latent vari- ables and will be marginalized out. Thus, only x and b are decision variables.
Let x; denote the i-th road segment on the map, for = 1....,4. In the Boolean formula Φ, the assign- ment x; = True indicates that road segment I; is se- lected. The uncertainty due to random events is mod- eled by joint probability distribution over all road seg- ments, P(11, 22, F3, .I). Figure 2(c) uses probabilistic circuit to represent P( I3, T3, x4). We represent the route selection using Boolean variables by and b2, where b1 = True corresponds to choosing route 1, which requires #1 = T2 = True The probability that route 1 is fully connected that is, all required segments are accessible is given by the marginal probability:
Each by is referred as a Probabilistic Predicate, which is evaluated true if and only if the inequality over the marginalized probability is satisfied. Each probabilistic con- straint is in the form of either (1) the marginal probability surpassing a given threshold gj. or (2) one marginal proba- bility being greater than another. Note that the biconditional "<>" can be relaxed to "=" or "<", and the "z" inequality can be generalized to "=,>" >", or to the reversed direction.
In this paper, we focus on the form given in the first line of equation (I).
P(b is assessible) =
Σ 53..44
P(a = 32 = True,T3, T.).
Probabilistic Circuits (PCs) are broad class of probabilis- tic models that support a wide range of exact and efficient inference tasks (Darwiche, 2002; 1999; Poon & Domingos, 2011; Rahman et al., 2014; Kisa et al., 2014; Dechter & Mateescu, 2007; Vergari et al., 2020; Peharz et al., 2020). Formally, a PC is computational graph that encodes probability distribution P(x) over a set of random variables x. The graph consists of three types of nodes: leaf nodes, product nodes, and sum nodes. Each node represents a distribution over a subset of the variables.
Let q [0, 1] denote the minimum required probability for reliable connectivity along the selected route. The goal is to select either route 1 (b, = True) or route 2 (b2 = True) such that the corresponding route's connectivity probability exceeds q. This can be summarized as the SMC problem:
Φ(x, b)
(b1 + b2) A (b1 11 A22
(b2 + 23 A AxA..
(a)
(6)
(0)
where
b
P 12,,,2,3333 23, x1) 9
23.24
Figure 2(c) illustrates an example PC over four variables. A leaf node u encodes a tractable univariate distribution Pa(x:) over single variable I;, such as Gaussian or Bernoulli distribution. A product node defines factor- ized distribution (x) = II P. (x), where ch(u) denotes the children of node u. A sum node u represents a mixture distribution (x(x)= = Eu (x), where We are normalization weights associated with each child v.
(d)
b2
Σ 21.22
P 22, 23) 2 q.
where + is the logical "exclusive or" operator. In part (a), the constraint ensures that only one route is selected. part
3

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
(b), the constraint indicates that: if route 1 is selected, both Ti and 22 must be assigned True. Part (c) applies similar condition for route 2. In part (d), M.g.,, P(x1, 22, 23, æ4) marginalizes out 23 and T1. representing the probability of route I's connectivity condition under random natural disasters. Part (e) is analogous to part (d).
four components: variable assignment, propagation, con- flict clause learning, and backtracking. Each component is systematically adapted to handle probabilistic constraints. A high-level overview is provided in Algorithm 1.
Compilation. Initially, knowledge compilation transforms all probability distributions into PCs with smooth and de- composable properties. This can be achieved by advanced tools (Darwiche & Marquis, 2002; Darwiche, 2004; Lagniez & Marquis, 2017). An example of compiled PCs is provided in Figure 2(c).
Since no general exact SMC solver currently exists, solv- ing SMC problems exactly requires combining tools from different domains. Assume q = 0.5, we have:
1. It first uses SAT solver to solve the Boolean SAT problem 6(x, b) and proposes a solution, e.g,, 21 = Ø2 = 61 = True, 23 = I1 = b2 = False. It implies that only route is selected.
Variable Assignment. Pick one variable among the remaining free variables and assign it with a value in False). Practical heuristics on the choice of vari- able and value to accelerate the whole process can be found in Moskewicz et al. (2001); Eén & Sörensson (2003); Hamadi et al. (2009).
2. Then, it infers the marginal probability Erg.rs P(æ1- =
42 = True, 23, x24) = 0.1 < q, which violates the prob- abilistic constraint. The detailed calculation is shown in Figure 7.
Propagation. Given partial variable assignments, this step simplifies the formula by propagating their logical impli- cations. For Boolean constraints, unit propagation (Zhang & Stickely, 1996) is used to infer additional variable as- signments and detect conflicts. For example, consider the Boolean formula & = (ar -a22) (222 V xz). If we assign 21 False, unit propagation forces 22 False to sat- isfy the clause (.1 V -x2), which subsequently propagates 23 = True to satisfy the clause (I2 V (z). This cascad- ing effect significantly improves the efficiency of solving Boolean constraints.
3. Since variables within the probabilistic constraint cause a conflict, it adds the negated clause -(x1 A Ø2 A by) to formula @ to omit this assignment in the future, and then returns step to find a new assignment.
The process exhibits a sequential dependency between the SAT solver and probabilistic inference, wherein each com- ponent must await the completion of the other. This mutual blocking results in suboptimal computational efficiency, and in the worst-case scenario, the SAT solver is required to exhaustively enumerate all feasible solutions.
However, existing propagation techniques are specifically designed for purely Boolean formulas. Extending this pro- cess to incorporate probabilistic constraints-by extracting useful information from partial assignments and efficiently detecting conflicts-remen
To address this issue, our Koco-SMC immediately detects conflict upon the partial assignment xi True, sav- ing time by avoiding further assignments to the remaining variables. Although remains unassigned, the maximum achievable probability under any completion of the assign- ment is already below the threshold q:
a challenging open problem. To address this, we propose the Upper-Lower Watch (ULW) method (see Section 3.3), a novel propagation technique for probabilistic constraints. ULW leverages tractable proba- bilistic circuits, enabled by advances in modern knowledge compilers, to efficiently track the upper and lower bounds of marginal probabilities.
Σ P(æ1 = True, Ø2, X2, TA) = 0.1 < q.
max
12,220 22g
This should trigger an immediate conflict, rather than de- ferring conflict detection until the SAT solver assigns Z2- As a result, Koco-SMC achieves greater efficiency than existing exact SMC solvers by pruning infeasible branches earlier in the search process.
Conflicts Clause Learning. A conftict occurs when the current partial assignment violates either a Boolean con- straint or a probabilistic constraint, indicating that the cur- rent branch of the search cannot lead to satisfying solution. In such cases, learned clause is derived and added to the Boolean formula to prevent the solver from revisiting the same conflicting assignment in the future. This mechanism enables Koco-SMC to effectively prune the search space and significantly accelerate the solving process.
3.2. Main Pipeline of KoCo-SMC
This section outlines the detailed procedure of the proposed Koco-SMC for solving SMC problems. As SMC prob- lems extend standard SAT by incorporating probabilistic constraints, EOCO-SMC builds upon and extends the clas- sical Conflict-Drivee Clause Learning framework (Silva & Sakallah, 1996; Bén & Sörensson, 2003), which comprises
When a conflict detected within a Boolean clause, there are existing techniques to add learned clause to the orig- inal Boolean formula, preventing the same conflict from occurring in the future (Hamadi et al., 2009).
4

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
When conflict arises from probabilistic constraint, Koco-SMC generates learned Boolean clause that cap- tures the root cause of the violation. This clause is con- structed by negating the current partial assignment respon- sible for making the constraint unsatisfiable. For exam- ple, consider the probabilistic constraint Exy.,, P(r1 = True, æ2, T3, I14) < q. which is unsatisfiable under the current assignment æ1 True. Koco-SMC derives the learned clause - This clause is then added to the Boolean formula, resulting in an updated constraint Φ^ (-x1,)), which prevents the solver from repeating the same conflict and eliminates the need to re-evaluate the same probabilistic inference in future branches.
where variable æ is assigned val, update UB(U)
LB(u) Pa val).
For a leaf node v over an remaining variable I E Xrans update UB(r) = (a True), Pa False)} and LB(²) = min (r True), (. False))-
For leaf node over y y y (the variable to be marginal- ized), update UB( = LB( 1.
Let ch(v) be the set of child nodes of v. Intermediate nodes, i.e., product nodes and sum nodes, can be updated by:
For a product node p, update UB(p) [uueas()) UB(u), and LB(p) = Iuuec((p) LB()..
This step undoes variable assignments when conflict detected, enabling the solver to backtrack and explore alternative branches of the search space.
Backtracking.
For a sum node s, UB(s) Encon(s) W,, and LB(s) = Eucca(e) W,LB(u), (u). Here, wy is the weight as- sociated with each child node u.
3.3. Upper-Lower Watch for Conflict Detection in Probabilistic Constraints
During initialization, the entire probabilistic circuit is tra- versed once to compute the bounds for every node, As the solving process proceeds, assigning free variable triggers updates only along the path from the affected leaf nodes to the root, ensuring computational efficiency. The correct- ness of the whole execution procedure is guaranteed by the smoothness and decomposability properties of probabilistic circuits. A former justification is provided in Lemma 3.1.
The satisfaction conflict of a probabilistic constraint is determined by the involved marginal probability. By main- taining an interval that bounds this marginal probability and refining it with each new variable assignment, we can detect satisfiability or conflict early when the range significantly deviates from the threshold.
Let Xassigned be the assigned variables, Xron denote the unassigned variables, and y be the marginalized-out latent variables. Determining the range of a marginal probability involves estimating the appropriate interval [LB, UB], such that for all possible values assigned to Xyem:
The bounds at the root node r correspond the bounds of the marginal probability in the probabilistic constraint. These estimated bounds are then used for conflict detection. Basically, if the lower bound LB(r) at the root exceeds the threshold in Equation (I), the constraint is guaranteed to be satisfied. Conversely, if the upper bound UB(r) is less than q. the constraint is unsatisfiable
LB < Σ, P( P(Xassigned, Xren; y) < UB,
where UB (resp. LB) is an estimated "upper bound" (resp. "lower bound") of the probabilistic constraint given current partial assignment Xassigned.
Lemma 3.1. Let probabilistic circuit P(x, y) defined over Boolean variables and y. If probabilistic circuit sat- isfies the smooth and decomposable property, our ULW guarantees that Equation 2 holds. The equality is attained for both LB and UB when all variables are assigned.
The proposed Upper-Lower Watch (ULW) algorithm mon- itors both values to track constraint violations. We show that computing sufficiently tight bounds can be reduced to traversal of these circuits.
Sketch of Proof. The result follows from applying the prop- erties of smooth and decomposable probabilistic circuits to the marginal probability inference problem. For a detailed proof, please refer to Appendix B.
Specifically, each node e in the probabilistic circuit repre- sents a distribution P. over variables covered by its children. Our ULW algorithm associates each node with an upper bound UB(u) and lower bound LB(u) for the marginal probability of P. under the current assignment Xassigned- Therefore, the UB(r) and LB(r) at the root node r are the upper and lower bounds of the whole probability.
4. Related Works
Satisfiability Problems. Satisfiability (SAT) determines whether there exists an assignment of truth values to Boolean variables that makes the entire logical formula true. Numerous SAT solvers show great performance in var- ious applications (Moskewicz et al., 2001: Silva & Sakallah, 1999; Eén & Sörensson, 2003; Hamadi et al., 2009).
To initialize or update the bounds, we traverse the proba- bilistic circuits in bottom-up manner. The update rule for the leaf nodes is:
For a leaf node e over an assigned variable x E Xassigned,
5

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
Algorithm 1 Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits.
Input: Boolean formula Φb MM weighted functions {11}}= and thresholds {g) ( Boolean variables x = (x) (x1.... . .NN
and = "bi....,6M) bxr).
Output: Satisfiability, variable assignment.
1: Compile M weighted functions {f1)ا4 into probabilistic circuits {C
Compilation
2: loop
3: Assign free variable to value in (True, False];
Variable assignment
4: Perform unit propagation on Φ.
5: for each probabilistic constraint C do
6: Update bounds for probabilistic constraint C,.
P ULW algorithm
7: Detect conflicts by comparing bounds with threshold qy-
8:
if no conflict is detected then
9:
if all variables are assigned then return SAT, variable assignments.
10:
11:
else
Propose learned clause ot and update Boolean formula Φ + & A... if no variable has been assigned then return UNSAT, no assignment. else
Clause learning
13:
14:
15:
16:
Undo assignments.
> Backtracking
Conflict-Driven Clause Learning (CDCL) (Silva & Sakallah, 1996) is a modern SAT-solving framework that has been widely applied. The process begins by making decisions to assign values to variables and propagating the consequences of these assignments. If conflict is encountered, i.e., clause is unsatisfied, the solver performs conflict analysis to learn a new clause that prevents the same conflict in the future. The solver then backtracks to an earlier decision point, and the process continues. Through clause learning and backtracking, CDCL improves efficiency and increases the chances of finding solution or proving unsatisfiability. Our Koco-SM CMC extends every component in the CDCL framework to handle probabilistic constraints.
et al. (2015); Choi et al. (2022) provide exact bounds by solving marginal MAP problems, yet they are more time- consuming than our method.
Probabilistic Circuit with specific structural properties, i.e., decomposability (Darwiche, 2001a; 1999), smoothness (Darwiche, 2001b), and determinism (Darwiche & Marquis, 2002), enable efficient probability inferences, scaling poly- nomially with circuit size. For example, partition functions and marginal probabilities are computed efficiently due to decomposability and smoothness, MAP requires determin- ism for maximization, and Marginal MAP further requires Q Q-determinism (Choi et al., 2022).
The process of transforming a probability distribution into a probabilistic circuit with a specific structure is referred to as knowledge compilation (Darwiche, 1999; 2001b;a; Dar- wiche & Marquis, 2002). Several knowledge compilers, such ACE (Darwiche & Marquis, 2002), C2D (Darwiche, 2004), and D4 (Lagniez & Marquis, 2017), have been de- veloped to convert discrete distributions into tractable PCs for various probabilistic inference tasks.
Probabilistic Inference and Model Counting, Probabilis- tic inference encompasses various tasks, such as calculating conditional probability, marginal probability, maximum posteriori probability (MAP), and marginal MAP (Cheng al., 2012). Fach of them is essential in fields like machine learning, data analysis, and decision-making processes. Model counting calculates the number of satisfying assign- ments for a given logical formula, and is closely related to probabilistic inference (Gomes et al., 2006; Achlioptas & Theodoropoulos, 2017). In discrete probabilistic models, computing probabilities can be translated to model count- ing (Chavira & Darwiche, 2008).
Specialized Satisfiability Modulo Counting. Stochas- tic Satisfiability (SSAT) (Papadimitriou, 1985) can encode SMC problems with Boolean constraint and one single probabilistic constraint by integrating Boolean SAT with probabilistic quantifiers. Advances in SSAT solvers (Lee et al., 2017; 2018; Fan & Jiang, 2023; Cheng et al., 2024) have improved their efficiency, but these solvers remain limited to problems with a single probabilistic constraint.
Our KoCo-SMC efficiently tracks upper and lower bounds for probabilistic constraints with partial variable assign- ments. In literature, Dubray et al. (2024); Ge & Biere (2024) compute approximate bounds for probabilistic constraints based on the DPLL algorithm, Marinescu al. (2014); Ping
Stochastic Constraint Optimization Problems can model
6

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
100
Empirical Rurning Time (soc)
10
KOLDASIC loung
Langcing L'AE
ICC COCCMMCCCR (oun)
UigelingAAA
CadeakkAAn
MIRBAL-UAII
10
Lingeling-D Th
Langeling HEBS
Solved Instances (%%
80
Lingeling HEeS
Lingeing
Cadeal-ALDUMC
Cediadl D4
MIRBAT
MEnEAF-ARCMCC
Lingeing-AttIM
CadeollggT
10a
LingsingeSID
60
Lingeling SETD
10
40
100
20
10-1
6.09 6.44 7.18 7.58 8.01 8.46 8.93
10a 10
10
10a
10a
10
10"
10
10'
10a
10
10*
Normalized Threshold Value
Time Limit (second)
Figure 3. (Left) The running time (horizontal axis) of different solvers on a selected SMC instance with varying thresholds (vertical axis). Our methad is slower hefore the critical point due the overhead of compilation time, but becomes much faster than the haselines beyond it due to early conflict detection, Additional results are in appendix Figures 13-15. (Right) The percentage of instances from the entire dataset solved within the time limit. Compared exact solvers, Koco-S solves 80% of SMC problems in 20 minutes, whereas baselines solve at most 40% of instances in a 3-hour time limit.
SMC problems by incorporating stochastic constraints. Ex- isting approaches solve them using techniques from Mixed- Integer Linear Programming or Constraint Programming (Latour et al., 2019; 2017).
geling SAT solver (Heule et al., 2019) to enumerate solu- tions and estimate Ey f(xx y) using sample means, which enables approximate inference of marginal probabilities. We Gibbs Sampler (Shapiro, 2003) (Gibbs-SAA and Be- lief Propagation (BP-SAA) (Ding & Xue, 2020) to draw samples. We also include XOR-SMC (Li et al., 2024), an approximated solver specifically for SMC problems.
5. Experiments
In the experiments, Figure shows KoCo-SMC 's superior time efficiency compared to available exact solvers. Fig- ure demonstrates Koco-SMC 's advantage in finding exact solutions over approximate solvers. Figure 5 shows that the proposed ULW algorithm accelerates solving SMC problems. Finally, Figure 6 demonstrates that KoCo-SMC can efficiently handle two real-world applications.
The exact solver baseline is composed of an exact SAT solver and probabilistic inference solvers. This approach first identifies solution to the Boolean formula and then verifies it with the probabilistic constraints. For the Boolean SAT solver, use Lingeling (Heule al., 2019), CaDi- Cal (Biere et al., 2024), MiniSAT (Eén & Sörensson, 2003) for their superior performance. For probabilistic inference, we use the UA12010 winning solver implemented in lib- DAI (Mooij. 2010) (UAT10) and the solver based on the hybrid best-first branch-and caanch-and-Bee and-bound algorithm (HBFS) de- veloped by Toulbar2 (Cooper al., 2010). Due to the underlying connection between probabilistic inference and weighted model counting, we also include model counters from recent Model Counting competitions (Fichte et al., 2021) from 2020 to 2023: D4 solver (I (Lagniez. & Marquis, 2017), 2017), ADDMC (Dudek et al., 2020), and SSTD (Korhonen & Järvisalo, 2023).
5.1. Experiment Settings
Dataset. We fix the number of probabilistic constraints to one. For the weighted function f. we use benchmark instances from the partition function task in the Uncertainty in Artificial Intelligence (UAI) Challenges, held between 2010 and 2022. We retain 50 instances defined over binary variables and group them into six categories: Alchemy (1 model), CSP models), DBN (6 models), Grids (2 models), Promedas (32 models), and Segmentation (6 models). For the Boolean formula é, we generate 9 random 3-coloring map problems using CNFgen (Lauria et al., 2017). These instances involve binary encodings with variable counts ranging from 75 to 675. Unless noted otherwise, each task uses three thresholds q obtained by multiplying the model's partition function by 10-20 10-10, and 10-1, This yields 1,350 data points in total.
Implementation of Koco-SMC. We applied ACE (Dar- wiche & Marquis, 2002) the knowledge compiler. The CDCL skeleton of Koco-SMC is implemented on top of Mi (Fén & Sörensson, 2003), for its easily extensi- ble structure. Appendix collects the detailed experiment settings.
Baselines We consider several approximate SMC solvers and exact SMC solvers. For the approximate solver, we include the Sampling Average Approximation (SAA) (Kley- wegt et al., base) method. Specificallyy, we use Lin-
5.2. Result Analysis
Comparison with Exact Solvers. We begin by examining how exact SMC solvers perform on problems with varying
7

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
Instaness (%)
100
XOR
ROCO-MM louns)
Rumning Time (sccond
10a
Solved Instamoes (%)
80
GAA
-0-
limerst
SPM
60-
Whng
10.
40
10--1 (Mostty SAT)
Threshold Values
(nleemeddate)
10-1 (Montly UNSAT)
Correct
Koco SMC (with ULN)
Keeo SMC (wohows CLW)
20
SMC (without ULW!
Kooo SMC (with CINN
8.01 8.46..93 Normalized Threshold Value (t)
10p 10 10 10 10"
16
102
10
10
Time Limit (seconds)
Figure 4. Comparison of KOCO-SMC and approximate solvers on datasets partitioned by threshold values. Each gap marks the point at which instances become exceedingly difficult for Koco-SMC. Divided by this gap, we show the performance of approximate solvers accordingly. Koco-SMC solves many instances exactly (lower segment), but it can time out on the complex cases (upper segment). Approximate solvers may produce answers to these challenging problems, but at the expense of solution quality.
Figure 5. The ULW in KoCO-SMC SM crucial for speeding up SMC problem solving. (Left) The running time with varying thresholds ULW propagation accelerates KoCO-SMC by 10 times compared with Koco-SMC without ULW when the threshold reaches 10 (Right) The pereentage of instances solved in 3 hours. ULW helps Koco-SMC to solve more instances within a given running time.
numbers of satisfying solutions. This done by adjust- ing the threshold value q and measuring the corresponding solving time. As q increases, satisfying assignments be- come increasingly rare, eventually resulting in unsatisfiable instances. Specifically, Figure 3(left) shows results for single SMC instance under different g values, where the Boolean constraint is derived from a 3-coloring problem on a 5 x 5 grid, and the probabilistic constraint is based on the smokers-10 uai instance from the UAI 2012 Competition.
cannot guarantee correctness, we classify their outputs as follows. If an output is verifiable, either because an exact solver supplies a reference solution or because the returned assignment can be checked by an exact model counter, we classify the output as correct wrong; otherwise, it is un- verifiable. Then for repeated runs, an instance is labeled Correct if any produces a correct solution, Timeout if no run finishes in time, Wrong if all runs are wrong, and Un- verifiable otherwise. The comparison between KoCo-SMC and approximate solvers is shown in Figure 4.
The SAA-based method provides rapid count estimates from samples. However, like the exact baselines, it can time out while searching for satisfying assignments, especially as the threshold rises and satisfying assignments become rarer. KOR-SMC efficiently reduces an SMC problem to a surro- gate SAT instance with guarantees, but its solution quality degrades on the hardest -hreisom)hheshhold cases, where many SMC instances lie near the SAT-UNSAT transition point. We found that XOR-SMC sometimes finds solu- tions that violate constraints. This is because it only checks the approximate bound. More careful parameter tuning and additional runs may improve its performance. Overall, Koco-SMC solves most instances exactly but may time out on complex cases. Approximate solvers sometimes return answers for these difficult problems, yet their solutions are often of lower quality, being incorrect or cannot be verified.
At low threshold values, all solvers are able quickly find satisfying assignments; however, Koco-SMC incurs ad- ditional overhead due to the knowledge compilation step. As the threshold increases, satisfying assignments become rarer, leading to increased solving time across all methods.
Notably, when the threshold becomes sufficiently high such that the instance is unsatisfiable, Koco-SMC exhibits re- duced solving time, while the runtimes of other solvers re- main high. This efficiency gain stems from Koco-SMe SMC's integrated ULW algorithm, which enables early detection of unsatisfiability unlike bascline solvers, which must ex- haustively enumerate all candidate assignments before con- cluding infeasibility.
The efficiency of KoCo-SMCI is further validated by evalu- ating it on the full dataset. Figure 3 (right) shows the per- centage of solved instances as function of runtime. This figure extends the results in Figure (right) by including additional configurations of Koco-SMC using different Boolean SAT solvers-LLngellnng (Lingeling-), AT (MiniSAT-), and CaDiCaL (CaDiCal-). Among all config- urations and baseline methods, Koco-SMC consistently achieves the best overall performance.
Effectiveness of Upper-Lower Bound Watch Algorithm. In Figure 5(left), ULW propagation accelerates Koco-SMC by 10 times compared with Koco-SMC without ULW when the threshold reaches 105. Figure 5(right) further demonstrates the contribution of ULW, where KoCo-SMC is 10 times faster than Koco-SM MMC without ULW for SMC problems solvable in around 10 minutes.
Comparison with Approximate Solvers. We compare Koco-SMe with approximate solvers under a 10-minute time limit. For fairness, approximate solvers may run mul- tiple times within this limit. Because approximate solvers
5.3. Case Studies
Application: Robust Supply Chain Design. In a supply chain network, each supplier represented as a node that
8

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
Running Time (sec)
10a
KOCO-SMC (ours)
Lingeling-D4
Running Time (sec)
KOCO-SMC (ouns)
Längeling-DL
Lingeling-UAI1
Mineling-ADDMM
Lingeling-UAIO
Längeling-DDDME ADDMC
LingelingHHike HHlls
Lingeling-SSTD SSTD
Lingeling-HBis HBFP
Lingeling-SST1
102
102
Small
Medium
Large
Amazon (b) Package Delivery on Different Graphs
UPS
USPS
(a) Robust Supply Chain with Different Network Size
Figure 6. (Left) Running time of each method for identifying the best trading plan. All methods are tested on three real-world supply chain networks of different sizes. (Right) Running time for identifying the best delivery path. All methods are tested on three road maps of different sizes. Our Koco-SMC finds all the exact satisfying solutions significantly faster.
purchases raw materials from upstream suppliers and sells products to downstream customers. The objective is sure valid trading path from the source provider to the end demander, while maximizing the overall success probabil- ity in the presence of disruptions such as natural disasters. The problem formulation includes two types of constraints: (I) The Boolean constraint ensures the existence of a valid path from the source provider to the end demander. (2) The probabilistic constraint evaluates the reliability of roads, which may be disrupted by stochastic events such as natural disasters, traffic accidents, or political instability.
to below a specified threshold. This probability accounts for factors such congestion, extreme weather, and road construction.
Suppose there are NN delivery locations, and let æi,5 =
True denote that the j-th location is visited in the i-th
position of the path. Combining constraints (I) and (2), we formulate the problem as an SMC instance: o(x) A
Ey y) <y), where {mas i E (1...., N]] is the set of decision variables representing the path, and is the set of latent environmental variables. The term P(x, y) denotes the probability of encountering heavy traffic given path x with environmental conditions y. Detailed settings are provided in Appendix D.5.
Let n2 E [True, False} represent the selection of trade be- tween nodes connected by i-th edge, where x; = True if the trade is selected. Combining the requirements (1) and (2), Φ(x) A (Ey P(x.y)
we have the SMC formulation:
We use three sets of delivery locations in Los Angeles: 8 Amazon Lockers, 10 UPS Stores, and 6 USPS Stores. The experimental graphs are: Amazon Lockers only (Ama- zon), Amazon Lockers plus UPS Stores (UPS), and the UPS graph extended with USPS Stores (USPS), with 8, 18, and 24 nodes, respectively. Traffic congestion probabilities are modeled using Bayesian network trained on LA traf- fic data (West, 2020). Figure 6 (right) shows the runtime required to find the optimal delivery route. KOCO-SMC efficiently discovers high-quality delivery plans under real- world uncertainty.
where the marginal probability Σy y) is the probabil- ity that all selected trades are carried out successfully and is the minimum requirement of successful probability.
We use 4-yeyer supply chain networks from the wheat-to- bread network with 44 nodes (Large) (Zokaee al., 2017). where each layer represents supplier tier. We also create synthetic networks with 20 (Small) and 28 (Medium) nodes. To identify the plan with the highest success probability, we incrementally raise the threshold from 0 to I by 1 x 10-2 until the SMC problem becomes unsatisfiable. Detailed settings are in Appendix D.4. The running time for finding the best plan is shown in Figure 6(left). Our Koco-SMC needs much less time than baselines to find the optimal plan.
6. Conclusion
We introduced Koco-SMC for exact solving of Satisfiabil- ity Modulo Counting problems. Unlike existing methods that combine SAT solvers with model counters, Koco- SMC employs an early conflict detection mechanism by comparing the upper and lower bounds of probabilistic infer- ences. Our Upper-Lower Watch algorithm efficiently tracks these bounds, enabling efficient solving. Experiments on large-scale datasets show that Koco-SMC delivers higher solution quality than approximate solvers and significantly outperforms existing exact solvers in efficiency. Real-world applications further demonstrate its potential for solving practical problems.
Application: Package Delivery. The task is to find path that visits all specified delivery locations exactly once while minimizing the probability of encountering heavy traffic (Hoong et al., 2012). Delivery locations and roads are modeled as nodes and edges in a graph, respectively. The problem involves two key components: (1) A Boolean constraint that ensures each location is visited exactly once, with road availability based real-world data from Google Maps. (2) A probabilistic constraint that limits the likeli- hood of encountering heavy traffic on any road segment
9

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
Acknowledgement
Cooper, M. C., de Givry, S., Sánchez-Fibla, M., Schiex, T., Zytnicki, M., and Werner, T. Soft are consisteney revisited. Artif. Intell., 174(7-8):449-478, 2010.
We thank all the reviewers for their constructive comments. This research was supported by NSF grant CCF-1918327, NSF Career Award IIS-2339844, DOE Fusion Energy Science grant: DE-SC0024583.
Darwiche, A. Compiling knowledge into decomposable negation normal form. In IJCAI, pp. 284-289. Morgan Kaufmann, 1999.
Impact Statement
Darwiche, A. Decomposable negation normal form. J. ACM, 48(4).608 647, 200
Satisfiabilityy Modulo Counting (SMC) extends traditional Boolean satisfiability by incorporating constraints that in- volve probability inference (model counting). This exten- sion allows for solving complex problems where both log- ical and probabilistic constraints must be satisfied. SMC has wide applications in supply chain design, shelter allo- cation, scheduling problems, and many others in Operation Research. For example, in scheduling problems, SMC can ensure that selected schedules meet probabilistic events, while in shelter allocation, can verify that the accessibility under random disasters is above specified threshold.
Darwiche, A. On the tractable counting of theory models and its application to truth maintenance and belief revi- sion. J. Appl. Non Class. Logics, 11(1-2):1134,, 2001b.
Darwiche, A. A logical approach to factoring belief net- works. In KR, pp. 409-420. Morgan Kaufmann, 2002.
Darwiche, A. New advances in compiling enf to decompos- able negation normal form. In ECAL, pp. 318-322, NLD, 2004. IOS Press. ISBN 9781586034528.
References
Darwiche, A. and Marquis, P. A knowledge compilation map. J. Artif. Intell. Res., 17:229-264, 2002.
Achlioptas, D. and Theodoropoulos, P. Probabilistic model counting with short xors. In SAT, volume 10491 of Lec- ture Notes in Computer Science, pp. 3-19, 2017.
d' Avila Garcez, A. S., Besold, T. R., Raedt, L. D., Földiák, P., Hitzler, P., Icard, T., Kühnberger, K., Lamb, L. C., Mikkkuainenn, R., and Silver, D. Neural-symbolic learning and reasoning: Contributions and challenges. In AAAI Spring Symposia. AAAI Press, 2015.
Almeida, R. M., Shi, Q. Gomes-Selman, J. M., Wu, X., Xue, Y., Angarita, H., Barros, N., Forsberg, B. R.,, García- Villacorta, R., Hamilton, S. K., Melack, J. M., Montoya, M., Perez, G., Sethi, S. A., Gomes, C. P., and Flecker, A. S. Reducing greenhouse gas emissions of amazon hydropower with strategic dam planning. Nature Com- munications, 10(1):4281, 2019.
Dechter, R. and Mateescu, R. AND/OR search spaces for graphical models. Artif. Intell., 171(2-3):33-066 2007.
Dennis, L. A., Farrell, M., and Fisher, M. Developing multi- agent systems with degrees of neuro-symbolic integration [A position paper]. CoRR, abs/2305. 2023.
Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., and Pollitt, F. Cadical 2.0. In CAV, volume 14681, pp. 133-152. Springer, 2024.
Ding, F. and Xue, Y. Contrastive divergence learning with chained belief propagation. In PGM, volume 138, pp. 161-172, 2020.
Chavira, M. and Darwiche, A. On probabilistic inference by weighted model counting. Artif. Intell., 172(6-7):772- 799, 2008
Dubray, A., Schaus, P., and Nijssen, S. Anytime weighted model counting with approximation guarantees for prob- abilistic inference. In CP, volume 307 of L/Plcs, pp. 10:1-10:16, 2024.
Cheng, C., Luo, Y., and Jiang, J. R. Knowledge compi- lation for incremental and checkable stochastic boolean satisfiability. In IJCAI, pp. 1862-1872. ijcai.org. 2024.
Dudek, J. M., Phan, V., and Vardi, M. Y. ADDMC: weighted model counting with algebraic decision diagrams. In AAAI, pp. 1468-1476 AAAI Press, 2020.
Cheng, Q., Chen, F., Dong, J., Xu, W., and Ihler, A. Approx- imating the operation for marginal-map inference. In AAAL, pp. 1882-1887, 2012.
Ećn, N. and Sörensson, N. An extensible sat-solver. In SAT, volume 2919, pp. 502-518. Springer, 2003.
Choi, Y., Friedman, T., and Van den Broeck, G. Solving marginal MAP exactly by probabilistic circuit transfor- mations. In AISTATS, volume 151 of Proceedings of Machine Learning Research, pp. 10196-10200 PMLR, 2022.
Fan, Y. and Jiang, J. R. Sharpssat: witness- gennersign stochastic boolean satisfiability solver. In AAAI, pp. 3949 3958. AAAI Press, 2023.
10

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
Fichte, J. K., Hecher, M., and Hamiti, F. The model counting competition 2020. ACM J. Exp. Algorithmics, 26:13:1- 13:26, 2021.
Lauria, M., Elffers, J., Nordström, J., and Vinyals, M. Cnf- gen: A generator of crafted benchmarks. In SAT, volume 10491, pp. 464-473. Springer, 2017.
Fredrikson, M. and Jha, S. Satisfiabilityy modulo counting: approach for analyzing privacy properties. In CSL- LICS, pp. 42:1-42:10. ACM, 2014.
Lee, N., Wang, Y., and Jiang, J. R. Solving stochastic boolean satisfiability under random-exist quantification. IJCAI, pp. 688-694. ijcai.org, 2017.
Ge, C. and Biere, A. Improved bounds of integer solution counts via volume and extending to mixed-integer linear constraints. In CP, volume 307 of LIPIcs, pp. 13:1-13:17, 2024.
Lee, N., Wang, Y., and Jiang, R. Solving exist-random quantified stochastic boolean satisfiability clause se- lection. In IJCAI, pp. 1339-1344 1345. ijcai.org, 2018.
Li, J., Jiang, N., and Xue, Y. Solving satisfiability modulo counting for symbolic and statistical AI integration with provable guarantees. In AAAI, pp. 20481-20499 2024.
Gomes, C. P., Sabharwal, A., and Selman, B. Model count- ing: A new strategy for obtaining good bounds. AAAI,
pp. 54-61, 2006.
Hamadi, Y., Jabbour, S., and Sais, L. Manysat: parallel SAT solver. J. Satisf. Boolean Model. Comput., 6(4):
Li, Z.,, Huang, Y., Li, Z., Yao, Y., Xu, J., Chen, T., Ma, X., and Lu, J. Neuro-symbolic learning yielding logical constraints. In NeurlPS, 2023.
245-262, 2009.
Heule, M. J. H., Järvisalo, M., and Suda, M. SAT compe- tition 2018. J. Satisf. Boolean Model. Comput., 11(1):
Marinescu, R., Dechter, R., and Ihler, A. ANDIOR search for marginal MAP. UAI, pp. 563-572. AUAI Press, 2014.
133-154, 2019.
Hoong, P. K., Tan, I. K. T., Chien, O. K., and Ting, C. Road traffic prediction using bayesian networks. In ICWCA, pp. 1-5. IEEE, 2012.
Mooij, M. libdai: A free and open source C++ library for discrete approximate inference in graphical models. J. Mach. Learn. Res., 11:2169-22 210099221131111 2010.
Israeli, and Wood, R. K. Shortest-path path network interdic- tion. Networks, 40(2):97-111, 2002.
Moskewicz, M. W., Madigan, C. F,, Zhao, Y., Zhang, L., and Malik, S. Chaff: Engineering an efficient SAT solver. In DAC, pp. 530-535. ACM, 2001.
Kempe, D., Kleinberg, J. M., and Tardos, É. Influential nodes in diffusion model for social networks. In ICALP, volume 3580 of Lecture Notes in Computer Science, pp- 1127-1138. Springer. 2005.
Papadimitriou, C. H. Games against nature. J. Comput. Syst. Sci., (122)288-301, 1985.
Kisa, D., Van den Broeck, G., Choi, A., and Darwiche, A. Probabilistic sentential decision diagrams. In KR, 2014.
Park, D. and Darwiche, A. Complexity results and ap- proximation strategies for MAP explanations. J. Artif. Intell. Res., 21:101-133, 2004.
Kleywegt, A. J., Shapiro, A., and Homem-de-Mello, T. The sample average approximation method for stochastic dis- crete optimization. SIAM J. Optim., 12(2):479-502, 2002.
Peharz, R., Lang, S., Vergari, A., Stelzner, K., Molina, A., Trapp, M., Van den Broeck, G., Kersting, K., and Ghahra- mani, Z. Einsum networks: Fast and scalable learning tractable probabilistic circuits. In ICML, volume 119 Proceedings of Machine Learning Research, pp. 7563- 7574. PMLR, 2020.
Korhonen, T. and Järvisalo, M. Sharpsat-td in model count- ing competitions 2021-2023. CoRR, abs/2308. 15819, 2023.
Lagniez, J. and Marquis, P. An improved decision-dnnf compiler. In IJCAL, pp. 667-673, ijcai.org, 2017.
Ping, W., Liu, Q., and Ihler, A. Decomposition bounds for marginal MAP. In NIPS, pp. 3267-3275, 2015.
Latour, A. L. D., Babaki, B., Dries, A., Kimmig, A., Van den Broeck, G., and Nijssen, S. Combining stochastic con- straint optimization and probabilistic programming from knowledge compilation to constraint solving. In CP, vol- ume 10416, pp. 491-511, 2017.
Poon, H. and Domingos, P. M. Sum-product networks: A new deep architecture. In UAI, pp. 337-346. AUAI Press, 2011.
Rahman, T. Kothalkar, P. V., and Gogate, V. Cutset net- works: A simple, tractable, and scalable approach for im- proving the accuracy of chow- liu trees. In ECML/KKDD, volume 8725. pp. 630-645. Springer, 2014.
Latour, A. L. D., Babaki, B., and Nijssen, S. Stochastic constraint propagation for mining probabilistic networks. In IJCAI, pp. 1137-1144 115.. ijeai.org, 2019.

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
Shapiro, A. Monte carlo sampling methods. Handbooks in operations research and management science, 10:353- 425, 2003.
Sheth, and Roy, K. Neurosymbolic value-inspired artificial intelligence (why, what, and how). IEEE Intell. Syst, 39(1):5-11, 2024.
Silva, J. P. M. and Sakallah, K. A. GRASP a new search algorithm for satisfiability, In ICCAD, pp. 220-227, IEEE Computer Society/ ACM, 1996.
Silva, J. P. M. and Sakallah, K. A. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers, 4865):506-52,, 1999.
Toth, P. and Vigo. D. (eds.). The Vehicle Routing Problem, volume 9 of SIAM monographs on discrete mathematics and applications. SIAM, 2002.
Vergari, A., Choi, Y., Peharz, R., and Van den Broeck, G. Probabilistic circuits: Representations, inference, learn- ing and applications. IJCAI Tutorial, 2020.
West, C. Los angeles traffic prediction bayesian network. htips://github www/ cwwp///w269////// / LLA_. Traffic_Bayesiant Net, 2020. Accessed: Septem- ber 30, 2024.
Zhang, H. and Stickely, M. E. An effcient algorithm for unit propagation. Proc. of AI-MATH, 96, 1996.
Zokaee, S., Jabbarzadeh, A., Fahimnia, B., and Sadjadi, J. Robust supply chain network design: an optimization model with real world application. Annals of Operations Research, 257:15 44, 2017.
12

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
A. Probabilistic Inference in Probabilistic Circuits
Probabilistic inference in a probabilistic circuit can be highly efficient, Figure 7 illustrates a decomposable and smooth probabilisttic circuit, where each node corresponds False), set the values of nodes æ1, T2, 23, and I4 to I, and set æ2 and Φ O. Finally, evaluate the root node obtain the probability, which in this case is 0.1.
binary distribution. To compute P(z1 zg = I4 True, 22
For the marginal probability, the circuit must be both decomposable and smooth to ensure correctness and efficiency. In Figure 7 (b), to calculate P(r3 = 24 True), set the values of nodes 43 and to 1, reflecting their assigned values. For the marginalized variables 21 and 22, set all associated nodes - I1. Tι, T2, and T2 to Then evaluate the root node, which should yield probability of 1.0.
P(z1 I3 24
True, 22 False) 0.1
Exy 22
P(13 = I4
True) = 1.0
0.5
0.5
0.5
0,5
True
True
True
True
T3
T4
L3
34
0.2
0.8
0.2
0.8
0.2
0.8
0.2
0.8
T22
TT
T2
I
T2
T1
T2
True
False
False
True
(a) compute probability P(2: 23 True, I2 False)
(b) compute marginal probability Ex Ples 24 True).
Figure 7. Example of probability inference in a decomposable and smooth probabilistic circuit. To infer the probability P(
24 True, da = False), set value of nodes æ1, T2. 43. and 24 to I. Also value of nodes Ti and æ2 to 0. The circuit evaluates True), set nodes 23 and z4 to 1. For the marginalized-out variables circuit evaluates to the marginal probability 1.0.
the probability 0.1. To infer the marginal probability P(r3 21 and 72, set all related nodes
B. Proof of Lemma 3.1
Assumption B.1 (Smooth and Decomposable (Choi al., 2022)). A smooth probabilistic circuit when all children of every sum node share identical sets of variables; probabilistic circuit is decomposable if the children of every product node have disjoint sets of variables; Smoothness and decomposability enable tractable computation of any marginal probability query. Definition B.2. Denote assigned variables in x as x, and those not assigned as X The exact upper and lower bounds of the marginal probability with the partial variable assignment are maxx, Ey P(xe, Xh, y) and minx, Ey P(xe, Xr. y)..
Proof. To prove that UB 2 maxx, Ey P(xe, Xn, y) and LB < minx, Ey P(xe, Xh, y), we need to relate the updating scheme with the marginal probability inference. We focus on the upper bound case (UB); the lower bound follows by a symmetric argument. Let X arg maxx, Ey P(x,, Xt. y) denotes the assignment to X₁, that maximizes the marginal probability. We now show that the updates in ULW algorithm guarantee UB Ey P(xe; xf, by recursion.
Base case. Consider leaf node corresponding to a single variable: (f) E is already assigned, then UB(r)) Pz(x). (2) If x E X₁, is unassigned, then U (()) = max, (.( 2 P.(x*). (3) If E is marginalized out, then (B - E, -,,
Po(y) 1.
From these cases, we observe that the upper bound computation potentially overestimates the contributions from leaf nodes associated with unassigned variables in Xn, while the contributions from X, and y remain unchanged. Once all variables are assigned, the leaf evaluations match those used in exact marginal inference.
13

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
X2)
Px(x1
W1
U2
U2
Po. (x1)
Pay (x2)
Pe. (x)
Poy (x1, x2)
Figure (Left) Example of decomposable product node (colored blue). Denote the product node as p. and has two children eı and e2. Child nodes encode P. (x1) and (x2) respectively and the product node encodes (x Xu) = Pe, (x.). Decomposability ensures Xı and X2 are disjoint. (Right) Example smooth sum node (colored red). Denote the sum node as s, and has two children vn and with weights wi and w2. Child nodes encode Po2 (x1, x2) and Poz (x1,x2) respectively and the sum node encodes P. (x x2) wi Pr (x1, x2) + w22 x2). Smoothness ensures all nodes encode probabilities over the same set of variables.
Induction step for product node. Suppose is a product node (see Figure 8 for an illustrationn. Without loss of generality, assume v has two child nodes, and 02, which represent Pv. (xe (1) Xx y()) and Po X y (()),
(2)
respectively.
By the decomposability property, the scopes of en and U2 are disjoint, i.e. they do not share any variables. This allows the maximization over the product to be decomposed into the product of maximization over the children. More formally, we
have
UB(C) = B(m) UB(22) 2 max I Po
(x(
(1) Xh y
(2))
Poz (x!2) xx
(2) (2))
max
(L)
(x Xh (1 (x! (2)
max
y())) y(2)
P (x Xx
(1) (1)) P. (x! x ,,y(2))
max x/x
max
P. (x x/,y)
x
Induction step for a sum node. Suppose e is sum node. Since the probabilistic circuit smooth, all of its children must share the same scope of variables. Without loss of generality, assume e has two child nodes, i/ and U2, which represent Po₁ and P Pgg. with corresponding weights wi and w2. Then we can derive
UB(()= wn wB(B)())) U222 2 max
Σ wi Po, (X', (Xe,, X210))
+ max X,
Σ w2 Po (og (Ke
X,
max X),
(x
By recursive application of the update rules, we conclude that the upper bound satisfies UB 2 maxx. Ey P(xe X), at the root node. A similar argument applies to the lower bound. Our proposed ULW algorithm follows this computation exactly, requiring only a single pass through the probabilistic circuit via bottom-up traversal.
C. Koco-SMC Implementation
Classical SAT solvers like MiniSAT (Eén & Sörensson, 2003) have achieved high performance in real-world applications. We implement our method based on MiniSAT version 2.2.0 The decision, unit propagation, and backtracking steps are primarily derived from their implementation. We introduce the ULW algorithm, which enables conflict detection for probabilistic constraints in SMC problems. In this section, we present the implementation of the key components of Koco-SMC. The pseudocode is shown in Algorithm
*MinSAA:: httpp::///g httpss:///tttuu..ooo http:///www....laassi.i.iiiiieee
14

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
Probabilistic Graphical Model
Weighted Boolean Formula
Probabilistic Circuit
d-DNNF
Figure 9, The process of constructing probabilistic cireuits from probabilistic graphical models by ACE.
Compilation RoCO-SMC requires that all probability distributions in the SMC problem be compiled into smooth and decomposable PCs. In our implementation, all distributions are represented probabilistic graphical models, either in the form of Bayesian networks Markov Random Fields.
The pipeline introduced in (Darwiche, 2002) (Fig. 9) compiles distribution into a Boolean formula augmented with literal weights, which is then further compiled into a tractable algorithmic circuit. From this circuit, a tractable probabilistic circuit is derived. We use ACE' as the knowledge compilation tool.
ULW Algorithm After performing unit propagation on the Boolean constraints, we record the currently assigned variables the current decision level. Next, we update the bounds for each affected probability distribution. These updated bounds then compared detect either conflict early satisfaction. If probabilistic constraint is already satisfied, mark it and skip further updates until a future backtracking step. If probabilistic constraint becomes unsatisfiable, raise conflict using the same mechanism as for Boolean conflicts and record corresponding conflict clause.
Conflict Clause from the Probabilistic Constraint The conflict clause derived from probabilistic constraint is a Boolean clause that captures the cause of the conflict. We construct this clause by taking the negation of the current variable assignment. For example, if a constraint of the form Σz, P(r1 = True, I2 = False, Fz3 > q triggers a conflict, we generate the Boolean clause (xn V x2) as its negation. This ensures that any future assignment where si True and 22 = False will violate the new clause, preventing the same unsatisfiable condition. Similar to CDCL-based SAT solvers, the learned clause is added to the Boolean formula that the solver avoid repeating the same conflict without needing to re-evaluate probabilistic inference.
D. Experiment Setting
D.1. Dataset Specification
All SMC problems in this study are in the form of o(x,, x,) f(x,,)) q) where d(xx, xy) is a CNF Boolean formula, is a (unnormalized) probability distribution. X decision variables that appear only in d, xy decision variables shared by Φ and f, and y are latent variables that are marginalized.
Boolean Formula We pick random variables from & and f as shared variables uniformly at random. The number of shared variables between & and f (denoted as xy) is determined as the lesser of either half the number of random variables in f or the total number of random variables in Φ; that is, the count of variables in xy will not exceed either half the total number of variables in f or the total number of variables in 6.
All d(x;, Xf) represent 3-coloring problems for graphs, which involve finding an assignment of colors to the nodes of graph such that no two adjacent nodes share the same color, using most 3 colors in total. Each node in the graph corresponds to 3 random variables, say æı, I2, and Zz. where z1 = True if and only if the node is colored with the first color. We consider only grid graphs of size k by k, resulting in & x x 3 variables.
Those Boolean formulas are generated by CNFgen using the command
enfgen kcolor grid k k -T shuffle
where the graph size k is set to 5, 10, and 15. For each grid graph, we shuffle the variable names randomly and keep 3 of them.
ACC: eea/aa..ea.cc..aeee///.a edu/ace
CCNggen: https:/ hattss//mmmssnase htt////ssmmmmaaaaaaaaaaaaaaa wetrrii..neetteee fgen/
15

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
Probability Distribution We use probabilistic graphical models from the UAT competition 2010-2022* including Markov random fields and Bayesian networks for the probabilistic constraints. Specifically, pick the data for PR inference task, which includes categories: Alchemy (2 models), CSP (3), DBN (6), Grids (8), ObjeciDetection (79), Pedigree (3), Promedas (33), and Segmentation (6). The models with non- non-Boolean variables are removed, resulting in the remaining 50 models: Alchemy (1 model), CSP (3), DBN (6), Grids (2), Promedas (32), and Segmentation (6). All distributions are in the UAI file format. Since model counters d4, ADDMC, and SharpSAT-TD only accept weight CNF format the model counting competition, we use bn2enf to convert data.
D.2. Baselines
Gibbs-SAA and BP-SAA are approximate SMC solvers based on Sample Average Approximation. The marginal probability in the form M, P(z, y) is approximated using samples. More specifically, we use a sampler to generate set of samples {(z, } according to distribution proportional to P(z, y). Then the marginal probability is estimated as the sample average N Σyer P(x, ((), multiplied by the number of possible configurations of For binary variables of length n, there are 2n possible configurations. We use the Gibbs Sampler (Gibbs-SAA) and Belief Propagation (BP-SAA) implementations from (Ding& & Xue, 2020) as the samplers. However, sampling is only an efficient probabilistic inference method, still requires fixing x in advance. Thus, we use Lingeling to enumerate solutions of ((x).
Given a time limit of hour, we set the number of samples 10000 and the number of Gibbs burn-in steps 40. For each SMC problem in the benchmark dataset, at least one of those runs produces correct result. The percentage of solved SMC problems is shown in Figure 4.
each approximate solver 5 times, and the problem is considered "solved" if
XOR-SMC an approximate solver from (Li et al., 2024). We set the parameter (which controls the probability of finding satisfying solution- higher T yields better performance at the cost of longer runtime) to 3. and incrementally increase the number of XOR constraints from until either timeout failure occurs. This process allows us find the most probable satisfying solution. Similar the SAA-based approaches, we run XOR-SMC 5 times.
Lingeling-UAII UAT10 and Lingeling-HBFS integrate the SAT solver Lingeling (Heule et al., 2019) with high-performance probabilistic inference solvers from the UAI Approximate Inference Challenge. The procedure begins by running I. Lingeling to produce solution that satisfies the Boolean formula the SMC problem. The resulting assignment is then passed the inference solver to compute the corresponding marginal probability. If this probability exceeds the specified threshold, the solution is reported and the algorithm terminates. Otherwise, the SAT solver is invoked to generate a different solution, and the process is repeated until all solutions have been enumerated. To ensure a fair comparison, repetitive file I/O and solver initialization overheads have been minimized.
Lingeling-UAte UAII0 uses the public inference solver LibDAI (Mooij, 2010), which participated in the UAI 2010 challenge and is available on GitHub". Bongeling-HBFF uses the Toulbar2 solver (Cooper et al., 2010), which implements hybrid best-first branch-and-bound algorithm (HBFS) for computing marginal probabilities. We use the public implementation of T for the probabilistic reasoning task, with default parameter settings.
Lingeling-Dee DD,, Lingeling-ADDMC, and Lingeling-SSTD are integrations of the Lingeling SAT solver with the weighted model counting solver in the Model Counting Competition from 2020 to 2023. Lingeling-Dee -D4 uses d4 solver based on knowledge compilation. Lingeling-ADDor -DDMMC uses the public implementation of the ADDMC solver 10, Lingeling-SSTD uses STTrpSAT-TDD' the model counter.
*UA12022: /tt.app...tss//aaaccooooptooottp
httpdd/ffttttso./......a.aaaaaaa html
'44: acsp:///gittubbccm//rr111//// 10 AADDo/..tter//gtttoooooo/rrrrrrp
16

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
X1
X4
X6
X2
X5
Xy
X3
Wheat Farm
Flour Factories
Bread Factories
Bakery store
Figure 10. An example wheat bread supply supply chain network. x, True means the trade is selected from the supplicr to the demander.
D.3. Hyper- Syper-Parameter Settings
In all experiments, use the public version of Lingeling implemented in PySAT with their default parameter. The time limit for all approximate solvers (Gibbs-SAA, XOR-SMC) is set to I hour per SMC problem. The time limit for all exact solvers is 3 hours. All experiments are executed on two 64-core AMD Epyc 7662 Rome processors with 16 GB of memory.
D.4. Application: Supply Chain Design
For the experiment real-world supply chain network, we refer to 4-layer supply chain network collected from real-world observations (Zokaee et al., 2017). An example is shown in Figure 10.
Decision Variable. Each edge between two nodes represents a trade, and the selection of trades can be encoded as a binary vector x E (True,False) L where M is the number of edges. Here, z; True indicates that the i-th edge (trade) is selected.
Boolean Constraints. Due to budget limitations, each node is assumed receive raw materials from exactly 2 upstream suppliers and sell its products to exactly downstream demanders.
Probabilistic Constraints. The supply chain design problem in (Zokaee et al., 2017) does not consider stochastic disasters; we address this by generating a Bayesian Network (BN) over all edges to model such random events. Let P(x1 = True, 222 = False....) denote the joint probability that trade on edge will not be affected by the disaster, trade on edge will be affected, and so on. Suppose we choose to conduct trades only on edges and 3. Then the marginal probability (æ= True, 23 True) = Ezz P True, 22, 23 True....) denotes the likelihood that the selected trades are all successful.
Ensuring that the probability of the selected trades not being affected by disasters exceeds certain threshold can be formulated as:
Σ P eeeseee Xunselected) > >g
Xatsclecto
where plan to execute trades edges Xselected- The marginal probability Σ P corresponds to the likelihood that all selected trades are successfully conducted. To find the optimal plan, we incrementally increase the threshold from 0 to in steps of 1 10-3, continuing until the SMC problem becomes infeasible. The last feasible solution is referred to as the best plan.
Construction of dataset. This network consists of 4 layers of nodes representing suppliers, with each layer containing 9, 7, 9, and 19 nodes, respectively. Adjacent layers are fully connected, meaning each node can trade with any node in the neighboring layers (i.e., the nearest upstream suppliers and downstream demanders). We evaluate all exact SMC solvers on
PPPSAAT: https:/ : hptpsttt..hhh/ap/p wiiitthhhhgtt...ee.. thub. io/
17

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
three supply chain networks: small network [5, 5, 5,, a medium network 7, 7]. and a large network [9. 7, 19). The vector [9, 7, 19] represents the structure of the real-world network, with 9, 7, 9, and 19 suppliers in each layer, respectively. The other two networks are synthetic but of comparable scale. The results are shown in Figure 6.
For the specification of each generated disaster BN, each node can have at most 5 parents, and the number of BN edges is approximately half of the maximum possible. The generated BN is included in our code repository.
D.5. Application: Package Delivery
For the case study of package delivery, our goal is to deliver packages to N residential areas. We want this path to be a Hamiltonian Path that visits each vertex (residential area) exactly once without necessarily forming a eycle. The goal is to determine whether such a path exists in a given graph.
Decision Variable. Using an order-based formulation with variables zt,j. where Ti,y denotes that the i-th position in the path is occupied by residential area j. i.e., residential j j is the i-th visited place.
True
if area j is visited in the i-th position in the path,
Fi.
False
otherwise.
where the total number of variables is N2 (for N cities).
Boolean Constraints. e a CNF that checks if the variable assignment forms Hamiltonian path. A Hamiltonian path in a graph is path that visits each vertex exactly once.
Probabilistic Constraints. Additionally, we want the schedule to have very high probability (g) of encountering light traffic.
P(Ipath) Σ P(Tppath Tenv) 2 q
where P denotes the probability of light traffic, Fpahh represents the decision variables for the chosen path, and Venv refers to latent environmental variables that affect traffic conditions, such weather, road quality, and other external factors. The marginal probability >x... P then represents the average probability of light traffic, marginalized over all possible environmental conditions.
The graph structures used in our experiments are based on cropped regions from Google Maps (Figure 11). We consider three sets of delivery locations: Amazon Lockers, 10 UPS Stores, and 6 USPS Stores. The three maps we examine are: Amazon Lockers only (Amazon), Amazon Lockers plus UPS Stores (UPS), and UPS graph with the addition of 6 USPS Stores (USPS). These graphs consist of 8, 18, and 24 nodes, respectively.
Construction of dataset.
The traffic condition probability is modeled by Bayesian network (Figure 11) simplified from Los Angeles traffic data (West, 2020).
stochasticity of random events
Hewtolss
The Childtenn Mussum of indiutaaaoo
Demoto
The UPS Store
The UPS Stor
The
UPS Store Aoa
Road Construction
Extreme Weather
Traffic Jam
Porch Drow
The und Stors sewicee
(a) Example Hamiltonian path for visiting 7 UPS stores. (b) Probability of light traffic over path P(x)
Figure 11. Bayesian network for single road (Hoong al., 2012; West, 2020).
To find the best route, we gradually decrease the threshold of the probability of encountering heavy traffic from to 0 in increments of 10-2, continuing until the threshold makes the SMC problem unsatisfiable. The running time for finding the best plan is shown in Figure 6(right).
18

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
E. Additional Results
E.1. Knowledge Compilation Time
The time for compiling graphical models to decomposable deterministic and smooth probabilistic circuits is shown in Figure 12.
40
#Instances
20
100 Knowledge Compilation Time (s)
Figure 12. Histogram of the knowledge compilation time for probability distributions the benchmark.
E.2. Comparison with Exact Solvers
Figure 3(left) is an example shown in the main text. Additional results on other SMCs consisting of different Boolean formulas and probabilistic graphical models are shown below.
19

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
(a) Probabilistic model from Alchemy
(b) Probabilistic model from CSP
kcolor 3, 5x5.cnff with smokers u0.
kcolor 3 5x5.enf with 54.wcsp.uai
10"
Keux-SMCC
10
Kocp-SMy
LingelingUAA10
Lingeling UADD
10a
Lingeling-+15 H655
Running Time (6)
Lingeling-HHUP
Lingeling 144
Lingeling-Dt
10"
LingelingAAph AADOMIC
Linglling-ADMMM
Running
ingeling--
102
Lingeling $811
107
10t
109
10-1
6,09c+124
7.52e+124
9.29e+124
9.96e+126
9.96e-129
4.80c-118
2.10e 89
9.23e-61
3.26c-49
3.26e 46
Threshold
Threshold
(c) Probabilistic model from DBN
(d) Probabilistic model from Grids
kcolor 5x5.cnf with rbm, 20.uai
kcolor _3 3.5x5.cnn with grid10x10.
10a
Kaco-SMC
104
Koce-SMC
Lingelin--UAAO
Lingeling: LApfo
Ranning (8)
10a
Lingeling HBFS
Running Time (4)
Lingeling-Jjäfe
Lingelng
Lingeling:
102
Lingeling ADDMC
LngelingADDWEE
10'
Lingoling
107
Lingllnn SETD
10a
10a
4.49e-20
9.77e+30
2.13er41
5:9Ge-46
5.90c+49
7.05c+90
1.53e+168
3.30c+245
1.986+275
1.98c+276
Threshold
Threshold
(e) Prohabilistic model from Promedas
(f) Probabilistic model from Segmentation
kcolor 3 5x5.enf with or chain 218.fg.um uai
kcolor 5x5.cnf with 2 17 s.binary:uai
Koco-SMC
10
KuggSMi
Lingeling UADI
Lingeling CADD
Rurning (6)
Lingoling HBPS
Running Time 6))
Lingeling HBPS
Lingeling
Lingeling Di
Lingeling-ADrAM
10a
10
Lingeing SSTD
LingeliggS55T
10-1
109.
10
1.45-225
1.17e-19
9.43e-14
8.77e-10
8.77e-07
2.18e-111
4.30e-97
9.45e-83 Threshold
5.61e-76
5.61e-73
Threshold
Figure 13. Results of SMC problems that consist of fixed CNF file (kcolor_3_5xš.cnf) representing the color problem 5 grid map and probabilistic graphical models from different categories.
20

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
(a) Probabilistic model from Alchemy
(b) Probabilistic model from CSP
kcolor 3 10x10.cnf with 54.wcsp.uui
kcolor 3. 10x10.enf with smokers. u0. u..
104
Kix--MCC
10
Kocp-SMC
Lingeling-UAI
Lingling EA
10"
Linglingg HBFS
Running Time (6)
Lingeling--1US
Lngeling
Lingeling-Dt
107
Kngoling-ADDXO
Ligellig-ADMM
Running
10'
ingeling-S5TD
10a
tir tingeingeet
109
10-1
109
6.05e+124
7.16e+124
8.46++124
8.9de+126
8.94e-129
4.80c-118
1.28e 89
3.39c-61
1.01e-49
1.01e-46
Threshold
Threshold
(c) Probabilistic model from DBN
(d) Probabilistic model from Grids
kcolor 3 10x10.cnf with rbm 20.uai
kcolor 3. 11x000.ccm with grid 10.00.10.uu
10a
Kaco-SMC
10
Koce Koce-SMC
Lingelin--UAAO
Lingeling:
Ranning (8)
Lingeling HBPS
Lingeling
Running Time (4)
Lingelin--
Lingeling<
Lingelin ADDMC
Lingliig-ADDoec Lingelig S6TU
10
Lingolng 3STD
102
10"
10a
10-1
10
4.49e-20
2.76e+31
L69e1-42
6.68e-447
6.68c+50
5.32c-86
2.46e+165
1.4c+244
1.906+2722
1.90c+275
Threshold
Threshold
(e) Prohabilistic model from Promedas
(f) Probabilistic model from Segmentation
kcolor 10x10.enf with or chain 21..fg.uai
kcolor 3 10x10.cnf with binaary.uai
Koco-SMC
Koco-SMc
Lingeling UAILO
Lingeling
Rurning (6)
Lingoling HBPS
Running Time (6)
10a
Lingeling HBPS
Lingeling DI
Vingeling-D4
Linglling-Aroo
Lingelin ADDM
101
Lingling SETD
101
10-1
1.45e-25
1.17e-19
9.43e-14
8.77e-10
8.77e-07
1.26e-148
3.18e-135
8.02e-118
1.09e-110
1.09e-107
Threshold
Threshold
Figure 14. Results of SMC problems that consist of fixed CNF file (kcolor representing the 3 color problem 10 10 grid map and probabilistic graphical models from different categories.
21

---

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
(a) Probabilistic model from Alchemy
(b) Probabilistic model from CSP
kcolor 3 15x15.cnf with 54.wcsp.uai
kcolor 3, 13x15.enf with smokers_ uai
104
Koco-SMCC
10
Kacp-SMi
Lingeling DAILD
Lingeling-UAl
10a
Lingeing
Running Time (6)
Lingeling--1US
Lingeling-Dt
Aagling
Lngellig-ADMMM
155
10a
Lin 1
Running
109
10.
10-1
6.08e+124
7.34e+124
3.86++124
9.43e+126
9.43e-129
4.80c-118
4.12c-91
3.55e-64 64
3.37e-53
3.37e-50
Threshold
Threshold
(c) Probabilistic model from DBN
(d) Probabilistic model from Grids
kcolor 3 15x15.cnf with rbm 20.uai
kcolor 3. 3_15x11115111 11x515.cnf with grid
10
Kaco-SMC
10
Koce SMC
Lingelin--UAAO
Lingeling:
Ranning (s)
10"
Lingeling HBFS
Running Time (4)
Lingeling-(
Lingelng
Lingeling-h4
10a
Lingaling ADDMC
102
Lingeling
10'
10a
10a
10-1
4.49--20
2.76e+31
L69e1442
6.68e-447
6.68c+50
2.86c-83
1.74e+162
1.06+241
1.994+269
1.93c+272
Threshold
Threshold
(e) Prohabilistic model from Promedas
(f) Probabilistic model from Segmentation
kcolor 15x15.enf with or chain 21..fg.uai
kcolor 3 15x15.cnf with binaary.uuii
Koco-SMC
104
Koco-SMi
Rurning (6)
10
Lingeling HBPS
Lingeling UADE
Running Time (6)
Lingoling
Lingeling HBPS
Lingeling
Vingeling-DA
Lingyling-ArgMe
Lingdlngg Al AMCMC
100
Lingllng SSTD
101
109
10
10-1
1.45e-25
1.17e-19
9.43e-14 Threshold
8.77e-10
8.77e-07
1.88e-150
1.39e-135
1.03-1166 Threshold
4.3e-1099
4.31e-106
Figure 15. Results of SMC problems that consist of fixed CNF file (kcolor representing the 3 color problem 15 15 grid map and probabilistic graphical models from different categories.
22


Reviews:
[{"review_id": "OL6PBbyQzM", "reviewer": "Reviewer_Vn9u", "summary": "Satisfiability modulo counting (SMC) is a generalisation of SAT that consists of a propositional formula phi(x,b) and a collection of statements of the forms\n\n1) the marginalisation of a discrete probability function f(x,y) (marginalising the variables in y) is at least some constant q, \n\n2) the marginalisation of a discrete probability function f(x,y) (marginalising the variables in y) is at least the marginalisation of a discrete probability function g(x,z) (marginalising the variables in z).\n\nThe truth value of statements of the form 1) and 2) determine the values of the boolean variables in b.\n\nThat is, SMC instance asks whether values for x can be give such that phi(x,b), where the variables in b are interpreted as the truth values of statements of the form 1) or 2).\n\nThe authors introduce an exact solver for SMC, which they call Koco-SMC. The authors claim that previous approaches to integrate SAT solver to this task boil down to having a SAT solver to enumerate all possible solutions to phi(x,b), and then using a probabilistic inference solver to check whether the constraints 1) and 2) hold, as dictated by the selection of the variables in b. The approach that the authors take in Koco-SMC is to use standard tools for CSPs (e.g., propagation, conflicts clause learning, backtracking) to pick partial assignments to variables in phi(x,b) and then to check whether those partial assignments for variables yield a contradiction for the probability statements. The authors construct probabilistic circuits for computing the value of the functions mentioned in 1) and 2). The use of such functions allows the authors to efficiently compute upper and lower bounds for the values of the functions under partial assignments. These lower and upper bounds can be then used to infer contradiction regarding the probability statements.\n\nFinally the authors experimentally compare their solver to other approximate and exact solver for solving SMCs. Their findings show that their approach is more efficient than others in the literature.\n\n## update after rebuttal\nI maintain my evaluation.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you very much for your review and your positive assessment of our paper. We appreciate your concise summary of our contributions and your acknowledgment of the practical value demonstrated by our experimental results.\n\n---\n\n### **Q1. Main Contribution**\n\nWe propose an integrated **exact SMC solver**, addressing the existing gap in this research community, which previously only had approximate solvers available. \nOur method achieves higher computational efficiency compared to vanilla exact solvers by utilizing our proposed ULW algorithm.\nVanilla exact solvers directly combine SAT solving and probabilistic inference processes, resulting in slow performance due to frequent back-and-forth invocations between these two solvers.\n\n---\n\n### **Q2. Novelty of Our ULW Algorithm**\n\nOur ULW algorithm is inspired by CSP, SAT, and optimization literatures. We have revised the related work section to further clarify the novelty of our contributions:\n\n1. **Relevance between ULW and Upper and Lower Bound Computation**:\n\n```\nOur KOCO-SMC efficiently tracks upper and lower bounds for probabilistic constraints with partial variable assignments. In literature, (Dubray et al., 2024; Ge & Biere, 2024) compute approximate bounds for probabilistic constraints based on the DPLL algorithm. (Choi et al., 2022; Ping et al., 2015; Marinescu et al., 2014) provide exact bounds by solving marginal MAP problems, yet they are more time consuming than our method.\n```\n\n2. **Relevance between SMC and Stochastic Constraint Optimization Problems**:\n\n```\nStochastic Constraint Optimization Problems (Latour et al.,2019; 2017) can be formulated as MILP or CP problems using stochastic constraints to solve SMC problems. Our KOCO-SMC is more specialized for this kind of problem.\n```\n\nThe related works above bridge the connection to the existing theoretical foundations. \n\n---\n\nThank you once again for your valuable feedback. Please let us know if you have any further concerns, and we would be happy to discuss them.", "claims_and_evidence": "The paper is well written and presented. The claims given are supported.", "methods_and_evaluation_criteria": "The authors give a comprehensive comparison of their approach to others in the literature. The methods and evaluation criteria seems suitable for the task.", "theoretical_claims": "The description of their approach in the main part of the paper seems plausible and correct. I did not check the correctness of all the claims from the appendix.", "experimental_designs_or_analyses": "I did not check details related to the experiments.", "relation_to_broader_scientific_literature": "The authors do a good job in setting the scene of the paper and in positioning their results with respect to literature.", "essential_references_not_discussed": "I am not aware of related works that should be cited.", "other_strengths_and_weaknesses": "I think the main abstract contribution of the paper is to use probabilistic circuits as an efficient method to compute upper and lower bounds for the probabilistic functions, which can then be used to yield contradictions. This approach also requires the use of partial assignments, but there the use of CSP techniques are quite standard. Otherwise, from the theoretical point of view, the paper is not that deep. However, if this approach is indeed novel, in this context, it a valuable contribution. Also the experimental results show that their approach work better in practice than the previous approaches.", "other_comments_or_suggestions": "None.", "questions_for_authors": "None.", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "1Ktf2sbfsQ", "reviewer": "Reviewer_1wbr", "summary": "This paper aims to provide an efficient solution to the satisfiability modulo counting problem. It proposes to use probabilistic circuits to encode the propositional formula which is further combined with a conflict-driven clause learning framework to compute bounds for the marginal distributions. Empirical evaluations on the resulting algorithm are further presented.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your careful review and for raising valuable questions.\n\n---\n\n### **Q1: Why is Koco-SMC More Efficient?**\n\nIn general, KOCO-SMC saves time by detecting conflicts early using partial variable assignments, whereas baseline solvers require full variable assignments.\n\n- **Baseline Solvers:** These solvers require multiple back-and-forth interactions between SAT-solving and probabilistic inference. Typically, they first assign **all decision variables** using the SAT solver before checking probabilistic constraints. When a conflict occurs, baseline solvers can only learn to avoid repeating that specific complete assignment.\n- **Koco-SMC:** In contrast, Koco-SMC performs back-and-forth checks after assigning **just a single variable**. It immediately updates the upper and lower probability bounds using the efficient ULW algorithm to detect conflicts. This approach allows conflicts to be discovered much earlier—after only partial assignments—thus avoiding unnecessary evaluations of remaining variables.\n\n**Extreme Example:** When probabilistic constraints in an SMC problem are inherently unsatisfiable, Koco-SMC can confirm unsatisfiability by assigning just a single decision variable. Baseline solvers, however, must enumerate and test all potential assignments generated by the SAT solver.\n\n---\n\n### **Q2: Clarification of the Problem Formulation**\n\n**(1) What are the differences between variables x, y, and z in Equations (1) and (2)?**\n\nThe variables **x** denote the decision variables, while **y** and **z** are latent variables that are marginalized out.\n\n**(2) It is unclear what the given probabilities are in Equations (1) and (2).**\n\nThe given probability distributions can be any weighted functions mapping Boolean variables to real numbers—for example, probabilistic circuits, Markov random fields, or Bayesian networks. The SMC problem formulation imposes no specific constraints on these probability distributions.\n\nFor KOCO-SMC, we specifically compiles probability distributions into probabilistic circuits because PCs have structural properties that significantly benefit our ULW algorithm.\n\n**(3) I don't understand the initialization as described at the end of Section 3 due to the previous two confusions.**\n\nThe initialization mentioned in line 226 refers to the computation of the initial upper and lower probability bounds within the PC.\n\n**(4) How is the value 0.1 at line 165 obtained?**\n\nThis value is provided as an illustrative example demonstrating why our method is more efficient. Detailed steps for this calculation are included in Appendix Figure 7.\n\nSpecifically, line 165 illustrates the calculation using the example distribution represented by the probabilistic circuit in Figure 2(c). By setting **x₁** and **x₂** to **True**, we can compute the marginal probability over **x₃** and **x₄** as **0.1**.\n\n---\n\n### **Q3: Answers to Specific Questions**\n\n- **What is the time complexity required to add the learned clauses to PCs?**\n    \n    The time complexity for adding learned clauses is constant. Our approach adds learned clauses only to the Boolean formula to prevent repeated conflicts. The structure of the PCs remains unchanged.\n    \n- **What if neither bound condition is met? Would it result in approximate solutions rather than an exact solver?**\n    \n    No, it would not lead to approximate solutions. Instead, it implies that additional variables must be assigned to narrow down the upper and lower bounds.\n    \n    Consider a constraint such as $\\sum_y f(x,y) > q$. If the lower bound of $\\sum_y f(x,y)$ is greater than $q$ (or the upper bound is less than $q$), we can conclude UNSAT (or SAT). Otherwise, we continue assigning variables. Once all variables are assigned, $\\sum_y f(x,y)$ will yield an exact numeric value without ambiguity. Thus, Koco-SMC remains an exact solver.\n    \n---\n\n### **Q4: Other Issue**\n\nThank you for suggesting the WMC algorithms based on CDCL. We have now incorporated these references and other relevant related work into the paper.\n\n---\n\nThank you again for your constructive comments. If there are any additional points you'd like us to clarify or discuss, please feel free to let us know.", "claims_and_evidence": "At the end of Section 3.1, the paper claims that the current solvers suffer from the fact that they need to go back and forth invocation between SAT solver and the probabilistic inference process. Still, in the proposed algorithm solver Koco-SMC, it uses the CDCL framework and there's still the back-and-forth since when an unsat assignment comes up, it augments the PC with the unsat clauses just like what the baseline does. Further, since the PC is required to be both smooth and decomposable in this framework, the process of adding learned clauses might introduce non-negligible computational cost. It is unclear to me why the proposed framework is more efficient.", "methods_and_evaluation_criteria": "I don't fully understand the problem formulation of SMC: 1) What are the differences between variables x, y and z in Equation (1) and (2)? 2) It is unclear what the given probabilities are but only the constraints on the marginal distributions are defined as in Equation (1) and (2). Are some probability tables also defined in the formulation of SMC as to the conditional probability tables in Bayesian networks? (3) I don't understand the initialization as described at the end of Section 3 due to the previous two confusions. (4) How is the 0.1 at Line 165 obtained?", "theoretical_claims": "Not applicable.", "experimental_designs_or_analyses": "The experimental results seem sound and the proposed algorithm outperforms the baseline methods.", "relation_to_broader_scientific_literature": "It contributes to the field of statistical machine learning.", "essential_references_not_discussed": "This work is closely related to the field of weighted model counting where some of the WMC algorithms are also CDCL [1] based but no reference is presented.\n\n[1] Möhle, Sibylle, and Armin Biere. \"Combining Conflict-Driven Clause Learning and Chronological Backtracking for Propositional Model Counting.\" GCAI. 2019.", "other_strengths_and_weaknesses": "N/A", "other_comments_or_suggestions": "N/A", "questions_for_authors": "See Methods And Evaluation Criteria.\n\n- What is the time complexity required to add the learned clauses to PCs? Would it blow up the size of PCs?\n- It seems only when the upper bound is lower than q or the lower bound is greater than q, there would be definite outcomes for satisfiability. What if it's neither case? Would it result in approximate solutions instead of being an exact solver?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "cRX8w4jZbX", "reviewer": "Reviewer_HcdQ", "summary": "This paper investigates the Satisfiability Model Counting problem, an extension of SAT that incorporates constraints involving probabilistic inference. The authors propose, KOCO-SMC, an efficient exact SMC solver that leverages probabilistic circuits through knowledge compilation to accelerate repeated probability estimation. To enhance efficiency, they introduce the ULW algorithm, which monitors lower and upper bounds of probabilistic inference for early conflict detection. Empirically, KOCO-SMC significantly outperformed existing exact and approximate SMC solvers on real-world problems.\n\n## update after rebuttal\nI thank the authors for their response and maintain my acceptance recommendation.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you very much for your review and suggestions.\n\n---\n### **Q1: Beyond conflict detection, is KOCO-SMC able to derive propagations from probabilistic inference constraints?**\n\nThis is a very good question. In our context, propagation specifically refers to unit propagation, which derives new variable assignments based on current assignments. Currently, we only perform unit propagation on the Boolean constraints and not on the probabilistic constraints.\n\nThe reason is as follows: consider the constraint $\\sum_y f(x_1, x_2, x_3, y) > q$. Suppose $x_1$ and $x_2$ have already been assigned, and $x_3$ remains unassigned. Since $f(\\cdot)$ is represented as a complex probabilistic circuit (PC), we cannot directly derive the assignment for $x_3$. Instead, we need to evaluate both cases—assigning $x_3$ as True and False—because this assessment can yield three possible outcomes: (1) Both assignments (True and False) satisfy the constraint. (2) Only one assignment satisfies the constraint. (3) Neither assignment satisfies the constraint.\n\n---\n\n### **Q2: Add Citations**\n\nWe have added a citation to CaDiCaL and included additional references in the \"Probabilistic Inference and Model Counting\" section:\n\n[1] Chavira, Mark, and Adnan Darwiche. \"On probabilistic inference by weighted model counting.\" *Artificial Intelligence* 172.6-7 (2008): 772-799.\n\n[2] Cheng, Qiang, et al. \"Approximating the sum operation for marginal-MAP inference.\" *Proceedings of the AAAI Conference on Artificial Intelligence*. Vol. 26, No. 1, 2012.\n\n[3] Gomes, Carla P., Ashish Sabharwal, and Bart Selman. \"Model counting: A new strategy for obtaining good bounds.\" *AAAI*. Vol. 6, 2006.\n\n[4] Achlioptas, Dimitris, and Panos Theodoropoulos. \"Probabilistic model counting with short XORs.\" *International Conference on Theory and Applications of Satisfiability Testing*. Springer International Publishing, Cham, 2017.\n\n---\n\n### **Q3: Writing typos**\n\nWe have added the missing word \"into\" at line 200.\n\n---\n\n### **Q4: Ethical Review Flag**\n\nWe noticed that you flagged this paper for an ethics review. We wanted to confirm whether this was done by accident. We would greatly appreciate further details to properly address any concerns.\n\n---\n\nWe greatly appreciate your insightful comments. If you have any additional suggestions or questions, please feel free to let us know—we are happy to address them.", "claims_and_evidence": "The properties of the ULW algorithm are supported by theoretical analysis, while empirical evaluations confirm the superior runtime performance of KOCO-SMC compared to existing methods.", "methods_and_evaluation_criteria": "The proposed methods behind KOCO-SMC, along with its empirical evaluation, are well-suited for SMC problems.", "theoretical_claims": "I have verified the claim in Lemma 3.1, and it is correct.", "experimental_designs_or_analyses": "I reviewed the experimental designs for the UAI dataset, the two real-world problems, and the ablation study for ULW. The designs and analyses appear sound to me.", "relation_to_broader_scientific_literature": "The SMC problem can encode both symbolic and probabilistic constraints and has found applications in real-world scenarios. This work introduces an efficient exact SMC solver, advancing the practical applicability of SMC problems. Previous works have primarily focused on approximate methods or relied on a straightforward combination of a SAT solver and a probabilistic inference solver, often resulting in poor efficiency.", "essential_references_not_discussed": "Citations are missing in the Probabilistic Inference and Model Counting section of the related works.", "other_strengths_and_weaknesses": "N.A.", "other_comments_or_suggestions": "Please add citation to CaDiCaL. \n\nAt line 200, \"into\" is missing between “probabilistic constraints” and “probabilistic circuits”.", "questions_for_authors": "Beyond conflict detection, is KOCO-SMC able to derive propagations from probabilistic inference constraints?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "F49Q5itf3Z", "reviewer": "Reviewer_L6SD", "summary": "This paper presents a new exact satisfiability-modulo-counting solver: `Koco-SMC`, and demonstrates its performance on benchmarks from a UAI benchmark set, compared to existing state-of-the-art exact and approximate SMC solvers.\n\nThe paper attempts to address a weakness in existing exact solvers: the need for them to alternate between a SAT solver and a probabilistic inference solver. It does so by incorporating an Upper Lower Watch (ULW) algorithm that keeps track of upper and lower bounds on the probabilistic inference parts of the problem, learning conflict clauses from those bounds as it goes.\n\nThe `Koco-SMC` pipeline relies on knowledge compilation to create a decision diagram that is converted into an arithmetic circuit, which is used for the inference. It incorporates branching heuristics, propagation and conflict-driven clause-learning techniques from the literature.\n\nIn the experimental evaluation `Koco-SMC` seems especially strong for problems where the probabilistic constraints are very hard to satisfy, or even result in unsatisfiable problems. `Koco-SMC` seems to refute unsatisfiable instance much faster than existing methods, due to its ability to detect conflicts instead of having to search a large search space.", "questions": "", "limitations": "", "rating": 1, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you very much for the detailed review. We will address your concerns and questions in the following reply.\n\n---\n### **Q1: Related works**\n\nWe deeply appreciate your effort in pointing out the lines of work we missed. We have carefully reviewed the related literature and summarized the main changes below:\n\n1. Relavance to upper and lower bound computation: [Link](https://anonymous.4open.science/r/anonym_koco_smc-61FD/plot/related-bounds.png)\n\n2. Relavance to Stochastic Constraint Optimization Problems: [Link](https://anonymous.4open.science/r/anonym_koco_smc-61FD/plot/related-optimization.png)\n\n3. Modified citations for PCs: [Link](https://anonymous.4open.science/r/anonym_koco_smc-61FD/plot/related-pc.png)\n\n---\n\n### **Q2: SMC problem definition**\n\n1. What is {$f_i$}$_{i=1}^K$?\n\nIt means a set of functions {$f_1,\\ldots, f_K$}. K is the number of total probabilistic constraints.\n\n2. Is it essential that $|x|=|y_i|=|z_i|$? \n\nNo, they are not, because x represents the decision variable, and y, z are marginalized-out latent variables. Their lengths can be arbitrary. We revised the notation in our problem formulation as follows and hope this answers your question.\n    \n[Link to the revised version](https://anonymous.4open.science/r/anonym_koco_smc-61FD/plot/problem-formulation.png)\n\n---\n\n### **Q3: Lemma 1 seems redundant**\n\nOur Lemma 1 holds, or equivalently, Equation 3 holds, when the PC satisfies the smoothness and decomposability properties. Otherwise, the computed upper and lower bounds (UB and LB) through our procedure may not be valid; that is, Equation 3 may be violated for some value assignments to the remaining variables. Thus, it is necessary to place Lemma 1 in the main text.\n\n---\n\n### **Q4: Experiments**\n\n1. Dataset details\n\nEach SMC instance consists of a CNF file for the Boolean SAT constraint, a UAI file for the probabilistic constraint, and a threshold value.\n\nThe original CNF files (9 files generated by CNFGen) and UAI files (50 files selected from UAI competitions held from 2010 to 2022, see details in Appendix C.4) are in the anonymous repository:\n\n`https://anonymous.4open.science/r/anonym_koco_smc-61FD/data/`\n\nThe threshold values are available in the file: `anonymous.4open.science/r/anonym_koco_smc-61FD/data/benchmark_ins/data/inst_[cnf name]_[uai name]/thresholds.txt`\n\nFor the compiled probabilistic circuit files,  most of them are excessively large (>1 GB), so we didn’t include them in the repository for now.\n\n2. Detailed settings for Figure 3\n\nIn Figure 3, we conduct an experiment on a single instance, where the CNF uses the 3-color5x5.cnf file (representing a 3-coloring problem on a 5×5 grid map), and the probabilistic distribution uses the smokers-10.uai file (from the UAI 2012 Competition), with various threshold $q$. The running time of our approach includes the knowledge compilation time for a fair comparison. We conduct extended experiments in Figures 14, 15, and 16.\n\n3. Regarding 'our method requires significantly less time across most instances'\n\nAccording to the results in Figures 3, 14, 15, and 16, we find our method is more efficient than baselines in most cases. In some cases, like Figure 14(c), our method shows inferior running time performance due to huge compilation overhead, which agrees with your statement.\n\n---\n\n### **Q5: Clarification on “Current exact SMC solvers (line 80)” and \"An existing exact SMC solver (line 155)\"**\n\nWe realize that these phrases are misleading as they suggest the existence of an actual tool. To clarify, we have revised the text accordingly.\n\n```\nSince there is no general exact SMC solver, solving SMC problems exactly requires combining tools from SAT solving and probabilistic inference.\n```\n\n---\n\n### **Q6: Other issues**\n\n1. On line 90, we didn’t see the hyperlink in the PDF. We would appreciate it if you could provide more context.\n\n2. Bibliography issue.\n   We've carefully revised the bibliography. [Link to new Bibliography](https://anonymous.4open.science/r/anonym_koco_smc-61FD/plot/references.png)\n\n3. Language and writing issues: We have cleared up the improper use of language errors according to your suggestions.\n\n4. Line 157: \"The root node  in the graph has no parent node.\"\n   It is changed to:\n\n   “The root node is the final output of the probabilistic circuit. It represents the overall probability distribution over the variables.”\n\n5. The use of the word \"model\" is somewhat overloaded in lines 137, 158, and 315.\n   We have cleaned up the usage of the word “model” in these lines for clarity.\n\n6. The use of the x-axis and y-axis for Figure 3 caption.\n   We have cleaned up the related text. It should be:\n\n   [Link to the revised Figure 3](https://anonymous.4open.science/r/anonym_koco_smc-61FD/plot/figure3.png)\n\n---\n\nThank you again for your detailed review—your comments have been incredibly helpful in improving the paper. We hope this addresses your concerns, and we’d be happy to discuss further if you have any additional feedback.", "claims_and_evidence": "I find that largely the claims about the experimental evaluation seem to be backed-up by the data. I do have some issues with the presentation of some of the data and the apparent conclusions that are drawn from it. I also feel that the paper may be missing some relevant literature, and therefore maybe also may be missing some SOTA in its evaluation. See comments below.", "methods_and_evaluation_criteria": "Based on the main text, I do not understand how the benchmark instances were selected for the experiment. I cannot find a URL to download the instances, or a reference to which instances were used, exactly. I have no idea what \"50 models over binary variables are kept.\" means in this context?\n\nAs I understand it, the benchmarks are created by somehow Frankensteining probabilistic constraints and SAT formulae together, but it is not clear to me how.\n\nI do like that the description of the used solvers is finally made quite explicit in Section 5.1.", "theoretical_claims": "There is a lemma, with a sketch of the proof. I'm not sure that a lemma is needed here. I find that it is phrased somewhat awkwardly (\"equality *can* be achieved\"? so sometimes it isn't?), and I feel like it does not add much compared to the existing (cited) literature on computing probabilities with arithmetic circuits. Hence, in my opinion this lemma does not add much. I would rather want to see the space it takes up now used to discuss more of the existing literature, or to clarify certain parts of the implementation or empirical evaluation (see also my notes elsewhere in this review on those topics).", "experimental_designs_or_analyses": "I find some of the claims insufficiently supported, in part because I find the way in which they are presented somewhat misleading. \n\nAn example is Figure 3. Its caption claims that \"Koco-SMC solves 80% of SMC problems in 20 ... \". However: as I understand the text, the figure shows the result for one problem (\"specific combination (3-color-5x5.cnf with smokers_10,uai)\", the meaning of which is also unclear to me) for different thresholds $q$. This implies to me that the problem structure (and thus the compiled probabilistic circuit) remains the same. As I understand it, the experiments show running time including the compilation time. Given that compilation time can certainly vary quite a lot from instance to instance (and are independent of threshold $q$), I find that presenting those times for just one problem instance (for varying $q$) a bit reductive. Furthermore, the claim that \"our method requires significantly less time across most instances\" does not seem to be backed up by any statistical tests that would demonstrate statistical significance, and it is not clear to me what this sentence even means (less time than what? what does \"across most instances\" mean?).\n\nI do think that reading Appendix C in detail would inspire trust in the quality of the empirical evaluation. However, my above comments on how I find the claims related to Figure 3 somewhat misleading, stands.", "relation_to_broader_scientific_literature": "As I understand it, the main contribution improves on the reported state of the art by learning conflicts directly from the probabilistic constraints, instead of alternating between a SAT solver and a solver for probabilistic inference. In my opinion, the paper misses some of the relevant literature, see remarks below.", "essential_references_not_discussed": "The reference for `CNFgen` is missing in the main text of the paper (and it only has a footnote in the appendix).\n\nIn my opinion, this paper should mention prior work on reasoning over constraints on the success probability of a literal-weighted CNF formula, and on the computation of upper and lower bound on the weighted model count of such a formula.\n\nThe following two works come from a line of work that presents algorithms for optimisation problems that require solving a constraint $C$ of the form $C := \\text{Pr}(F(X,Y)) \\bowtie \\theta$, where $F(X,Y)$ represents a CNF on decision variables $X$ and random variables $Y$, where $0 < \\theta \\leq 1$ is a threshold on the success probability, and $\\bowtie \\in \\{\\leq, \\geq\\}$. They leverage existing MILP and CP technology to aid in branching, propagation and conflict learning, as well as creating a propagation algorithm specifically for probabilistic constraints on arithmetic circuits, allowing for the stochastic constraint to be combined with other constraints. Since they allow for multiple constraints of the above form to be added, and are similar in terms of approach (knowledge compilation, CNF, etc), I feel like they are close enough to the contents of this paper to merit at least a mention in the related work section, but probably a more detailed discussion or comparison:\n\nA. L. D. Latour, B. Babaki, A. Dries, A. Kimmig, G. Van den Broeck, and S. Nijssen, ‘Combining stochastic constraint optimization and probabilistic programming — from knowledge compilation to constraint solving’, in _Proceedings of the 23rd international conference on principles and practice of constraint programming (CP 2017)_, in Lecture notes in computer science, vol. 10416. Springer, 2017, pp. 495–511.\n\nA. L. D. Latour, B. Babaki, and S. Nijssen, ‘Stochastic Constraint Propagation for Mining Probabilistic Networks’, in _Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence_, Macao, China: International Joint Conferences on Artificial Intelligence Organization, Aug. 2019, pp. 1137–1145. doi: [10.24963/ijcai.2019/159](https://doi.org/10.24963/ijcai.2019/159).\n\nThe following work studies the use of knowledge compilation to derive lower and upper bounds on the success probability of a literal-weighted input Horn formula. Despite the title mentioning approximation guarantees, I believe the methods provided in this work also provide true weighted model counts. Given that the proposed work puts a lot of emphasis on the bounds computation, I feel that this literature should probably be mentioned:\n\nA. Dubray, P. Schaus, and S. Nijssen, ‘Anytime Weighted Model Counting with Approximation Guarantees for Probabilistic Inference’, presented at the International Conference on Principles and Practice of Constraint Programming (CP), 2024. doi: [10.4230/LIPIcs.CP.2024.10](https://doi.org/10.4230/LIPIcs.CP.2024.10).\n\nIn the same spirit I think this work could merit a mention, since it concerns satisfiability modulo counting the number of solutions of a set of mixed-integer constraints, again keeping track of lower and upper bounds:\n\nC. Ge and A. Biere, ‘Improved Bounds of Integer Solution Counts via Volume and Extending to Mixed-Integer Linear Constraints’, presented at the International Conference on Principles and Practice of Constraint Programming (CP), 2024. doi: [10.4230/LIPIcs.CP.2024.13](https://doi.org/10.4230/LIPIcs.CP.2024.13).\n\nFinally, the following work also focuses on knowledge compilation for lower and upper bounds on the success probability of a literal-weighted input CNF, certifying the correctness of those bounds. This bit of literature is maybe a bit further from the contents of the proposed work, but I believe that it might still merit a mention:\n\nC. Cheng, Y.-R. Luo, and J.-H. R. Jiang, ‘Knowledge Compilation for Incremental and Checkable Stochastic Boolean Satisfiability’, presented at the Thirty-Third International Joint Conference on Artificial Intelligence, Aug. 2024, pp. 1862–1872. doi: [10.24963/ijcai.2024/206](https://doi.org/10.24963/ijcai.2024/206).\n\nI also find it strange that [Choi et al., 2022] is used as the reference for Smooth & Decomposability. Why not  cite \n\nA. Darwiche, ‘On the Tractable Counting of Theory Models and its Application to Truth Maintenance and Belief Revision’, Journal of Applied Non-Classical Logics, vol. 11, no. 1–2, pp. 11–34, Jan. 2001, doi: 10.3166/jancl.11.11-34.\n\nfor smoothness and\n\nA. Darwiche, ‘Decomposable negation normal form’, _J. ACM_, vol. 48, no. 4, pp. 608–647, Jul. 2001, doi: [10.1145/502090.502091](https://doi.org/10.1145/502090.502091).\n\nA. Darwiche, ‘Compiling knowledge into decomposable negation normal form’, in _Proceedings of the sixteenth international joint conference on artificial intelligence, IJCAI 99, Stockholm, Sweden, july 31 - august 6, 1999. 2 volumes, 1450 pages_, T. Dean, Ed., Morgan Kaufmann, 1999, pp. 284–289. [Online]. Available: [http://ijcai.org/Proceedings/99-1/Papers/042.pdf](http://ijcai.org/Proceedings/99-1/Papers/042.pdf)\n\nfor decomposability? Or maybe the classic\n\nA. Darwiche and P. Marquis, ‘A Knowledge Compilation Map’, _Journal of Artificial Intelligence Research_, vol. 17, pp. 229–264, Sep. 2002, doi: [10.1613/jair.989](https://doi.org/10.1613/jair.989)\n\n?\n\nIf the papers must cite Choi et al. 2022, then please fix the currently incorrect representation of Guy Van den Broeck's name? It's rendered correctly in [Kisa et al., 2014].\n\nI find in general that the bibliography is very sloppy. [Darwiche 1999] and [Darwiche 2002] have \"Citeseer\" in their bibliography entries. The reference for [Shet et al. 2023] is a preprint, even though that work also seems to have a published version. There is some weirdness going on in the pdf where there are a lot of instances of empty space hyperlinking to the bibliography entry for [Li et al., 2024], which itself does not list page numbers. A lot of titles are rendered incorrectly, with letters that should be in uppercase being rendered as lower-case, instead. Furthermore, some items use abbreviated venue titles, while others write them out fully.", "other_strengths_and_weaknesses": "I really like the detailed case studies that are described in the paper. I also want to compliment the authors on their efforts to make the line graphs b+w printer-friendly. The paper contains few typos, and I find that it reads well in general.", "other_comments_or_suggestions": "lines 47-48: I'm a bit surprised to find only references to workshops here, not to actual literature, except for Sheth et al 2023, which is a reference to a preprint even though a published version of that same work is also available.\n- Figure 2: poor formatting. Subfigures are not actually formatted as such, which results in a mismatch of fonts and an inability to search the figure for text.\n- line 80: I would really like to see references here so I know which \"Current exact SMC solvers\" the paper is referring to.\n- line 90: why is there a hyperlink to the [Li et al., 2024] entry in the bibliography at the start of this paragraph?\n- lines 102-103: what is meant with \"the largest dataset based on the UAI Competition benchmark\"? Could this be made more specific? As I understand it, each edition of UAI has a different benchmark set? It would be helpful if the paper was more transparent about which benchmarks were used exactly, and if there was a reference here.\n- lines 105-106: It would help my understanding if the paper explained the notation of $\\{f_i\\}^{K}_{i=1}$. What is $K$? What is $i$? Why does $i=1$ need to be there?\n- Lines 108-110: Is it essential that $|\\mathbf{x}| = |\\mathbf{y}_i| = |\\mathbf{z}_i|$? Why or why not? Are there any constraints on the value of $L$?\n- Line 143: \"Formally, PC\" missing indefinite article.\n- Line 157: \"The root node $r$ in the graph has no parent node.\" This confuses me. Seems obvious, right? Why does it need specifying?\n- The use of the word \"model\" is somewhat overloaded in the paper. It seems that in line line 137 it means \"a satisfying assignment to a Boolean satisfiability formula\", in line 158 it means \"a representation of a probability distribution\", and in line 315 it means \"problem instance\"? Do I understand this correctly? Could the writing be improved by being more explicit about this overloading?\n- Line 151: why is there no part (d)?\n- Line 155 \"An existing exact SMC\" solver: Which one? Can I have a reference? Or is the intended meaning \"any existing exact SMC solver that we are aware of\"?\n- Line 185: \"SMC solver\" missing \"s\".\n- Line 350: I find \"facing SMC problems\" a very awkward description of what is going on.\n- Line 352: Should this and the following $Q$s be $q$s, instead?\n- Line 355-356: I have no idea what \"specific combination (3-color-5x5.cnf with smokers_10,uai)\" means.\n- I will die on this hill: an x-axis is only an x-axis if it is labelled with \"x\". Otherwise, it is likely a horizontal axis, or a time axis, or in this case maybe s $q$-axis, or whatever is appropriate. Similar hill for y-axis.\n- There are spaces missing here and there after Figure numbers.", "questions_for_authors": "Q1. Can the authors please reflect on how their work relates to the work presented in [Latour et al., 2017], [Latour et al., 2019], and [Dubray et al., 2024] (see above)? As I currently understand the paper, I feel like these are relevant enough to be mentioned, or maybe even compared against. For now, this is a reason for me to recommend rejection.\n\nQ2. Can the authors please elaborate on their claim that \"Our method typically requires significantly less time across most instances.\"? As argued above, I find this claim, especially in the context of Fig 3 somewhat misleading. As I explained above, I do not know what it means, which for now also makes me less eager to recommend accepting the work.", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: This paper addresses the Satisfiability Modulo Counting (SMC) problem, which extends SAT by incorporating probabilistic constraints. The authors propose KOCO-SMC, an exact solver that uses probabilistic circuits to efficiently compute bounds for probability statements within a conflict-driven clause learning framework. Experimental results demonstrate that KOCO-SMC outperforms existing exact and approximate SMC solvers across various benchmarks.

The authors were largely positive about the paper. The sole negative reviewer did not further engage in the discussion which is taken as an indication of agreement to the other reviews. 

Hence I recommend accepting the paper.
Decision: Accept (poster)