Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits

Thank you very much for the detailed review. We will address your concerns and questions in the following reply.

---

Q1: Related works

We 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:

1. Relavance to upper and lower bound computation: Link

2. Relavance to Stochastic Constraint Optimization Problems: Link

3. Modified citations for PCs: Link

---

Q2: SMC problem definition

1. What is {$f_i$}$_{i=1}^K$?

It means a set of functions {$f_1,\ldots, f_K$}. K is the number of total probabilistic constraints.

2. Is it essential that $|x|=|y_i|=|z_i|$?

No, 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.

Link to the revised version

---

Q3: Lemma 1 seems redundant

Our 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.

---

Q4: Experiments

1. Dataset details

Each SMC instance consists of a CNF file for the Boolean SAT constraint, a UAI file for the probabilistic constraint, and a threshold value.

The 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:

https://anonymous.4open.science/r/anonym_koco_smc-61FD/data/

The 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

For the compiled probabilistic circuit files, most of them are excessively large (>1 GB), so we didn’t include them in the repository for now.

2. Detailed settings for Figure 3

In 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.

3. Regarding 'our method requires significantly less time across most instances'

According 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.

---

Q5: Clarification on “Current exact SMC solvers (line 80)” and "An existing exact SMC solver (line 155)"

We realize that these phrases are misleading as they suggest the existence of an actual tool. To clarify, we have revised the text accordingly.

Since there is no general exact SMC solver, solving SMC problems exactly requires combining tools from SAT solving and probabilistic inference.

---

Q6: Other issues

1. On line 90, we didn’t see the hyperlink in the PDF. We would appreciate it if you could provide more context.

2. Bibliography issue. We've carefully revised the bibliography. Link to new Bibliography

3. Language and writing issues: We have cleared up the improper use of language errors according to your suggestions.

4. Line 157: "The root node in the graph has no parent node." It is changed to:

   “The root node is the final output of the probabilistic circuit. It represents the overall probability distribution over the variables.”

5. The use of the word "model" is somewhat overloaded in lines 137, 158, and 315. We have cleaned up the usage of the word “model” in these lines for clarity.

6. The use of the x-axis and y-axis for Figure 3 caption. We have cleaned up the related text. It should be:

   Link to the revised Figure 3

---

Thank 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.

Thank you very much for your review and suggestions.

---

Q1: Beyond conflict detection, is KOCO-SMC able to derive propagations from probabilistic inference constraints?

This 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.

The 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.

---

Q2: Add Citations

We have added a citation to CaDiCaL and included additional references in the "Probabilistic Inference and Model Counting" section:

[1] Chavira, Mark, and Adnan Darwiche. "On probabilistic inference by weighted model counting." Artificial Intelligence 172.6-7 (2008): 772-799.

[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.

[3] Gomes, Carla P., Ashish Sabharwal, and Bart Selman. "Model counting: A new strategy for obtaining good bounds." AAAI. Vol. 6, 2006.

[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.

---

Q3: Writing typos

We have added the missing word "into" at line 200.

---

Q4: Ethical Review Flag

We 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.

---

We 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.

Thank you for your careful review and for raising valuable questions.

---

Q1: Why is Koco-SMC More Efficient?

In general, KOCO-SMC saves time by detecting conflicts early using partial variable assignments, whereas baseline solvers require full variable assignments.

• 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.
• 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.

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.

---

Q2: Clarification of the Problem Formulation

(1) What are the differences between variables x, y, and z in Equations (1) and (2)?

The variables x denote the decision variables, while y and z are latent variables that are marginalized out.

(2) It is unclear what the given probabilities are in Equations (1) and (2).

The 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.

For KOCO-SMC, we specifically compiles probability distributions into probabilistic circuits because PCs have structural properties that significantly benefit our ULW algorithm.

(3) I don't understand the initialization as described at the end of Section 3 due to the previous two confusions.

The initialization mentioned in line 226 refers to the computation of the initial upper and lower probability bounds within the PC.

(4) How is the value 0.1 at line 165 obtained?

This 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.

Specifically, 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.

---

Q3: Answers to Specific Questions

• What is the time complexity required to add the learned clauses to PCs?

  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.

• What if neither bound condition is met? Would it result in approximate solutions rather than an exact solver?

  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.

  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.

---

Q4: Other Issue

Thank you for suggesting the WMC algorithms based on CDCL. We have now incorporated these references and other relevant related work into the paper.

---

Thank 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.

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.

---

Q1. Main Contribution

We propose an integrated exact SMC solver, addressing the existing gap in this research community, which previously only had approximate solvers available. Our method achieves higher computational efficiency compared to vanilla exact solvers by utilizing our proposed ULW algorithm. Vanilla 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.

---

Q2. Novelty of Our ULW Algorithm

Our 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:

1. Relevance between ULW and Upper and Lower Bound Computation:

Our 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.

2. Relevance between SMC and Stochastic Constraint Optimization Problems:

Stochastic 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.

The related works above bridge the connection to the existing theoretical foundations.

---

Thank 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.