Solving Exist-Random Quantified Stochastic Boolean Satisfiability via Clause Selection

1 Introduction

Stochastic Boolean satisfiability (SSAT) was first formulated in [Papadimitriou, 1985] and interpreted as games against nature. In an SSAT formula, a Boolean variable can be randomly quantified with probability p by a randomized quantifier, which specifies that the variable evaluates to TRUE with probability p. With randomized quantifiers, SSAT serves as a natural formalism for an abundance of computational problems endowed with randomness, such as propositional probabilistic planning, trust management, and Bayesian network inference [Hnich et al., 2011; Littman et al., 2001; Majercik, 2009]. The verification problem of VLSI circuits with probabilistic errors has also been investigated under the framework of SSAT recently [Lee and Jiang, 2014]. From the perspective of computational complexity, SSAT lies in the complexity class PSPACE-complete, the same as quantified Boolean formula (QBF). Therefore, advancing the scalability of SSAT solving not only benefits practical applications, but also has profound theoretical values.

∗The authors contributed equally to this work.

In this paper, we focus on the exist-random quantified SSAT formulas of the form Φ = ∃X R Y.φ, which is known as E-MAJSAT [Littman et al., 1998]. Computational problems, such as computing a maximum a posteriori (MAP) hypothesis or a maximum expected utility (MEU) solution [Dechter, 1998] in belief networks, and searching an optimal plan for probabilistic conformant planning domains [Littman et al., 1998], can be formulated with E-MAJSAT.

Among previous endeavors, several techniques have been investigated to solve SSAT. Prior work MAXPLAN [Majercik and Littman, 1998] utilizes Davis-Putnam-LogemannLoveland (DPLL) search [Davis et al., 1962] and improves its efficiency by considering pure variables, unit propagation, and subproblem memorization. DCSSAT [Majercik and Boots, 2005] enhances MAXPLAN by applying the divideand-conquer strategy to break SSAT formulas into many subproblems and solve them separately. The technique of knowledge compilation has also been exploited to solve EMAJSAT. ComPlan [Huang, 2006] compiles the problems into deterministic, decomposable negation normal form (dDNNF) [Darwiche, 2001; 2002], and performs a branchand-bound search. It is further improved in [Pipatsrisawat and Darwiche, 2009] by an enhanced bound computation method. Recent work [Fremont et al., 2017] proposed a maximum model counting algorithm for solving a special case of E-MAJSAT with all probabilities of randomized quantifiers equal to 0.5.

Recently, modern SAT techniques have been utilized to solve random-exist quantified SSAT formulas in [Lee et al., 2017], which inspires us to examine the possibility of applying QBF solving techniques in the SSAT domain.

In this paper, we exploit the clause selection technique, which has been introduced in QBF solving recently [Janota and Marques-Silva, 2015; Rabe and Tentrup, 2015], and propose a clause containment learning method for E-MAJSAT solving. To the best of our knowledge, this paper is the first attempt to adopt approaches developed for QBF to solve SSAT. In addition to the learning technique, weighted model counting, which has been widely adopted in probabilistic inference [Chavira and Darwiche, 2008; Sang et al., 2005], is utilized in the proposed algorithm to compute probabilities.

We evaluate the proposed algorithm with a wide range of benchmarks including random formulas, planning problems, and probabilistic circuit verification. Experiments show that our method achieves significant performance gains and memory savings compared to the state-of-the-art SSAT solvers.

2 Preliminaries

We represent Boolean values TRUE and FALSE by symbols ⊤ and ⊥, respectively. In the sequel, a variable x is assumed in the Boolean domain B = {⊤,⊥}. A literal is a variable (called a positive literal) or the negation of a variable (called a negative literal). For a literal l, let var(l) denote the variable of l. Boolean connectives ¬, ∨, ∧,⇒,≡ are interpreted in their conventional meanings. A clause is a disjunction of literals. A propositional Boolean formula φ is in Conjunctive Normal Form (CNF) if φ is a conjunction of clauses. A variable x is said to be pure in a formula if its appearances in the formula are all in the positive phase x or in the negative phase ¬x. A cube is a conjunction of literals. In the sequel, we assume propositional Boolean formulas are in CNF.

