# solving_stochastic_boolean_satisfiability_under_randomexist_quantification__beb9975a.pdf

Solving Stochastic Boolean Satisﬁability under Random-Exist Quantiﬁcation

Nian-Ze Lee , Yen-Shi Wang , and Jie-Hong R. Jiang ,

Graduate Institute of Electronics Engineering, Department of Electrical Engineering National Taiwan University, Taipei, Taiwan {d04943019, b03901116, jhjiang}@ntu.edu.tw

Stochastic Boolean Satisﬁability (SSAT) is a powerful formalism to represent computational problems with uncertainty, such as belief network inference and propositional probabilistic planning. Solving SSAT formulas lies in the PSPACEcomplete complexity class same as solving Quantiﬁed Boolean Formulas (QBFs). While many endeavors have been made to enhance QBF solving in recent years, SSAT has drawn relatively less attention. This paper focuses on random-exist quantiﬁed SSAT formulas, and proposes an algorithm combining modern satisﬁability (SAT) techniques and model counting to improve computational efﬁciency. Unlike prior exact SSAT algorithms, the proposed method can be easily modiﬁed to solve approximate SSAT by deriving upper and lower bounds of satisfying probability. Experimental results show that our method outperforms the stateof-the-art algorithm on random k-CNF and AIrelated formulas in both runtime and memory usage, and has effective application to approximate SSAT on VLSI circuit benchmarks.

1 Introduction

First formulated in [Papadimitriou, 1985], stochastic Boolean satisﬁability (SSAT) was described as a game against nature. Probabilistic factors are introduced into the world of Boolean logic through the creation of the randomized quantiﬁer. A Boolean variable randomly quantiﬁed with probability p has a probability p of evaluating to TRUE. Exploiting randomized quantiﬁers, SSAT is capable of modeling a variety of computational problems inherent with uncertainty [Hnich et al., 2011], such as propositional probabilistic planning, belief network inference, and trust management [Majercik, 2009]. Recently, it has also been applied to the formal veriﬁcation of probabilistic circuits [Lee and Jiang, 2014]. From computational complexity point of view, SSAT lies in the PSPACEcomplete complexity class, same as quantiﬁed Boolean satisﬁability (QSAT). Therefore, developing good algorithms for SSAT not only brings practical beneﬁts for real-world applications, but also is of theoretical interest.

Among the prior efforts made to approach SSAT, most of them are based on Davis-Putnam-Logemann-Loveland (DPLL) search [Davis et al., 1962]. MAXPLAN [Majercik and Littman, 1998] improves DPLL-based search by considering pure literal, unit propagation, and subproblem memorization. ZANDER [Majercik and Littman, 2003] incorporates several threshold pruning heuristics to reduce the search space. DC-SSAT [Majercik and Boots, 2005] divides the SSAT formulas into many subproblems and conquer them separately. The solution of the original formula is then constructed on top of the solutions of subproblems. Approximate SSAT solving, which derives upper or lower bounds of satisfying probability of an SSAT formula instead of solving it exactly, was investigated in [Majercik, 2007]. Resolution for SSAT has also been addressed in [Teige and Fr anzle, 2010]. Model counting algorithms are under active development in recent years. In addition to exact model counting [Sang et al., 2004; 2005a], approximate model counting [Gomes et al., 2006; 2007; Chakraborty et al., 2016] has been addressed to improve scalability by relaxing exactness. In this work, exact or approximate model counting is exploited as an ingredient for SSAT solving. On the other hand, projected model counting [Aziz et al., 2015], which computes the numbers of satisfying assignments projected on a subset of original variables, is subsumed by random-exist quantiﬁed SSAT. Therefore, our proposed method can be applied to solve projected model counting. In contrast to the prior DPLL-based SSAT algorithms with pruning heuristics and subproblem memorization, our goal is to take advantage of modern SAT solvers [E en and S orensson, 2003a; 2003b] and model counters as a blackbox engine for solving SSAT. To the best of our knowledge, this work is the ﬁrst attempt to directly use a SAT solver as a plug-in engine for SSAT solving. In this paper, we focus on the random-exist quantiﬁed SSAT formula of the form Φ =

X Y.φ, which is the counterpart of the forall-exist quantiﬁed QBF formula. The random-exist quantiﬁed SSAT has applications in belief network inference [Cooper, 1990; Bacchus et al., 2003], probabilistic planning, and probabilistic circuit veriﬁcation [Lee and Jiang, 2014]. In addition to SAT solving, we incorporate weighted model counting, which has been widely used in probabilistic inference [Sang et al., 2005b; Chavira and Darwiche, 2008], in the proposed algorithm to tackle randomized quantiﬁers. The proposed al-

Proceedings of the Twenty-Sixth International Joint Conference on Artiﬁcial Intelligence (IJCAI-17)

