Solving Stochastic Boolean Satisfiability under Random-Exist Quantification

1 Introduction

First formulated in [Papadimitriou, 1985], stochastic Boolean satisfiability (SSAT) was described as a game against nature. Probabilistic factors are introduced into the world of Boolean logic through the creation of the randomized quantifier. A Boolean variable randomly quantified with probability p has a probability p of evaluating to TRUE. Exploiting randomized quantifiers, 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 verification of probabilistic circuits [Lee and Jiang, 2014]. From computational complexity point of view, SSAT lies in the PSPACEcomplete complexity class, same as quantified Boolean satisfiability (QSAT). Therefore, developing good algorithms for SSAT not only brings practical benefits 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 quantified 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 first attempt to directly use a SAT solver as a plug-in engine for SSAT solving. In this paper, we focus on the random-exist quantified SSAT formula of the form Φ = R X∃Y.φ, which is the counterpart of the forall-exist quantified QBF formula. The random-exist quantified SSAT has applications in belief network inference [Cooper, 1990; Bacchus et al., 2003], probabilistic planning, and probabilistic circuit verification [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 quantifiers. The proposed algorithm 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 benefit from the advancement of the solvers without any modification. Moreover, unlike previous DPLL-based methods, the proposed algorithm can be easily modified 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 artificial 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 specified set of variables. A Boolean formula φ is called satisfiable if there exists a satisfying complete assignment for φ. We write SAT(φ) = ⊤ to denote φ is satisfiable. A satisfying assignment of φ is also called a model of φ, denoted by φ.model. On the other hand, if φ has no satisfying assignment, it is unsatisfiable 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 satisfiable (resp. unsatisfiable), τ 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 satisfiability 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 satisfiable 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 unsatisfiable.

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 find 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 satisfiability, 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 finding the minimum satisfying assignment is also known as finding the minimum hitting set.

Minimum Conflicting 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 unsatisfiability, which is represented as a conjunction of literals in τ causing the conflict. If some literals in τ are irrelevant to the conflict, 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 conflicting assignment. The process of finding the minimum conflicting assignment is also known as finding the minimum UNSAT core.

2.2 Model Counting

Given a CNF formula φ, the model counting problem finds 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 defined 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 confidence level.

2.3 Stochastic Boolean Satisfiability

A stochastic Boolean satisfiability (SSAT) formula is of the form

where Qi ∈ {∃, R pi } and φ is a quantifier-free Boolean formula. In addition to the existential quantifier ∃, the randomized quantifier R pi on xi assigns a probability pi ∈ [0, 1] for xi to be true. The quantifier part is called the prefix, and the Boolean formula is called the matrix. Given an SSAT formula Φ, let v be the outermost variable in the prefix. The satisfying probability of Φ can be computed by the following rules.

1. Pr[⊤] = 1, b) Pr[⊥] = 0, c) Pr[Φ] = max{Pr[Φ|¬v],Pr[Φ|v]}, if v is existentially quantified, d) Pr[Φ] = (1 - p)Pr[Φ|¬v] + pPr[Φ|v], if v is randomly quantified by R p ,

where Φ|¬v and Φ|v denote the SSAT formulas derived by eliminating the outermost quantifier of v by substituting the value of v in the matrix with ⊥ and ⊤, respectively. In this paper, we aims at solving the random-exist quantified SSAT formula of the form Φ = R 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 quantified SSAT formula Φ = R 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 suffices to check whether φ(X, Y )|τ is satisfiable or not. A naive solution to computing the satisfying probability of Φ exhaustively examines all assignments on X, classifies 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 satisfiable 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 efficiency of the enumeration of all possible assignments on X. As will be shown in Section 4, the minterm-generalization techniques are essential to the efficiency 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 difficulty 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 Φ = R X∃Y.φ(X, Y ). The proposed algorithm works as follows. First assume the runtime limit TO to be infinity, while the effect of imposing a runtime limit on SolveRESSAT will be explained in Section 3.4. Two SAT solvers are used in SolveRESSAT. 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 satisfiable. Depending on the satisfiability of φ(X, Y )|τ , the

SolveRESSAT input: Φ = R 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 τ + := MinimalSatisfying(φ, τ); 08 C⊤ := C⊤ ∪ {τ +}; 09 else //SAT(φ|τ ) = ⊥ 10 τ + := MinimalConflicting(φ, τ); 11 C⊥ := C⊥ ∪ {τ +}; 12 ψ := ψ ∧¬τ +; 13 return (1-ComputeWeight(C⊥), ComputeWeight(C⊤)); end

minterm τ is generalized into a cube by the subroutine MinimalSatisfying or MinimalConflicting. Instead of finding the minimum satisfying or conflicting assignment, which is computationally expansive, we resort to finding a minimal satisfying or conflicting assignment, i.e., an assignment having no literals removable without affecting the (un)satisfiability, to leverage the efficiency 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 unsatisfiable, which signifies the Boolean space spanned by X has been exhaustively searched. The subroutine ComputeWeight is then invoked to evaluate the weight of the collected cubes. The subroutines MinimalConflicting, MinimalSatisfying, and ComputeWeight 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 MinimalSatisfying generalizes τ to τ + via the following steps.

1. Remove every clause C in φ(X, Y )|τ that contains some true literal in µ.
2. For each literal l in τ, drop l and examine whether the rest of clauses remain satisfied by scanning these clauses and checking if each of them still contains some true literal. If the rest of clauses are all satisfied, discard l; otherwise, put l in τ +.

After the above steps, the SAT minterm τ is generalized into a minimal satisfying assignment τ +.

3.2 Minimal Conflicting Assignment