A Boolean formula φ over a set of variables X = {x1, . . . , xn} defines a unique Boolean function Bn → B. Let vars(φ) denote the set of variables appearing in a Boolean formula φ. An assignment τ over a set of variables X ⊆ vars(φ) for a formula φ is a mapping τ : X → B. An assignment τ : X → B is a complete assignment for formula φ if X = vars(φ); otherwise, i.e., X ⊂ vars(φ), it is a partial assignment. Given a Boolean formula φ and an assignment τ over vars(φ), the cofactor of φ under τ, denoted by φ|τ , is derived by substituting every occurrence of each variable x ∈ vars(φ) in φ by τ(x). If φ|τ = ⊤, we call τ a satisfying assignment of φ. The satisfiability problem of a Boolean formula φ asks whether or not φ has a satisfying assignment. We write SAT(φ) = ⊤ to denote that φ is satisfiable. A satisfying assignment of φ is also called a model of φ. On the other hand, if φ has no satisfying assignment, it is unsatisfiable and written as SAT(φ) = ⊥. Given two Boolean formulas φ and ψ, we write φ |= ψ if every satisfying assignment for φ also satisfies ψ. In the sequel, we alternatively represent an assignment τ as a cube, a clause C as a set of literals, and a CNF formula as a set of clauses.

2.1 Stochastic Boolean Satisfiability

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

where Qi ∈ {∃, R pi } and φ is a quantifier-free Boolean formula. Symbol ∃ denotes the existential quantifier, and R pi denotes the randomized quantifier on xi for the probability of xi = ⊤ equal to pi ∈ [0, 1]. Given an SSAT formula Φ, the quantification structure Q1x1 . . .Qnxn is called the prefix, and the Boolean formula φ is called the matrix.

Let v be the outermost variable in the prefix of an SSAT formula Φ. The satisfying probability of Φ, denoted by Pr[Φ], can be computed recursively by the following rules.

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

In this paper, we focus on solving E-MAJSAT, the exist-random fragment of SSAT with the form Φ = ∃X R Y.φ(X, Y ), where X and Y are two disjoint sets of variables. The satisfying probability of Φ is obtained through maximizing Pr[Φ|τ ], called the satisfying probability of Φ conditioned on τ , over all assignments τ on X.

2.2 Model Counting

The model counting problem of a Boolean formula φ asks to find the number of satisfying assignments of φ. Model counting algorithms can be classified into two categories: exact model counting and approximate model counting. The former computes the exact number of satisfying assignments of a formula; the latter computes an upper or a lower bound of the number of satisfying assignments with some confidence level. In its weighted version, a weight function ω is defined to map each variable x ∈ vars(φ) to some weight ω(x) ∈ [0, 1], which can be seen as the probability Pr[x = ⊤]. The weight of a positive literal x (resp. negative literal ¬x) of variable x is defined to be ω(x) (resp. 1 - ω(x)). The weight of an assignment is defined to be the product of the weights of its individual literals. The weight of a formula equals the summation of weights of its satisfying assignments.

Given an E-MAJSAT formula Φ = ∃X R Y.φ(X, Y ) and an assignment τ on X, cofactoring the matrix with τ results in a formula φ|τ referring only to variables in Y . The prefix R Y induces a weight function ω : Y → [0, 1] for each variable y ∈ Y , where ω(y) equals the probability annotated on the randomized quantifier of y. As a result, the conditional satisfying probability Pr[Φ|τ ], which equals the weight of the formula φ|τ under the weight function ω, can be obtained by invoking a weighted model counter on the formula φ|τ with the weight function ω. In the sequel, the invocation of a weighted model counter is expressed by WeightModelCount( R Y.φ|τ ), which returns the conditional satisfying probability Pr[ R Y.φ|τ ].

2.3 Clause Selection