gorithm uses the SAT solver and model counter in a standalone manner, leaving the internal structures of these solvers intact. Due to the stand-alone usage of these solvers, the proposed algorithm may directly beneﬁt from the advancement of the solvers without any modiﬁcation. Moreover, unlike previous DPLL-based methods, the proposed algorithm can be easily modiﬁed to solve approximate SSAT by deriving upper and lower bounds of satisfying probability. To evaluate the proposed algorithm, a prototype program was implemented and experimented with random k-CNF formulas, strategic companies [Cadoli et al., 1997] formulas arising from the artiﬁcial intelligence (AI) domain, and benchmarks from analysis of very-large-scale integration (VLSI) circuits. Our method outperforms the state-of-the-art algorithm on random k-CNF and strategic companies formulas in both runtime and memory consumption, and is capable of solving approximate SSAT on circuit benchmarks while the state-of-the-art method fails to compute the exact satisfying probability.

2 Preliminaries

Let B = { , }, where and denote logic TRUE and FALSE. A literal is a Boolean variable or its negation. A clause (resp. cube) is a disjunction (resp. conjunction) of literals. A conjunctive normal form (CNF) formula is a conjunction of clauses. A Boolean formula φ over variables X = {x1, . . . , xn} induces a Boolean function mapping from Bn to B. The set of Boolean variables appearing in a Boolean formula φ is denoted as vars(φ). An assignment τ on variables X vars(φ) of formula φ is a mapping from X to B. An assignment τ is called a complete assignment on vars(φ) if X = vars(φ); otherwise, it is called a partial assignment on vars(φ). The formula of φ induced under the assignment τ on X vars(φ) is obtained by substituting every appearance of x X in φ by τ(x), and is denoted as φ|τ. A complete assignment τ is called a satisfying (resp. an unsatisfying) (complete) assignment for φ if φ|τ = (resp. φ|τ = ). Similarly, a partial assignment τ + on X vars(φ) for φ is called a satisfying (resp. an unsatisfying) (partial) assignment on vars(φ) if for some (resp. every) assignment µ on vars(φ) \ X, φ valuates to (resp. ) under the complete assignment obtained by combining τ and µ. In the sequel, we alternatively represent an assignment τ for φ as a cube. A cube is called a minterm when it corresponds to a complete assignment with respect to a speciﬁed set of variables. A Boolean formula φ is called satisﬁable if there exists a satisfying complete assignment for φ. We write SAT(φ) = to denote φ is satisﬁable. A satisfying assignment of φ is also called a model of φ, denoted by φ.model. On the other hand, if φ has no satisfying assignment, it is unsatisﬁable and written as SAT(φ) = .

2.1 Generalization of SAT or UNSAT Assignments

Consider a CNF formula φ(X, Y ), where X and Y are two disjoint sets of Boolean variables. Given an assignment τ on X, if φ(X, Y )|τ is satisﬁable (resp. unsatisﬁable), τ is called a SAT (resp. an UNSAT) minterm of φ on X. The generalization process of a SAT or an UNSAT minterm τ aims at

expanding it to a cube τ +, while maintaining the satisﬁability of φ(X, Y )|τ + the same as φ(X, Y )|τ.

Example 1 Consider formula φ(x1, x2, y1, y2) = x1 ( x2 y1 y2). The assignment τ = x1x2 on X, i.e., τ(x1) = , τ(x2) = , is a satisfying assignment, or a SAT minterm, of φ on X as φ|τ is satisﬁable by assignment µ = y1y2. On the other hand, the partial assignment τ + = x1, i.e., τ +(x1) = , is an unsatisfying partial assignment, or an UNSAT cube, of φ as φ|τ + is unsatisﬁable.

Minimum Satisfying Assignment For a CNF formula φ(X, Y ), let τ be a SAT minterm on X and let µ be a satisfying assignment for φ(X, Y )|τ on Y . To generalize τ into a cube, one can ﬁnd a subset of literals from τ and µ that are able to satisfy all clauses in φ while the number of literals taken from τ is as few as possible. If some literals in τ are irrelevant to the satisﬁability, they can be dropped from τ, thus expanding τ to a SAT cube τ +. If in the SAT cube τ +, the number of literals taking from τ is minimized, τ + is called the minimum satisfying assignment. The process of ﬁnding the minimum satisfying assignment is also known as ﬁnding the minimum hitting set.

Minimum Conﬂicting Assignment Given an UNSAT minterm τ of a CNF formula φ, modern SAT solvers, such as Minisat [E en and S orensson, 2003a; 2003b], are able to analyze the reason of unsatisﬁability, which is represented as a conjunction of literals in τ causing the conﬂict. If some literals in τ are irrelevant to the conﬂict, they are dropped from τ, thus expanding τ to an UNSAT cube τ +. If the number of literals in the UNSAT cube τ + is minimized, τ + is called the minimum conﬂicting assignment. The process of ﬁnding the minimum conﬂicting assignment is also known as ﬁnding the minimum UNSAT core.