Let τ be an UNSAT minterm on X for φ(X, Y ). The analysis of unsatisfiability can be done with a modern SAT solver (e.g., using analyzeFinal() in Minisat) to find a conjunction of literals from τ responsible for the conflict. However, in general this conjunction of literals might not be minimal, meaning that some of the literals can be dropped. The subroutine MinimalConflicting takes the conjunction of literals responsible for the conflict 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 unsatisfiable by invoking a SAT call. If it is unsatisfiable, discard l; otherwise, put l in τ +. After the above steps, the UNSAT minterm τ is generalized into a minimal conflicting assignment τ +.

3.3 Weight Computation

The subroutine ComputeWeight aggregates the weight of collected cubes by invoking a weighted model counter. Because the weighted model counter takes CNF formulas as input, ComputeWeight first 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 Modification for Approximate SSAT

The proposed algorithm can be easily modified to solve approximate SSAT, where upper and lower bounds of the satisfying probability of an SSAT formula are computed. Suppose SolveRESSAT is forced to terminate before the selector ψ becomes unsatisfiable. The weights of the collected SAT and UNSAT cubes are still valid and can be aggregated by ComputeWeight, and the resulted weights reflect the lower and upper bounds of the satisfying probability, respectively. The early termination can be triggered by imposing a runtime limit for SolveRESSAT. Compared to previous DPLL-based methods that branch on a single variable, the proposed algorithm considers all randomly quantified variables together and exploits the concept of SAT and UNSAT cubes over the Boolean space spanned by randomly quantified 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 find tight bounds even with a short time limit. Compared to the DPLL-based state-of-theart methods, which cannot be easily modified for approximate SSAT, the proposed method enjoys the flexibility of solving SSAT approximately or exactly, depending on the imposed runtime constraint.

We note that the proposed algorithm is more efficient 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 efficiency. 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 SolveRESSAT solves a random-exist quantified SSAT formula.

Example 2 Consider the random-exist quantified SSAT formula Φ = R 0.5 r1r2r3∃e1e2e3.φ, with φ consisting of clauses

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 ψ first selects the assignment τ0 = ¬r1¬r2¬r3. Since φ|τ0 is unsatisfiable (due to the conflict between C4 and C5), the subroutine MinimalConflicting returns τ + 0 = ¬r3, which is the minimal conflicting assignment responsible for this conflict. Note that this minimal conflicting assignment τ + 0 reflects 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 unsatisfiable due to the conflict among clauses C1, C2, and C3, and the minimal conflicting assignment τ + 1 equals τ1. After conjoining ψ with ¬τ + 1 , suppose τ2 = ¬r1r2r3 is chosen. Formula φ|τ2 is satisfiable through the assignment µ0 = ¬e1e2¬e3. The subroutine MinimalSatisfying is invoked to generalize τ2 to τ + 2 = r2r3, which reflects 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 satisfiable through the assignment µ1 = ¬e1¬e2¬e3, assignment τ3 is generalized to τ + 3 = r1r3 by MinimalSatisfying. After conjoined with ¬τ + 3 , formula ψ becomes unsatisfiable, 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 ComputeWeight is finally invoked and returns 0.375 as the satisfying probability of Φ.

4 Experimental Results

Our solver, named reSSAT, 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 ApproxMC [Chakraborty et al., 2013] and observed that ApproxMC outperformed Cachet mainly on difficult 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 reSSAT without minterm generalization is denoted as reSSAT-b. A runtime limit of 1000 seconds was imposed on each formula. No memory limit was 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 mn range from k - 1 to k + 2. For each combination of parameters, five formulas were generated. To convert the generated CNF formulas into random-exist quantified SSAT formulas, half of the variables in a CNF formula are randomly quantified with probability 0.5, and the rest of the variables are existentially quantified. (Note that a randomexist SSAT formula with randomized quantifiers of arbitrary probabilities can be converted to one with only randomized quantifiers 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, reSSAT-b only solved 229 formulas within the runtime limit of 1000 seconds, while Dc solved 266 formulas. On the other hand, reSSAT solved all 300 formulas, showing that the minterm-generalization technique is essential to the efficiency of reSSAT. Specifically, 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, reSSAT 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 quantified QBFs, i.e., QBFs of the form Φ = ∀X∃Y.φ(X, Y ). By changing universal quantifiers 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 when the universal player plays her/his moves at random. We take the strategic companies problem, which was defined in [Cadoli et al., 1997], as an example to evaluate the performance of SSAT algorithms on planning applications.

Figure 3: Results of strategic companies SSAT formulas.

The strategic companies problem can be briefly 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 quantified 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 quantifiers in the original QBFs to randomized ones with probabilities 0.5. The satisfying probability reflects 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 reSSAT-b only solved 12 formulas, Dc solved 30 formulas. Enabling the minterm-generalization technique makes reSSAT 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, reSSAT 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 verification of probabilistic circuits. As probabilistic errors are becoming more common in advanced nanometer technology, the probabilistic equivalence checking (PEC) problem asks to compute the probability for a probabilistic circuit to produce different outputs from its faultless specification. PEC was encoded into a random-exist quantified 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 specified 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 quantified 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 reSSAT 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 reSSAT 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, reSSAT derived tight bounds on some of the benchmarks. For example, for formulas c432 and c7552, the upper bounds derived by reSSAT with a 60second timeout are very close to the exact satisfying probabilities, while Dc could not finish the computation on these two benchmarks even after 1000 seconds. On the other hand, notice that the derived bounds were not refined 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 reSSAT when the upper or lower bound of satisfying probability converges rapidly. The inexact 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

• reSSAT outperforms Dc in terms of both runtime and memory consumption on random and strategic companies formulas, and
• reSSAT 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 quantified 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 efficiency. 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 modified 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 finding bounds of the formulas. In several cases, the derived bounds are very close to, or even match the exact satisfying probability. This approximation flexibility 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 quantified 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.