Clause selection is a recently proposed technique for QBF solving [Janota and Marques-Silva, 2015; Rabe and Tentrup, 2015]. Given a CNF formula φ(X, Y ) over a set of variables X∪Y with X∩Y = ∅, we divide each clause C ∈ φ into two sub-clauses C X and C Y , where C X (resp. C Y ) consists of the literals whose variables are in X (resp. Y ). For example, for C = (x1 ∨ x2 ∨ y1 ∨ y2), we have C X = (x1 ∨ x2) and C Y = (y1 ∨ y2). Clearly, C = C X ∨ C Y .

A clause C is said to be selected by an assignment τ over X if every literal in C X is assigned to ⊥ by τ ; C is said to be deselected by τ if some literal in C X is assigned to ⊤ by τ ; C is said to be undecided if it is neither selected nor deselected. We also use φ|τ to denote the set of clauses selected by the assignment τ. A selection variable sC is introduced for each clause C and defined by sC ≡ ¬C X . Hence, sC is an indicator of the selection of clause C. That is, sC = ⊤ (resp. sC = ⊥) indicates C is selected (resp. deselected). Let S be the set of selection variables for clauses in φ(X, Y ). The formula ψ(X, S) = ∧C∈φ (sC ≡ ¬C X ) is called the selection relation of φ(X, Y ).

Example 1 Consider a CNF formula φ(X, Y ) over two sets of variables X = {e1, e2, e3} and Y = {r1, r2, r3}. φ(X, Y ) consists of four clauses:

C1 : (e1 ∨ r1 ∨ r2) C2 : (e1 ∨ e2 ∨ r1 ∨ r2 ∨ ¬r3) C3 : (¬e2 ∨¬e3 ∨ r2 ∨¬r3) C4 : (¬e1 ∨ e3 ∨ r3)

A selection variable si is introduced for each clause, and S = {s1, s2, s3, s4}. The selection relation ψ(X, S) of φ(X, Y ) equals

Consider the complete assignment τ1 = ¬e1¬e2¬e3 over X. It selects C1 and C2, and deselects C3 and C4, as can be seen from the selection relation cofactored by τ1, which results in ψ(X, S)|τ1 = s1s2¬s3¬s4. Consider the partial assignment τ2 = ¬e1e3 over X. It selects C1, deselects C4, and leaves C2 and C3 undecided. Notice that the two complete assignments ¬e1¬e2e3 and ¬e1e2e3 consistent with τ2 select {C1,C2} and {C1,C3}, respectively. The clause C1 selected by the partial assignment τ2 lies in the intersection of the sets of clauses selected by the two complete assignments consistent with τ2.

3 Clause Containment Learning

Consider an E-MAJSAT formula Φ = ∃X R Y.φ. To obtain the satisfying probability of Φ, it suffices to enumerate every assignment τ on X, and calculate the corresponding conditional satisfying probability Pr[Φ|τ ]. Clearly, the above brute-force approach is computationally expensive. Inspired by the idea of clause selection discussed above, we propose clause containment learning to prune the search space. The proposed learning technique deduces useful information after each trial of an assignment τ on X. The learnt information is recorded as blocking clauses to avoid wasteful exploration and thus accelerates the search process. The proposed learning technique is based on the following key observation.

Property 1 Given an E-MAJSAT formula Φ = ∃X R Y.φ(X, Y ) and two assignments τ1 and τ2 over

By Property 1 and clause selection, we propose clause containment learning as detailed below. After cofactoring φ with an arbitrary assignment τ1 over X, a set of clauses φ|τ1 is selected. For any other assignment τ2 selecting every clause in φ|τ1 , i.e., φ|τ1 ⊆ φ|τ2 , we have φ|τ2 |= φ|τ1 . Therefore, Pr[Φ|τ2 ] ≤ Pr[Φ|τ1 ] holds by Property 1. Since the satisfying probability Pr[Φ|τ2 ] is not greater than Pr[Φ|τ1 ], the assignment τ2 is not worth trying. For all such assignments, they should be blocked after τ1 has been explored.