2.2 Model Counting Given a CNF formula φ, the model counting problem ﬁnds the number of satisfying assignments of φ. In its weighted version, a weight function ω maps each Boolean variable x vars(φ) to a weight ω(x) [0, 1], which represents Pr[x = ]. The weight of a negative literal x is deﬁned to be 1 ω(x). The weight of an assignment equals the product of the weights of its individual literals. The weight of a Boolean formula equals the summation of weights of its satisfying assignments. There are two categories of model counting algorithms: Exact model counting computes the precise number of satisfying assignments of a formula; approximate model counting computes the upper or lower bounds of the number of satisfying assignments of a formula with some conﬁdence level.

2.3 Stochastic Boolean Satisﬁability A stochastic Boolean satisﬁability (SSAT) formula is of the form Φ = Q1x1 . . . Qnxn.φ,

where Qi { ,

pi} and φ is a quantiﬁer-free Boolean formula. In addition to the existential quantiﬁer , the randomized quantiﬁer

pi on xi assigns a probability pi [0, 1] for xi to be true. The quantiﬁer part is called the preﬁx, and the

Proceedings of the Twenty-Sixth International Joint Conference on Artiﬁcial Intelligence (IJCAI-17)

Boolean formula is called the matrix. Given an SSAT formula Φ, let v be the outermost variable in the preﬁx. The satisfying probability of Φ can be computed by the following rules. a) Pr[ ] = 1, b) Pr[ ] = 0, c) Pr[Φ] = max{Pr[Φ| v], Pr[Φ|v]}, if v is existentially quantiﬁed, d) Pr[Φ] = (1 p)Pr[Φ| v] + p Pr[Φ|v], if v is randomly quantiﬁed by

p, where Φ| v and Φ|v denote the SSAT formulas derived by eliminating the outermost quantiﬁer of v by substituting the value of v in the matrix with and , respectively. In this paper, we aims at solving the random-exist quantiﬁed SSAT formula of the form Φ =

X Y.φ(X, Y ), where X = {x1, . . . , xn} and Y = {y1, . . . , ym} are two disjoint sets of Boolean variables.

3 Solving Random-Exist SSAT Consider a random-exist quantiﬁed SSAT formula Φ =

X Y.φ(X, Y ). The satisfying probability of Φ equals the summation of weight of all SAT minterms on X, or, equivalently, 1 minus the summation of weight of all UNSAT minterms on X. To identify an assignment τ on X as a SAT or an UNSAT minterm, it sufﬁces to check whether φ(X, Y )|τ is satisﬁable or not. A naive solution to computing the satisfying probability of Φ exhaustively examines all assignments on X, classiﬁes them as SAT or UNSAT minterms, and aggregates the weight of collected minterms. The above naive solution can be improved by exploiting the minterm-generalization techniques discussed in Section 2.1. For instance, in Example 1, τ = x1x2 x3 is a SAT minterm for φ(x1, x2, x3) = x1 (x2 x3). Observe that φ(x1, x2, x3) is satisﬁable under the partial assignment τ + = x1x2. In other words, the SAT minterm τ can be generalized into the SAT cube τ +, which contains two minterms. Through the generalization analysis, more than one minterm can be collected in a single SAT solving run, enhancing the efﬁciency of the enumeration of all possible assignments on X. As will be shown in Section 4, the minterm-generalization techniques are essential to the efﬁciency of the proposed method. However, the weight of each collected cubes cannot be summed up directly due to the potential non-disjointness between the generalized cubes. This difﬁculty can be overcome by applying weighted model counting to evaluate the weight of the collected cubes. The above idea gives rise to the proposed algorithm, formalized in Figure 1, to evaluate Φ =

X Y.φ(X, Y ). The proposed algorithm works as follows. First assume the runtime limit TO to be inﬁnity, while the effect of imposing a runtime limit on Solve RESSAT will be explained in Section 3.4. Two SAT solvers are used in Solve RESSAT. In addition to the SAT solver holding the matrix CNF φ(X, Y ), the other SAT solver ψ(X), called the selector in the sequel, is initialized with any empty set of clauses. The selector ψ(X) is in charge of selecting an assignment τ on X. After τ is chosen, the matrix solver φ(X, Y ) will check whether or not φ(X, Y )|τ is satisﬁable. Depending on the satisﬁability of φ(X, Y )|τ, the

Solve RESSAT input: Φ =

