Thank you for your valuable review and feedback, which have provided us with an opportunity to clarify and strengthen our work.

---

1. Main contribution clarification

Our main contribution is the proposal of an efficient exact solver for SMC problems, addressing a gap where existing solvers are either approximate or slow concatenation-based exact solvers. In the worst case, a concatenation-based exact solver would require enumerating almost all solutions before reaching an SAT/UNSAT conclusion.

Our pipeline is built on the CDCL framework, as we recognized that probabilistic constraints can be seamlessly integrated into CDCL-based SAT solvers as additional "probabilistic clauses."

---

2. Related work of the Upper-Lower Watch

Our idea is to use the upper and lower bounds of probabilities to avoid unnecessary searches. Similar ideas can be found in branch-and-bound, which maintains upper and lower bounds of the objective function to prune suboptimal branches of the search tree, and in alpha-beta pruning, which uses bounds on the evaluation of game states to eliminate branches in the game tree that cannot affect the final decision. We have included this in the related work section (Paragraph 3, Appendix A).

To make it a complete approach, we relate this bound monitoring to Marginal MAP inference and observe that probabilistic circuits with specific structures can enable efficient MMAP inference. These serve as the stepping stones of our approach.

---

We hope this response addresses the reviewer’s concerns and provides clarity on the contributions. Thank you again for your insightful feedback.

Thank you for raising the Stochastic SAT (SSAT) problems with a detailed explanation. We found the SSAT is highly relevant to our work. We would like to address your concerns as follows:

Summarized Message

SSAT solvers can only handle SMC problems with one Boolean constraint and one probabilistic constraint. They do not generalize to those with multiple probabilistic constraints. Empirically, state-of-the-art SSAT solvers assume independence among random variables. In experiments, our probabilistic constraints are from real-world Markov random fields with highly correlated variables, where SSAT cannot be applied. Thus the comparison in efficiency would be limited.

---

Detailed explanation for SSAT and SMC problems

---

1. SSAT Captures a subset of SMC instances:

The SMC problems with Boolean constraints and probabilistic constraints are outlined in Equation (1). In our experiments, we focused on a specific form of SMC problem: $\phi(X) \wedge \left(\sum_Y f(X, Y) > \text{threshold}\right)$, where X and Y are two sets of Boolean variables, $\phi(X)$ is a Boolean formula, and $\sum_Y f(X, Y)$ is a weighted model counting term. The goal is to determine whether there exists an assignment to X that satisfies the formula.

SSAT solvers can address this specific case of SMC problems by leveraging their formulation of existential and randomized quantifiers. For the suggested SSAT problem: Exists(X), Random(Y), $\phi(X) \wedge f(X, Y)$, where f(X, Y) is a weighted Boolean formula. Using state-of-the-art SSAT solvers, one could solve: $\arg \max_X \sum_Y f(X, Y)$, where X satisfies $\phi(X)$. Then we could equivalently solve the SMC problem mentioned before.

SSAT solvers can efficiently handle this case of SMC problems. Yet, their applicability is limited with multiple probabilistic constraints. A comparison of the special case of SMC problems (with a single probabilistic constraint and independent variables) would provide only limited insight and would not generalize to the full class of SMC problems.

---

2. SSAT and SMC have a different specialization.

• SSAT excels at handling problems with sequences of existential and randomized variables, such as those involving max-sum-max-... operations. This is beyond the scope of our SMC formulation.

• SMC is suited to handling multiple probabilistic constraints simultaneously. For example: consider an SMC problem involving two probabilistic constraints $\phi(X) \wedge \left(\sum_Y f_1(X, Y) > q_1\right) \wedge \left(\sum_Z f_2(X, Z) > q_2\right)$. This type of scenario is common in real-world problems that SMC is designed to model. Modeling such problems as a max-sum problem would require optimizing multiple objectives over shared variables, which SSAT solvers cannot directly address.

---

3. The assumption on probability in SSAT is too rigid in SMC problem setting.

A key limitation of SSAT solvers is their assumption of independence among all random variables $x_1, \ldots, x_n$, i.e., $P(x_1, \ldots, x_n) = P(x_1)P(x_2) \cdots P(x_n)$. This limits their applicability in scenarios where the joint distribution is complex. In contrast, KOCO-SMC uses challenging data with highly correlated variables modeled by Markov random fields. If we were to conduct experiments on these specific cases, we intuitively expect SSAT solvers to outperform KOCO-SMC due to the rich body of work and the many advances in the SSAT domain. However, these results would not reflect the broader applicability of KOCO-SMC to more general SMC problems.

---

Thank you again for bringing up SSAT, as it represents an important and relevant line of work that we had not addressed. We have included a more detailed discussion of SSAT and its relationship to SMC in our revised manuscript (in Appendix A). We hope this addresses your concerns and look forward to any additional feedback you might have.

We deeply appreciate your detailed review and for pointing out the issue in the Lemma regarding MMAP inference. Your observations are invaluable, and we address your concerns as follows:

---

1. Clarification of the Requirement for Q-Deterministic Circuits

You are correct. To guarantee exact upper and lower bound monitoring leveraging tractable MMAP inference, the probabilistic circuit must be Q-deterministic. We acknowledge that the previous version of our paper did not address this correctly. We have incorporated your comments and corrected the manuscript.

The SMC problems we address can be represented as $\phi(x_1, \ldots, x_n) \wedge \left(\sum_y f(x_1, \ldots, x_n, y) > \text{threshold}\right)$, where $\phi(x_1, \ldots, x_n)$ is a Boolean formula, and $\sum_y f$ is a weighted model counting term. Denoting the set of decision variables $x_1, \ldots, x_n$ as the set $Q$, inferring the exact upper and lower bounds for $\sum_y f$ corresponds to solving an MMAP problem. This can be achieved by compiling the function $f$ into a Q-deterministic (smooth and decomposable) probabilistic circuit.