The core idea in the proposed clause containment learning is to block every unexplored assignment τ2 that selects a set of clauses φ|τ2 containing a set of clauses φ|τ1 previously selected by an explored assignment τ1. To block the assignment τ2, we enforce at least one of the clauses in φ|τ1 to be deselected. Recall that the selection variable sC of clause C valuates to ⊥ if and only if C is deselected. Therefore, a learnt clause, which is the disjunction of the negation of selection variables of clauses in φ|τ1 , is deduced to record this information. The above idea gives rise to the proposed algorithm in Figure 1 to solve E-MAJSAT formulas. (Lines 03,07,08 and 11 describe enhancement techniques of the proposed algorithm, which will be discussed in Section 4.)

SolveEMAJSAT input: Φ = ∃X R Y.φ(X, Y ) output: Pr[Φ] begin 01 ψ(X, S) := (∧C∈φ (sC ≡ ¬CX )) ∧ (∧pure l:var(l)∈X l); 02 prob := 0; 03 s-table := BuildSubsumeTable(φ); 04 while SAT(ψ) = ⊤ 05 τ := the found model of ψ for variables in X; 06 if SAT(φ|τ ) = ⊤ 07 τ ′ := SelectMinimalClauses(φ, ψ); 08 ϕ := RemoveSubsumedClauses(φ|τ ′ , s-table); 09 prob := max{prob, WeightModelCount( R Y.ϕ)}; 10 CS := ∨C∈ϕ ¬sC; 11 CL := DiscardLiterals(φ, CS, prob); 12 else //SAT(φ|τ ) = ⊥ 13 CL := MinimalConflicting(φ, τ); 14 ψ := ψ ∧CL; 15 return prob; end

The algorithm involves two SAT solvers: one works on the matrix φ(X, Y ) of the input formula, and the other works on the selection relation ψ(X, S) for clauses in φ(X, Y ). Using the definition of selection variables, line 01 initializes the selection relation together with asserting the literals of pure X variables. If a variable e in X is pure in φ, assigning the literals of e to ⊤ deselects the clauses containing e, and does not affect other clauses. Because the conditional satisfying probability is greater if less clauses are selected, we can always assert pure X variables.

The selection relation is used to select different assignments τ over X. If φ|τ is satisfiable, a weighted model counter is invoked to compute the conditional satisfying probability Pr[ R Y.φ|τ ] under the assignment τ. The blocking clause CL derived based on the proposed containment learning technique is conjoined with ψ to prevent clauses in φ|τ being simultaneously selected again.

On the other hand, suppose φ|τ is unsatisfiable. We can deduce a conjunction of literals from τ responsible for the conflict by using a SAT solver to analyze the conflict (e.g., using the subroutine analyzeFinal in Minisat [E´en and S¨orensson, 2003a; 2003b]). In general, the conjunction of literals may not be minimal, meaning that some literals can be discarded and the conflict remains unaffected. The subroutine MinimalConflicting makes the conjunction of literals responsible for the conflict minimal as follows. For each literal l in the conjunction, temporarily drop l and check whether φ(X, Y ) is still unsatisfiable. If it is unsatisfiable, discard l; otherwise, keep l in the conjunction. Repeating the above process for every literal makes the conjunction minimal. Complementing the minimal conjunction of literals yields a learnt clause, which is then conjoined with the selection relation to block assignments that make φ unsatisfiable.

When the selection relation becomes unsatisfiable, it indicates that the space spanned by variables X has been completely searched. The algorithm will return the encountered maximum conditional satisfying probability, which equals the satisfying probability of the input E-MAJSAT formula.

We illustrate the working of algorithm SolveEMAJSAT in the following example.