X Y.φ(X, Y ) and a runtime limit TO output: Upper and lower bounds (PU, PL) of satisfying prob. begin 01 ψ(X) := ; 02 C := ; 03 C := ; 04 while SAT(ψ) = runtime < TO 05 τ := ψ.model; 06 if SAT(φ|τ) = 07 τ + := Minimal Satisfying(φ, τ); 08 C := C {τ +}; 09 else //SAT(φ|τ) = 10 τ + := Minimal Conﬂicting(φ, τ); 11 C := C {τ +}; 12 ψ := ψ τ +; 13 return (1 Compute Weight(C ), Compute Weight(C )); end

Figure 1: Algorithm: Solving random-exist quantiﬁed SSAT.

minterm τ is generalized into a cube by the subroutine Minimal Satisfying or Minimal Conﬂicting. Instead of ﬁnding the minimum satisfying or conﬂicting assignment, which is computationally expansive, we resort to ﬁnding a minimal satisfying or conﬂicting assignment, i.e., an assignment having no literals removable without affecting the (un)satisﬁability, to leverage the efﬁciency of UNSAT core computation for effective generalization. After τ is generalized to τ + and enlisted in C or C , the negation of τ +, which is a blocking clause, will be conjoined with ψ to prune the assignments contained by τ +. The above process is repeated until ψ becomes unsatisﬁable, which signiﬁes the Boolean space spanned by X has been exhaustively searched. The subroutine Compute Weight is then invoked to evaluate the weight of the collected cubes. The subroutines Minimal Conﬂicting, Minimal Satisfying, and Compute Weight are detailed below.

3.1 Minimal Satisfying Assignment Given a SAT minterm τ on X for φ(X, Y ), let µ be the satisfying assignment on Y for φ(X, Y ). The subroutine Minimal Satisfying generalizes τ to τ + via the following steps. a) Remove every clause C in φ(X, Y )|τ that contains some true literal in µ. b) For each literal l in τ, drop l and examine whether the rest of clauses remain satisﬁed by scanning these clauses and checking if each of them still contains some true literal. If the rest of clauses are all satisﬁed, discard l; otherwise, put l in τ +. After the above steps, the SAT minterm τ is generalized into a minimal satisfying assignment τ +.

3.2 Minimal Conﬂicting Assignment Let τ be an UNSAT minterm on X for φ(X, Y ). The analysis of unsatisﬁability can be done with a modern SAT solver (e.g., using analyze Final() in Minisat) to ﬁnd a conjunction of literals from τ responsible for the conﬂict. However, in general this conjunction of literals might not be minimal, meaning that some of the literals can be dropped. The

Proceedings of the Twenty-Sixth International Joint Conference on Artiﬁcial Intelligence (IJCAI-17)

subroutine Minimal Conﬂicting takes the conjunction of literals responsible for the conﬂict computed by a SAT solver and makes it minimal as follows. For each literal l in the conjunction, drop l and examine whether φ(X, Y ) remains unsatisﬁable by invoking a SAT call. If it is unsatisﬁable, discard l; otherwise, put l in τ +. After the above steps, the UNSAT minterm τ is generalized into a minimal conﬂicting assignment τ +.

3.3 Weight Computation The subroutine Compute Weight aggregates the weight of collected cubes by invoking a weighted model counter. Because the weighted model counter takes CNF formulas as input, Compute Weight ﬁrst negates each collected cube to turn it into a clause, and conjoins the resulting clauses into a CNF formula. As the CNF formula is the negation of the disjunction of the cubes, the weight of the cubes equals one minus the weight of the CNF formula, which is computed by a weighted model counter.

3.4 Modiﬁcation for Approximate SSAT The proposed algorithm can be easily modiﬁed to solve approximate SSAT, where upper and lower bounds of the satisfying probability of an SSAT formula are computed. Suppose Solve RESSAT is forced to terminate before the selector ψ becomes unsatisﬁable. The weights of the collected SAT and UNSAT cubes are still valid and can be aggregated by Compute Weight, and the resulted weights reﬂect the lower and upper bounds of the satisfying probability, respectively. The early termination can be triggered by imposing a runtime limit for Solve RESSAT. Compared to previous DPLL-based methods that branch on a single variable, the proposed algorithm considers all randomly quantiﬁed variables together and exploits the concept of SAT and UNSAT cubes over the Boolean space spanned by randomly quantiﬁed variables, making the intermediate collected SAT and UNSAT cubes convey useful information about the upper and lower bounds of the exact satisfying probability. As will be seen in our experiments over formulas arising from VLSI circuit analysis, the proposed algorithm is able to ﬁnd tight bounds even with a short time limit. Compared to the DPLL-based state-of-theart methods, which cannot be easily modiﬁed for approximate SSAT, the proposed method enjoys the ﬂexibility of solving SSAT approximately or exactly, depending on the imposed runtime constraint. We note that the proposed algorithm is more efﬁcient in memory consumption than previous DPLL-based algorithms. Prior DPLL-based algorithms mostly apply subproblem memorization to avoid repeated computation on the same subproblem. However, without special treatment, such memorization may result in rapid growth in memory usage. On the other hand, in the proposed algorithm, the numbers of collected cubes are greatly reduced by the aforementioned minterm generalization, which gives rise to the memory efﬁciency. In our empirical evaluation, the proposed algorithm consumed two orders of magnitude less memory than the state-of-the-art DPLL-based algorithm. The following example illustrates how Solve RESSAT solves a random-exist quantiﬁed SSAT formula.