During the solving process, even if some decision variables are assigned as the “evidence variable”, MMAP for the remaining unassigned variables remains tractable, as discussed in Section 2.2 of [Choi et al., 2022].

However, in terms of experiments, we could not ensure that all our data could be compiled into Q-deterministic circuits due to limited control of the knowledge compiler. We have addressed this in the limitations section (Page 14, line 712). If Q-determinism could be guaranteed, the performance would likely improve further, due to the more accurate bound monitoring.

---

2. Future extension: A Relaxed Upper-Lower watch without Q-Determinism

Compiling distributions into Q-deterministic circuits can require extensive time or space (exceeding 20 GB in our experiments). To address this, we propose a relaxed version of ULW for broader applicability. The only modification lies in the updating rule for sum nodes. Specifically, when monitoring the upper bound at each sum node, instead of computing the maximum of its child nodes, we calculate the sum of their upper bounds.

Intuitively, this guarantees that the value evaluated at each node is no less than the value after a full variable assignment, ensuring the validity of the upper and lower bounds. This approach relies only on decomposability and smoothness, eliminating the need for determinism. It may result in arbitrarily loose bounds so is not ideal for analysis. Due to time constraints, we will explore this relaxed version in greater detail with experimental results in the next iteration of our work.

---

Thank you again for your feedback. We hope this clarifies our responses and addresses your concerns. Please let us know if you have other concerns.

Thank you for your detailed comments and for giving us the opportunity to further clarify our paper.

1. The unclarity of current notation

We will carefully revise the notations to ensure a clearer presentation in the next version. During the discussion period, we will keep it the same, because the changes in notation may cause misunderstandings for other reviewers.

---

2. Is there a conflict clause extracted from a probabilistic constraint?

If the model counter identifies a solution that does not satisfy a probabilistic constraint, it adds a trivial clause negating the current assignment to the Boolean formula to avoid the same conflict. For example, if the Boolean SAT solver proposes the solution $(x_1 = \text{True}, x_2 = \text{False})$ and the model counter determines it is UNSAT, we add the clause $(\neg x_1 \vee x_2)$ to the Boolean formula.

---

3. how to define “solved” in Figure 3 for UNSAT instances?

For our KOCO-SMC, which is an exact solver, "solved" means that it determines the problem is UNSAT. For approximate solvers, "solved" means they successfully conclude UNSAT in at least one of five runs. In both cases, timeout instances are treated as UNKNOWN.

---

4. What is the benchmark in Figure 5?

In Figure 5, we compare our KOCO-SMC with a variant that does not utilize the Upper-Lower Watch mechanism. In this variant, upper and lower bounds are not monitored for early conflict detection; instead, counting is performed only after all variables have been assigned. In the left figure, we illustrate the effect of varying the threshold by selecting a single SMC problem that remains solvable within 3 hours across different threshold values. Noted that “solvable” refers to reaching the correct answer (either SAT or UNSAT) in the given time.

---

5. Minor mistake

We have revised the text around line 233.

---

We hope the reviewer’s concerns are addressed and they will consider updating their score. We welcome further discussions.

Thank you for your valuable feedback. We collect the response to address your concerns as follows.

1. For Limited Problem Scope

The SMC framework is inherently general and capable of modeling a wide range of decision-making problems involving stochasticity. In the experimental section, we used instances from the UAI competition, which are from domains such as graph coloring, medical diagnosis, and family lineage analysis. We tried our best to cover as many application domains as possible.

Furthermore, we demonstrated step-by-step how real-world cases can be formulated as SMC problems, such as route planning (Figure 2), supply chain design (Appendix C.4), and package delivery (Appendix C.5). These problems are then efficiently solved using KOCO-SMC. Our paper proposes an efficient exact solver for SMC problems, which can be applied to any SMC problem formulated as described in Equation (1).

We would be delighted if you could suggest any additional relevant applications for the SMC framework.

---

2. For Complexity Analysis

The worst-case complexity of KOCO-SMC remains NP^PP, as finding an exact solution for SMC problems inherently falls into this complexity class. The complexity class NP^PP refers to problems solvable by an NP machine with access to an oracle for a PP (Probabilistic Polynomial-Time) problem. Our innovation lies in improving practical efficiency through pre-compilation and conflict detection rather than altering the theoretical complexity. We used experiments on synthetic data in Section 4.2 to demonstrate the efficiency.

---

3. Comparison with Baseline Exact Solvers

SAT-exact solvers require repeatedly finding a complete variable assignment of the Boolean part and verifying the model counting, which necessitates exploring every branch of variable assignments. In contrast, KOCO-SMC sequentially assigns variables one by one, detecting conflicts early and pruning unnecessary branches in the search space, significantly improving efficiency.

We illustrate this with the example shown from line 221 to line 230. Baseline first computes an all-variable assignment, $x_1 = x_2 = b_1 = True, x_3=x_4=b_2=False$. Then the PC part computes the summation, which results in UNSAT. Our method immediately raises conflict given partial assignment $x_1 = `True`$, which saves time by avoiding assigning values to the rest variables. Because the PC part is UNSAT, i..e.,$P(x_1 = `True`, x_2, x_3, x_4)=0.1<0.5$, when $x_1 = `True`$.

---

Thank you again for your feedback. We hope this clarifies our responses and addresses your concerns. Please let us know if you have other concerns.