Example 2 Continuing Example 1, we show how algorithm SolveEMAJSAT in Figure 1 (without the enhancement techniques) solves the E-MAJSAT instance Φ = ∃e1e2e3 R 0.5 r1r2r3.φ(X, Y ). Let the first tried assignment τ1 be ¬e1¬e2¬e3, which selects C1, C2. The algorithm derives Pr[ R 0.5Y.φ|τ1 ] = 0.75 by invoking the weighted model counter in line 09. The learnt clause CL = (¬s1 ∨ ¬s2) is conjoined with ψ to prevent C1 and C2 being selected simultaneously again. Suppose the second tried assignment τ2 is ¬e1e2¬e3, which selects C1. The weighted model counter gives Pr[ R 0.5Y.φ|τ2 ] = 0.75, and the learnt clause CL = (¬s1) is conjoined with ψ to prevent C1 being selected again. Let the third tried assignment τ3 be e1e2¬e3, which selects C4. The weighted model counter gives Pr[ R 0.5Y.φ|τ3 ] = 0.5, and the learnt clause CL = (¬s4) is conjoined with ψ to prevent C4 being selected again. Let the fourth tried assignment τ4 be e1e2e3, which selects C3. The conditional satisfying probability Pr[ R 0.5Y.φ|τ4 ] equals 0.75, and the learnt clause CL = (¬s3) is conjoined with ψ to prevent C3 being selected again. Suppose the fifth tried assignment τ5 is e1¬e2e3, which deselects every clause, making φ|τ5 = ⊤ and Pr[ R 0.5Y.φ|τ5 ] = 1. Since there is no selected clause, the learnt clause CL is empty, and the selection relation becomes unsatisfiable after being conjoined with an empty clause. The unsatisfiability of the selection relation reveals that the space spanned by variables X has been exhaustively searched, and the algorithm returns the satisfying probability, which equals 1, of the E-MAJSAT instance.

4 Enhancement Techniques

The computational efficiency of algorithm SolveEMAJSAT is greatly affected by the strength of learnt clauses. We introduce three enhancement methods, minimal clause selection, clause subsumption, and partial assignment pruning, to strengthen the learnt clauses deduced by the proposed learning technique. In Figure 1, the enhancement techniques are executed by subroutines SelectMinimalClauses (in line 07), RemoveSubsumedClauses (in line 08), and DiscardLiterals (in line 11), to be detailed in the following three sections, respectively.

4.1 Minimal Clause Selection

As discussed before, the selection relation ψ(X, S) is in charge of choosing an assignment τ over variables X and thus selects a set of clauses from the matrix φ(X, Y ). However, the set of selected clauses may not be minimal, meaning that it is possible for another assignment τ ′ to select a set of clauses contained in that selected by τ, i.e., φ|τ ′ ⊂ φ|τ . Notice that the length of a learnt clause equals the number of selected clauses. Therefore, selecting fewer clauses gives a stronger learnt clause, as well as a higher conditional satisfying probability. Starting from a set of initially selected clauses φ|τ , the first enhancement technique minimal clause selection decreases the number of selected clauses by making the set of initially selected clauses minimal as follows. The learnt clause is conjoined with ψ(X, S) so that ψ(X, S) is solved under the unit assumption [E´en and S¨orensson, 2003b] to ensure that at least one of the currently selected clauses must be deselected in the future. The above process repeats until the selection relation becomes unsatisfiable.

4.2 Clause Subsumption

The second enhancement technique, clause subsumption, decreases the length of the learnt clause via examining the subsumption relation among the selected clauses. Recall that clause C1 subsumes clause C2 if every literal appears in C1 also appears in C2. Using the lookup table of the subsumption relation computed by subroutine BuildSubsumeTable, the procedure RemoveSubsumedClauses simplifies the set of selected clauses φ|τ by removing subsumed clauses.

4.3 Partial Assignment Pruning

To illustrate the third enhancement technique partial assignment pruning, we first take a closer look at the learnt clause deduced by the proposed clause containment learning. Given a matrix φ(X, Y ) and an assignment τ over X, a learnt clause consists of the negation of the selection variables of the selected clauses. For each selected clause C, if the selection variable sC is substituted by its definition sC ≡ ¬C X , the learnt clause CL becomes the disjunction of the sub-clauses C X , i.e., CL = ∨C∈φ|τ C X .

From the above illustration, we observe that the learnt clause can be strengthened as follows. First, temporarily discard some literal l in the learnt clause. Second, invoke a weighted model counter to compute the conditional satisfying probability contributed by the selected clauses. Third, compare the probability to the current maximum satisfying probability. If the probability is no greater, literal l is discarded; otherwise, it is kept in the clause. Fourth, repeat the above steps for other literals.