Example 2 Consider the random-exist quantiﬁed SSAT formula Φ =

0.5r1r2r3 e1e2e3.φ, with φ consisting of clauses C1 : (r1 r2 e1) C2 : (r1 r3 e2) C3 : (r2 r3 e1 e2) C4 : (r3 e3) C5 : (r3 e3) At the beginning, the selector ψ(r1, r2, r3) is initialized to an empty set of clauses, and the sets C and C for collecting SAT and UNSAT cubes are empty. Suppose ψ ﬁrst selects the assignment τ0 = r1 r2 r3. Since φ|τ0 is unsatisﬁable (due to the conﬂict between C4 and C5), the subroutine Minimal Conﬂicting returns τ + 0 = r3, which is the minimal conﬂicting assignment responsible for this conﬂict. Note that this minimal conﬂicting assignment τ + 0 reﬂects an upper bound of 0.5 for the satisfying probability of Φ. The selector ψ is then strengthened through conjunction with the negation of τ + 0 to block the searched subspace. Next, suppose τ1 = r1 r2r3 is selected. Under τ1, formula φ|τ1 is unsatisﬁable due to the conﬂict among clauses C1, C2, and C3, and the minimal conﬂicting assignment τ + 1 equals τ1. After conjoining ψ with τ + 1 , suppose τ2 = r1r2r3 is chosen. Formula φ|τ2 is satisﬁable through the assignment µ0 = e1e2 e3. The subroutine Minimal Satisfying is invoked to generalize τ2 to τ + 2 = r2r3, which reﬂects a lower bound of 0.25 for the satisfying probability of Φ. Similarly, the negation of τ + 2 is conjoined with ψ. Next, let the assignment chosen by ψ be τ3 = r1 r2r3. Since φ|τ3 is satisﬁable through the assignment µ1 = e1 e2 e3, assignment τ3 is generalized to τ + 3 = r1r3 by Minimal Satisfying. After conjoined with τ + 3 , formula ψ becomes unsatisﬁable, which indicates the Boolean space over {r1, r2, r3} has been explored exhaustively. At the end, we have C = {τ + 0 , τ + 1 } = { r3, r1 r2r3} and C = {τ + 2 , τ + 3 } = {r2r3, r1r3}. The subroutine Compute Weight is ﬁnally invoked and returns 0.375 as the satisfying probability of Φ.

4 Experimental Results Our solver, named re SSAT, was implemented in the C++ language. The experiments were conducted on a Linux machine with Intel Xeon 2.1 GHz CPU and 126 GB RAM. We compared the proposed approach with the state-of-theart DPLL-based SSAT solver DC-SSAT. The SAT solver Minisat-2.2 and model counter Cachet were used in our program as underlying computational engines. (We tried approximate model counter Approx MC [Chakraborty et al., 2013] and observed that Approx MC outperformed Cachet mainly on difﬁcult instances while Cachet tended to perform better on other instances. As our benchmarks favored Cachet, it was used in our experiments.) Three sets of formulas, including random k-CNF, strategic companies, and probabilistic equivalence checking formulas, were used to evaluate our solver against DC-SSAT, abbreviated as Dc in the sequel. A basic version of re SSAT without minterm generalization is denoted as re SSAT-b. A runtime limit of 1000 seconds was imposed on each formula. No memory limit was

Proceedings of the Twenty-Sixth International Joint Conference on Artiﬁcial Intelligence (IJCAI-17)

Figure 2: Results of selected random SSAT formulas.

imposed, but peak memory usage during execution was examined.

4.1 Random k-CNF Formulas The random k-CNF formulas are generated using the cnfgen command [Lauria, 2012]. Let k be the number of literals in a clause, n be the number of variables, and m be the number of clauses. A collection of 700 CNF formulas is generated with the following parameter settings. Let k range from 3 to 9, n equal 10, 20, 30, 40, 50, and the clausesto-variables ratio m

n range from k 1 to k + 2. For each combination of parameters, ﬁve formulas were generated. To convert the generated CNF formulas into random-exist quantiﬁed SSAT formulas, half of the variables in a CNF formula are randomly quantiﬁed with probability 0.5, and the rest of the variables are existentially quantiﬁed. (Note that a randomexist SSAT formula with randomized quantiﬁers of arbitrary probabilities can be converted to one with only randomized quantiﬁers of probability 0.5 through rewriting using auxiliary variables [Lee and Jiang, 2014].) Out of the 700 generated formulas, we selected 300 formulas with their satisfying probabilities evenly distributed in [0, 1] for evaluation. The results are shown in Figure 2. Without minterm generalization, re SSAT-b only solved 229 formulas within the runtime limit of 1000 seconds, while Dc solved 266 formulas. On the other hand, re SSAT solved all 300 formulas, showing that the minterm-generalization technique is essential to the efﬁciency of re SSAT. Speciﬁcally, the number of collected cubes with minterm generalization is on average 8 times smaller than that without the generalization, and the runtime is reduced by an order of magnitude. Compared to Dc, re SSAT achieved an average runtime improvement by 5 times, and a maximum peak memory reduction by 2 orders of magnitude.

4.2 Planning Formulas Many planning problems can be formulated in terms of forall-exist quantiﬁed QBFs, i.e., QBFs of the form Φ = X Y.φ(X, Y ). By changing universal quantiﬁers to randomized ones, random-exist SSAT formulas can be obtained. In essence, under the game interpretation of QBFs, the satisfying probability of these SSAT formulas corresponds to the likelihood for the existential player to win the QBF game

Figure 3: Results of strategic companies SSAT formulas.

when the universal player plays her/his moves at random. We take the strategic companies problem, which was deﬁned in [Cadoli et al., 1997], as an example to evaluate the performance of SSAT algorithms on planning applications. The strategic companies problem can be brieﬂy described as follows. Suppose a businessman owns n companies that produce m kinds of products. A company is strategic if it is in a minimal set of companies that together produce all kinds of products. The information of whether a company is strategic is valuable to the businessman. Suppose the businessman encounters a crisis and considers to sell out some companies, but hopes to keep producing every kind of products. As a result, he may prefer to sell out a non-strategic company. The problem is more complicated by taking the controlling relations into account. If a company is controlled by other companies, it means that the company can be sold out only if some of its controlling companies is also sold out. The problem to decide whether a company is strategic or not can be encoded as forall-exist quantiﬁed QBFs [Faber and Ricca, 2005; Leone et al., 2006]. We modify the QBFs of the strategic companies problem, taken from QBFLIB [Giunchiglia et al., 2005], to their SSAT variants by changing the universal quantiﬁers in the original QBFs to randomized ones with probabilities 0.5. The satisfying probability reﬂects the likelihood for a company to be strategic. The QBFs we experimented with describe the strategic companies problems under the following setting of parameters: n equals 5, 10, 15, . . . , 75, m = 3n, and the number of controlling relations equals 4, 9, 14, 19. The results of the 60 formulas are plotted in Figure 3. While re SSAT-b only solved 12 formulas, Dc solved 30 formulas. Enabling the minterm-generalization technique makes re SSAT solve all 60 formulas. The results show that the technique worked well not only on random formulas, but also on structured instances from AI applications. Compared to Dc, re SSAT achieved an average runtime improvement by 2 orders of magnitude, and a maximum peak memory reduction by 2 orders of magnitude as well.

4.3 Probabilistic Equivalence Checking Formulas Another SSAT application, formulated in [Lee and Jiang, 2014], is formal veriﬁcation of probabilistic circuits. As probabilistic errors are becoming more common in advanced

Proceedings of the Twenty-Sixth International Joint Conference on Artiﬁcial Intelligence (IJCAI-17)

Table 1: Results of solving SSAT formulas from probabilistic equivalence checking.

formula statistics re SSAT (TO=60s) re SSAT (TO=1000s) Dc (TO=1000s) circuit #Var #Cla #Ran Ans. runtime (s) UB LB runtime (s) UB LB runtime (s) Prob. c432 330 879 37 1.03E-02 TO 1.07E-02 4.30E-05 TO 1.05E-02 8.50E-05 TO TO c499 217 522 42 1.56E-13 0.32 1.56E-13 1.56E-13 0.13 1.56E-13 1.56E-13 0.00 1.56E-13 c880 451 1167 62 4.18E-02 TO 9.78E-02 3.00E-06 TO 8.18E-02 3.00E-06 TO TO c1355 771 2181 44 6.41E-02 TO 3.20E-01 0.00E+00 TO 3.08E-01 0.00E+00 TO TO c1908 270 705 35 7.38E-04 TO 8.83E-04 4.00E-05 TO 7.38E-04 7.90E-05 210.86 7.38E-04 c3540 321 807 52 1.71E-03 TO 1.17E-02 5.03E-04 TO 1.17E-02 1.61E-03 217.42 1.71E-03 c5315 918 2190 188 4.64E-01 TO 6.28E-01 0.00E+00 TO 6.28E-01 0.00E+00 TO TO c7552 648 1308 212 2.34E-01 TO 2.35E-01 7.32E-03 TO 2.35E-01 7.32E-03 TO TO maximum memory usage (MB) 164 718 42466