Benefiting from the three enhancement techniques, the efficiency of the proposed algorithm is greatly improved, as will be shown in our experiments.

We emphasize two more strengths of the proposed algorithm. First, during the computation, the proposed algorithm keeps deriving lower bounds for the satisfying probability, and the bounds gradually converge to the final answer.

Therefore, in contrast to previous DPLL-based methods like DC-SSAT [Majercik and Boots, 2005], the proposed algorithm can be easily modified to solve approximate SSAT by returning the greatest encountered lower bound upon timeout. Second, the proposed algorithm is efficient in memory usage, since it stores the learnt information compactly via selection variables, and the weighted model counting is invoked on selected clauses, whose sizes are typically much smaller than that of original matrix.

5 Experimental Results

A prototyping program 1 of the proposed algorithm SolveEMAJSAT was implemented in the ABC [Mishchenko, 2005] environment with SAT solver Minisat-2.2 [E´en and S¨orensson, 2003a]. For weighted model counting, we tried Cachet [Sang et al., 2004; 2005], but the overall performance was not satisfactory. Instead, we adopt the well-developed BDD package CUDD [Somenzi, 1998], and weighted model counting of the formula is done by traversing the BDD built from the formula, as proposed in [Darwiche and Marquis, 2002]. The experiments were conducted on a Linux machine with an Intel Xeon 2.1 GHz CPU and 126 GB RAM.

We evaluated the proposed algorithm on both random kCNF and application formulas. We compared the proposed approach to the state-of-the-art SSAT solver DC-SSAT, the maximum model counter MAXCOUNT [Fremont et al., 2017], which relies on the approximate counter APPROXMC [Chakraborty et al., 2016], and the E-MAJSAT solver ComPlan. As ComPlan is not publicly available, we used the CNF-to-d-DNNF compilation time of c2d [Darwiche, 2002], a key step in ComPlan, to estimate the performance of ComPlan. Because MAXCOUNT can only handle randomized quantifiers with probability 0.5, to compare MAXCOUNT against other methods we convert formulas involving randomized quantifiers with probabilities not equal to 0.5 into equivalent ones with all probabilities equal to 0.5 by the conversion method proposed in [Lee and Jiang, 2014].

In the sequel, our proposed approach with all three enhancement techniques enabled, DC-SSAT, MAXCOUNT, and the CNF-to-d-DNNF compiler are referred to as erSSAT, Dc, Max, and c2d, respectively. A runtime limit of 1000 seconds was imposed on each formula, and the symbol "-" denotes timeout. We did not impose a memory limit, but recorded the maximum memory usage during execution.

5.1 Random k-CNF Formulas

The random k-CNF formulas were generated by the cnfgen package [Lauria, 2012]. A collection of 280 formulas were generated with k, i.e., the number of literals in a clause, ranging in {3, 4, 5, 6, 7, 8, 9}, the number of variables ranging in {10, 20, 30, 40, 50}, and clause-to-variable ratio ranging in {k-1, k, k+1, k+2}. Two formulas were generated for each parameter combination. To convert the propositional formulas into E-MAJSAT formulas, half of the variables are existentially quantified, and the rest are randomly quantified with probability 0.5.

1 Available at https://github.com/nianzelee/ssatABC.git

Among the collection of 280 formulas, erSSAT solved 216 instances exactly and computed lower bounds for the rest 64 instances with confidence level 1, while Dc and c2d solved 210 and 209 instances, respectively. On the other hand, Max computed lower bounds for 257 instances with confidence level greater than 0.8. Moreover, the maximum memory usage of erSSAT is two orders (resp. one order) of magnitude less than that of Dc (resp. c2d). As the runtime and memory usage of ComPlan are bounded below by c2d, we conclude that erSSAT has the best performance among compared solvers over random formulas.

5.2 Application Formulas