nanometer technology, the probabilistic equivalence checking (PEC) problem asks to compute the probability for a probabilistic circuit to produce different outputs from its faultless speciﬁcation. PEC was encoded into a random-exist quantiﬁed SSAT formula in [Lee and Jiang, 2014]. The SSAT formulas for probabilistic equivalence checking (PEC) are created as follows. The circuit with probabilistic errors is generated by assigning some gates in the original faultless circuit to be erroneous randomly. Two parameters are speciﬁed to control the generation of probabilistic circuits. The erroneous rate ϵ controls the probability of the happening of an error at a logic gate, and the defective rate δ controls the ratio of the number of erroneous gates to the total number of gates in the whole circuit. In our experiments, we use circuits from ISCAS benchmark suits and set ϵ = 0.125, δ = 0.01. Table 1 shows the experimental results on PEC formulas. Columns 2, 3, and 4 show the numbers of variables, clauses, and randomly quantiﬁed variables in the formulas. Column 5 shows the exact satisfying probability of the formulas, computed by the signal probability method based on binary decision diagram (BDD) [Lee and Jiang, 2014]. Since re SSAT has the capability of solving approximate SSAT, we set a relatively short timeout of 60 seconds to evaluate its ability to derive upper and lower bounds for satisfying probability under a strict time constraint. Columns 6, 7, and 8 (resp. Columns 9, 10, and 11) show the runtime, upper bounds, and lower bounds of re SSAT with the timeout set to 60 (resp. 1000) seconds. Columns 12 and 13 show the runtime and satisfying probability of Dc with a 1000-second timeout. While both methods failed to compute the exact answers on most of the cases, re SSAT derived tight bounds on some of the benchmarks. For example, for formulas c432 and c7552, the upper bounds derived by re SSAT with a 60second timeout are very close to the exact satisfying probabilities, while Dc could not ﬁnish the computation on these two benchmarks even after 1000 seconds. On the other hand, notice that the derived bounds were not reﬁned much after 60 seconds. The reason for the bounds not getting tight might lie in that in early search period, large cubes might have been collected and blocked huge search space. In other words, even if the runtime limit is increased, the additional small cubes collected do not contribute to a large fraction of the estimated probability. However, such a phenomenon does not hinder the application of re SSAT when the upper or lower bound of satisfying probability converges rapidly. The inex-

act estimation can be valuable when the exact computation is unavailable, such as c432 and c7552 in the experiment. The above empirical results on the three benchmark families suggested that re SSAT outperforms Dc in terms of both runtime and memory consumption on random and strategic companies formulas, and re SSAT gives reasonable bounds on satisfying probability within 60 seconds, while Dc timed out on some of the PEC formulas.

5 Conclusions In this paper, we focused on solving random-exist quantiﬁed SSAT formulas. In contrast to the previous DPLL-based algorithms, we proposed a novel algorithm using SAT solver and weighted model counter as underlying engines to improve computational efﬁciency. Leveraging the great success of modern SAT solving techniques, the proposed algorithm outperforms the state-of-the-art method in the experiment on random k-CNF and strategic companies formulas. Moreover, unlike previous exact SSAT methods, the proposed algorithm can be easily modiﬁed to solve approximate SSAT by deriving upper and lower bounds of satisfying probability. We demonstrated the applicability of our SSAT solver to VLSI circuit analysis. While the state-of-the-art solver fails to compute the exact satisfying probability, the proposed method succeeded in ﬁnding bounds of the formulas. In several cases, the derived bounds are very close to, or even match the exact satisfying probability. This approximation ﬂexibility of our method can be helpful when SSAT is applied to real-world applications. For future work, we intend to extend the proposed algorithm to arbitrary quantiﬁed SSAT formulas.

Acknowledgements The authors thank Stephen Majercik for kindly providing the SSAT solver DC-SSAT, and anonymous reviewers for valuable suggestions. This work was supported in part by the Ministry of Science and Technology of Taiwan under grants 104-2628-E-002-013-MY3, 105-2221-E-002-196MY3, 105-2923-E-002-016-MY3, and 106-2912-E-002-002MY3.

Proceedings of the Twenty-Sixth International Joint Conference on Artiﬁcial Intelligence (IJCAI-17)

References [Aziz et al., 2015] R. Aziz, G. Chu, C. Muise, and P. Stuckey. # SAT: Projected model counting. In Proc. SAT, pages 121 137, 2015. [Bacchus et al., 2003] F. Bacchus, S. Dalmao, and T. Pitassi. Algorithms and complexity results for #SAT and Bayesian inference. In Proc. FOCS, pages 340 351, 2003. [Cadoli et al., 1997] M. Cadoli, T. Eiter, and G. Gottlob. Default logic as a query language. IEEE Transactions on Knowledge and Data Engineering, 9(3):448 463, 1997. [Chakraborty et al., 2013] S. Chakraborty, K. Meel, and M. Vardi. A scalable approximate model counter. In Proc. CP, pages 200 216, 2013. [Chakraborty et al., 2016] S. Chakraborty, K. Meel, and M. Vardi. Algorithmic improvements in approximate counting for probabilistic inference: From linear to logarithmic SAT calls. In Proc. IJCAI, 2016. [Chavira and Darwiche, 2008] M. Chavira and A. Darwiche. On probabilistic inference by weighted model counting. Artiﬁcial Intelligence, 172(6-7):772 799, 2008. [Cooper, 1990] G. Cooper. The computational complexity of probabilistic inference using Bayesian belief networks. Artiﬁcial Intelligence, 42(2-3):393 405, 1990. [Davis et al., 1962] M. Davis, G. Logemann, and D. Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394 397, 1962. [E en and S orensson, 2003a] N. E en and N. S orensson. An extensible SAT-solver. In Proc. SAT, pages 502 518, 2003. [E en and S orensson, 2003b] N. E en and N. S orensson. Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science, 89(4):543 560, 2003. [Faber and Ricca, 2005] W. Faber and F. Ricca. Solving hard ASP programs efﬁciently. In Proc. LPNMR, pages 240 252, 2005. [Giunchiglia et al., 2005] E. Giunchiglia, M. Narizzano, L. Pulina, and A. Tacchella. Quantiﬁed Boolean Formulas satisﬁability library (QBFLIB), 2005. http://www. qbflib.org. [Gomes et al., 2006] C. Gomes, A. Sabharwal, and B. Selman. Model counting: A new strategy for obtaining good bounds. In Proc. AAAI, pages 54 61, 2006. [Gomes et al., 2007] C. Gomes, J. Hoffmann, A. Sabharwal, and B. Selman. From sampling to model counting. In Proc. IJCAI, pages 2293 2299, 2007. [Hnich et al., 2011] B. Hnich, R. Rossi, A. Tarim, and S. Prestwich. A survey on CP-AI-OR hybrids for decision making under uncertainty. Hybrid Optimization, pages 227 270, 2011. [Lauria, 2012] M. Lauria. CNFgen: Combinatorial benchmarks for SAT solvers, 2012. http:// massimolauria.github.io/cnfgen/.

[Lee and Jiang, 2014] N.-Z. Lee and J.-H. Jiang. Towards formal evaluation and veriﬁcation of probabilistic design. In Proc. ICCAD, pages 340 347, 2014. [Leone et al., 2006] N. Leone, G. Pfeifer, W. Faber, T. Eiter, G. Gottlob, S. Perri, and F. Scarcello. The DLV system for knowledge representation and reasoning. ACM Transactions on Computational Logic, 7(3):499 562, 2006. [Majercik and Boots, 2005] S. Majercik and B. Boots. DCSSAT: A divide-and-conquer approach to solving stochastic satisﬁability problems efﬁciently. In Proc. AAAI, pages 416 422, 2005. [Majercik and Littman, 1998] S. Majercik and M. Littman. Maxplan: A new approach to probabilistic planning. In Proc. AIPS, pages 86 93, 1998. [Majercik and Littman, 2003] S. Majercik and M. Littman. Contingent planning under uncertainty via stochastic satisﬁability. Artiﬁcial Intelligence, 147(1-2):119 162, 2003. [Majercik, 2007] S. Majercik. APPSSAT: Approximate probabilistic planning using stochastic satisﬁability. International Journal of Approximate Reasoning, 45(2):402 419, 2007. [Majercik, 2009] S. Majercik. Stochastic Boolean satisﬁability. Handbook of Satisﬁability, 185:887 925, 2009. [Papadimitriou, 1985] C. Papadimitriou. Games against nature. Journal of Computer and System Sciences, 31(2):288 301, 1985. [Sang et al., 2004] T. Sang, F. Bacchus, P. Beame, H. Kautz, and T. Pitassi. Combining component caching and clause learning for effective model counting. In Proc. SAT, pages 20 28, 2004. [Sang et al., 2005a] T. Sang, P. Beame, and H. Kautz. Heuristics for fast exact model counting. In Proc. SAT, pages 226 240, 2005. [Sang et al., 2005b] T. Sang, P. Beame, and H. Kautz. Performing Bayesian inference by weighted model counting. In Proc. AAAI, pages 475 481, 2005. [Teige and Fr anzle, 2010] T. Teige and M. Fr anzle. Resolution for stochastic Boolean satisﬁability. In Proc. LPAR, pages 625 639, 2010.

Proceedings of the Twenty-Sixth International Joint Conference on Artiﬁcial Intelligence (IJCAI-17)