We collected seven families of application formulas for evaluation. The first two families, Toilet-A and Conformant, are exist-forall-exist quantified QBFs from [Giunchiglia et al., 2005]. We converted them into exist-random-exist SSAT formulas by changing universal quantifiers to randomized ones with probabilities 0.5. The third family Sand-Castle is a probabilistic conformant planning problem, which was encoded as an E-MAJSAT formula in [Majercik and Littman, 1998]. The fourth, fifth, and sixth families are taken from [Fremont et al., 2017], which encode the maximum satisfiability (MaxSat), quantitative information flow (QIF), and program synthesis (PS) problems, respectively, into maximum model counting. The last family is taken from [Lee and Jiang, 2014], which encodes the maximum probabilistic equivalence checking (MPEC) of analyzing the maximum probability for a probabilistic circuit to produce erroneous outputs.

Table 1 shows the results, where benchmarks statistics, including the numbers of variables (#V), clauses (#C), outermost existentially quantified variables (#E1), randomized quantified variables (#R), and innermost existentially quantified variables (#E2), are reported. In the table, runtime information is reported in seconds. For erSSAT, the obtained lower bound (LB), the time (T1) spent to first reach the obtained LB, and the entire runtime (T2), are reported. For Dc, the exact probability (Pr) and runtime (T) are reported. As Dc is an exact SSAT solver, either it terminates and returns an answer, or it times out without producing any information. For Max, the lower bound (LB), confidence level (CL) of LB, and the rumtime (T) are reported. For c2d, the time (T) spent on compiling a formula into d-DNNF is reported. A "-" entry in T, T1, or T2 indicates that the time limit was reached. We note that, if T2 of erSSAT is not a "-", the corresponding LB is the exact answer to the formula. Also the LB values obtained by erSSAT are of confidence level 1.

The results suggest that erSSAT was able to quickly derive tight lower bounds in families Toilet-A, Conformant, Sand-Castle, MaxSat, and MPEC. Specifically, for Toilet-A, erSSAT generally spent less time than Max did to derive the same lower bounds while Max timed out on four larger cases. For Conformant, erSSAT derived lower bounds at the order of 10-1 for all formulas, while Dc, Max, and c2d timed out on most of them. For Sand-Castle, erSSAT exactly solved three formulas, and derived lower bounds greater than 0.99 for the rest. In contrast, Dc and c2d outperformed erSSAT on these instances because they are specially designed for solving probabilistic conformant planning tasks. On the other hand, Max failed in deriving lower bounds for all the formulas. For families QIF and PS, erSSAT did not perform as good as Max due to the fact that the formulas in these two families share the property that only very few assignments to the outermost existentially quantified variables can lead to large satisfying probabilities close to 1. It is not surprising as Max is particularly designed for such formulas.

In terms of memory usage, erSSAT is more efficient than Dc and c2d while Max used the least amount.

5.3 Analysis of Enhancement Techniques

To analyze the effect of the proposed enhancement techniques on computational efficiency, we tested our program under different configurations over random k-CNF formulas. Let the enabled enhancement techniques be indicated by letter m for minimal clause selection, s for clause subsumption, and p for partial assignment pruning. On average, erSSAT-{p} achieved 31% speedup over erSSAT; erSSAT-{m,p} achieved 11% speedup over erSSAT-{p}; erSSAT-{m,s,p} achieved 2% speedup over erSSAT-{m,p}.

For application formulas, the enhancement techniques in general do not produce consistent runtime improvements due to their computational overheads. However they helped in exact solving of more formulas within the timeout limit. The results suggest the benefit of the three enhancement techniques to the efficiency of the proposed algorithm.

6 Conclusions

We developed a new approach to solving E-MAJSAT formulas. In contrast to prior methods based on DPLL search or knowledge compilation, we proposed the clause containment learning technique, inspired by clause selection recently developed in QBF evaluation, and design a novel algorithm to solve E-MAJSAT efficiently. Under the framework of clause containment learning, three enhancement techniques were proposed to improve the computational efficiency. Experiment results show the benefit of our method. For future work, we intend to solve SSAT with general prefix structure.

Acknowledgements

This work was supported in part by the Ministry of Science and Technology of Taiwan under grants 104-2628E-002-013-MY3, 105-2221-E-002-196-MY3, 105-2923-E002-016-MY3, and 106-2912-E-002-002-MY3.