Probabilistic Satisfiability: Logic-Based Algorithms and Phase Transition

1 Introduction

Probabilistic satisfiability (PSAT) is an NP-complete problem that requires the joint application of deductive and probabilistic reasoning. It consists of an assignment of probabilities to a set of propositional formulas, and its solution consists of a decision on whether this assignment is consistent. For example, consider Problem 1.1, in which the goal is to verify the truthfulness of the claims.

Problem 1.1 Three friends usually go to a bar, and every night at least two of them are at their exclusive table. Each of them claims to go to the bar "only" 60% of the nights.

Question: Can they be telling the truth? Why?

In this case, the statement of the friends has to be checked against an established fact, namely the presence of two of them every night. Another instance of PSAT is the following.

Problem 1.2 Selecting architecture students is notoriously hard. Staff at a university analysed students that received their final degrees and concluded that:

• at least 75% had good grades in their Math entrance test or showed good drawing abilities;
• at most a third had good Math grades or did not show any drawing abilities.

Question: Is this consistent with the low expectation (at most 15%) of students that do well in the Math entrance tests?

∗Work supported by Fapesp Project 2008/03995-5 (LOGPROB).

†Partially supported by CNPq grant PQ 302553/2010-0.

This problem involves imprecise probability judgements, widening the scope of application areas. In fact, there is a large number of potential application areas for PSAT, from machine learning to the modelling of biological processes, from hardware and software verification to economics and econometrics. However, there are very few, if any, practical algorithms available, used in limited applications.

This work aims at studying PSAT algorithms 1 to reveal its empiric complexity distribution and, in particular, detect the existence of a phase-transition behaviour.

1.1 A Brief History of PSAT

The original formulation of PSAT is attributed to George Boole [1854]. The problem has since been independently rediscovered several times (see [Hailperin, 1986; Hansen and Jaumard, 2000]) until it was presented to the Computer Science and Artificial Intelligence community by Nilsson [Nilsson, 1986] and was shown to be an NP-complete problem, even for cases where the corresponding classical satisfiability is known to be in PTIME [Georgakopoulos et al., 1988].

The PSAT problem is formulated in terms of a linear algebraic problem of exponential size. The vast majority of algorithms for PSAT solving in the literature are based on linear programming techniques, such as column generation, enhanced by several types of heuristics [Kavvadias and Papadimitriou, 1990; Hansen et al., 1995].

Boole's original formulation of the PSAT problem did not consider conditional probabilities, but extensions for them have been developed [Hailperin, 1986; Hansen et al., 1995; Hansen and Jaumard, 2000; Walley et al., 2004]; the latter two works also cover extensions of PSAT with imprecise probabilities. A few tractable fragments of PSAT were presented [Andersen and Pretolani, 2001]. In this work, however, we concentrate on PSAT's original formulation.

With respect to practical implementations, initial attempts to implement a solution led to the belief that the problem appeared to be very hard [Nilsson, 1993]. There are computational results reported in [Jaumard et al., 1991] and [Kavvadias and Papadimitriou, 1990], solving PSAT problems of 140 variables and 300 sentences. However, these implementations were rarely, if ever, used to solve practical instances of PSAT problems or served as a basis to practical applications.

1 All implementations available at psat.sourceforge.net.

1.2 Phase Transition of NP-complete Problems

Cheeseman et al. [1991] presented the phase-transition phenomenon for NP-complete problems and conjectured that it is a property of all problems in that class. Gent and Walsh [1994] studied phase transition for SAT problems parameterised by the rate m/n, where m is the number of clauses in a 3-SAT instance and n is the number of variables, and showed that the harder instances concentrate around a point where m/n = Pt, the phase transition point. When the rate m/n is small (< 3) almost all instances are satisfiable, and when this rate is high (> 6) instances are unsatisfiable, and the decision time remains low at both cases. At the phase transition point Pt, the number of expected satisfiable instances is 50%, which for 3-SAT is Pt ≈ 4.3.

To the best of our knowledge, no phase transition has been described for PSAT so far.

Very efficient SAT solvers are now available [Moskewicz et al., 2001; E´en and S¨orensson, 2003], but the SAT phase transition behaviour remains independent of implementation and number of atoms. However it relies on presenting the problem in a normal form, usually in clausal form with a fixed number of atoms per clause.

Efficient SAT-solvers enabled the solution of other NPcomplete problems by translating them to a SAT instance and applying the solvers. Cook's theorem guarantees that there exists a polynomial-time translation from any NP-complete problem into SAT. However, no such translation is found in the literature from PSAT to SAT.

1.3 Goals and Organisation of the Paper

The aim of this work is to study logic-based PSAT algorithms and their empiric complexity distribution, looking for a PSAT phase transition behaviour.

For that, we formally present the PSAT problem and develop a logic-based normal form of it in Section 2, based on which two kinds of algorithms are developed. A (canonical) reduction of PSAT to SAT is developed in Section 3. And an efficient SAT-based modification of usual linear programming PSAT algorithms in Section 4. The empiric complexity distribution on both algorithms is presented and PSAT phase transition behaviour is detected. We end with a discussion on what helped the detection of the PSAT phase transition and its efficiency.

2 The PSAT Problem

A PSAT instance is a set Σ = {P (αi) ▷◁i pi|1 ≤ i ≤ k}, where α1, . . . , αk are classical propositional formulas defined on n logical variables P = {x1, . . . , xn}, which are restricted by probability assignments P (αi) ▷◁i pi, ▷◁i ∈ {= , ≤, ≥} and 1 ≤ i ≤ k. Variables are also called atoms.

There are 2n possible propositional valuations v over the logical variables, v : P → {0, 1}; each such valuation is extended, as usual, to all formulas, v : L → {0, 1}. A probability distribution over propositional valuations π : V → [0, 1], is a function that maps every valuation to a value in the real interval [0, 1] such that ∑2n i=1 π(vi) = 1. The probability of a formula α according to distribution π is given by Pπ(α) = ∑{π(vi)|vi(α) = 1}.

Nilsson [1986]'s formulation of PSAT considers a k × 2n matrix A = [aij] such that aij = vj(αi). The probabilistic satisfiability problem is to decide if there is a probability vector π of dimension 2n that obeys the PSAT restriction:

A PSAT instance Σ is satisfiable iff its associated PSAT restriction (1) has a solution. If π is a solution to (1) we say that π satisfies Σ. The last two conditions of (1) force π to be a probability distribution. Usually the first two conditions of (1) are joined, A is a (k + 1) × 2n matrix with 1's at its first line, p1 = 1 in vector p(k+1)×1, so ▷◁1-relation is "=".

Example 2.1 Consider Problem 1.1, with friends {1, 2, 3}. Let xi represent that person i is at the bar tonight, i ∈ {1, 2, 3}. As every night at least two friends are at the bar, no two friends can be absent at the same night, represented by ¬(¬xi ∧ ¬xj ) with 100% certainty for i ̸= j:

Furthermore, each claims to be at the bar "only" 60% of the time:

and the question is if there exists a probability distribution that simultaneously satisfies these 6 probability assignments.

Consider now Problem 1.2. Let x1 mean that a student has good grades in the Math entrance test and x2 mean that that student showed good drawing abilities. In this case, we obtain the restrictions Σ:

Consider a probability distribution π and all the possible valuations as follows.

which jointly satisfies the assignments above, so Problem 1.2 is satisfiable. We are going to study algorithms to compute one such probability distribution if one exists. □

An important result of [Georgakopoulos et al., 1988] guarantees that a solvable PSAT instance has a "small" witness.

Fact 2.2 If a PSAT instance Σ = {P (αi) = pi|1 ≤ i ≤ k} has a solution, then there are k + 1 columns of A such that the system A(k+1)×(k+1)π = p(k+1)×1has a solution π ≥ 0.

The solution given by Fact 2.2 serves as an NP-certificate for this instance, so PSAT is in NP. Furthermore, as propositional satisfiability (SAT) is a subproblem obtained when all pi = 1, PSAT is NP-hard. So PSAT is NP-complete.

It follows from the Cook-Levin Theorem [Cook, 1971] that there must be a polynomial time reduction from PSAT to SAT. However, finding an efficient reduction is neither obvious nor easy. In the following, we study some logical properties of PSAT instances to study ways in which this kind of reduction can be performed.

First, some notation. If A is an m×n matrix, Aj represents its j-th column, and if b is an m-dimensional column, A[j := b] represents the matrix obtained by substituting b for Aj ; if A is square matrix, |A| is A's determinant. If A is a {0, 1}- matrix, where each line corresponds to a variable, than each Aj can be seen as valuation.

2.1 A PSATNormal Form

We say that a PSAT instance Σ = {P (αi) ▷◁i pi|1 ≤ i ≤ l} is in (atomic) normal form if it can be partitioned in two sets, 〈Γ,Ψ〉, where Γ = {P (αi) = 1|1 ≤ i ≤ m} and Ψ = {P (yi) = pi|yi is an atom, 1 ≤ i ≤ k}, with 0 < pi < 1, where l = m+ k. The partition Γ is the SAT part of the normal form, usually represented only as a set of propositional formulas and Ψ is the atomic probability assignment part.

By adding a small number of extra variables, any PSAT instance can be brought to normal form.

Theorem 2.3 (Normal Form) For every PSAT instance Σ there exists an atomic normal form instance 〈Γ, Ψ〉 such that Σ is a satisfiable iff 〈Γ, Ψ〉 is; the atomic instance can be built from Σ in polynomial time. □

Example 2.4 The presentation of Problem 1.1 in Example 2.1 is already in normal form, with Γ = {x1 ∨ x2, x1 ∨ x3, x2 ∨ x3} and Ψ = {P (x1) = P (x2) = P (x3) = 0.6}. This indicates that the normal form is a "natural" form in many cases, such as when one wants to confront a theory Γ with the evidence Ψ.

For the formulation of Problem 1.2, we start by rewriting the problem in the form P (α) ≤ p as

Add three new variables, y1, y2, y3 and make

The normal form allows us to see a PSAT instance 〈Γ,Ψ〉 as an interaction between a probability problem Ψ and a SAT instance Γ. Solutions to the instance can be seen as solutions to Ψ constrained by the SAT instance Γ.

This is formalised as follows. A valuation v over y1, . . . , yk is Γ-consistent if there is an extension of v over y1, . . . , yk, x1, . . . , xn such that v(Γ) = 1.

Lemma 2.5 A normal form instance 〈Γ,Ψ〉 is satisfiable iff there is a (k + 1) × (k + 1)-matrix AΨ, such that all of its columns are Γ-consistent and AΨπ = p has a solution π ≥ 0.

In Lemma 2.5, a line is added to represent ∑i πi = 1, π a distribution over k+1 Γ-consistent valuations. This the basis for the PSAT solving algorithms that present next.

3 Reduction of PSAT to SAT

A (canonical) reduction is a polynomial time translation of an instance of PSAT into an instance of SAT, such that the PSAT instance is satisfiable iff the SAT instance is. As both PSAT and SAT are NP-complete, the existence of a reduction is guaranteed.

We present a reduction that inputs a normal form PSAT instance 〈Γ,Ψ〉 and outputs a SAT formula that encodes Lemma 2.5. Given p (here presented as Ψ), we search for a matrix A(k+1)×(k+1) whose columns are Γ-consistent and a probability distribution π ≥ 0 such that Aπ = p. We assume that the elements of p and π are represented by a fixed point number in binary positional system with precision bπ bits, where each bit is a boolean variable, the higher the bit's index the higher its significance. As aij, πi1 j1 , pi2 j2 ∈ {0, 1}, each such element is represented by a boolean variable. This is represented by the following schema.

3.1 Determining the Precision

The hard part of this encoding is to find a large enough precision bπ that guarantees the correctness and polynomial size of the encoding, assuming a fixed number of bits in the input.

To guarantee a polynomial time reduction, the number of bits bπ in which the components of vector π are encoded has to be bounded by a polynomial on the size of input of the PSAT instance. By Cramer's rule, πj = |A[j:=p]| |A| so we estimate the maximum precision bπ as twice the number of bits of the maximum possible determinant of a 0, 1-matrix A. For that, we use a result due to J. Hadamard who solved the Maximum Determinant Problem; see [Garling, 2007].

Thus bπ = 2 (⌈ k+2 2 log(k +2)⌉ - (k + 1)) = O(k log k), and the reduction is polynomial-time. This bound presupposes rational arithmetic; correctness is kept in the presence of truncation errors due to the convexity of the solution space.

3.2 The SAT Instance

Multiplication of aij · πj is encoded as a simple conjunction of each bit-variable of πj with the variable representing aij. Sums will be directly encoded as bitwise sums for each position, which demands a carry-bit and a result-bit for each position. Equality is encoded as bitwise equivalence. Due to space reasons we do not detail the reduction formulas here.

We only point that the number of variables in the clausal SAT instance is O(k3 log k) and that the number of clauses is also O(k3 log k), where k = |Ψ|.

This implies that reduction makes PSAT solving a lot less efficient than SAT solving, both if P = NP or if P ̸= NP !

3.3 Results: A PSAT Phase Transition

A translation of PSAT instances into SAT was implemented in C++, which invoked the zchaff SAT solver [Moskewicz et al., 2001]. We generate uniformly distributed random PSAT instances in normal form with k probability assignments, n variables y1, . . . , yk, xk+1, . . . , xn and m 3-SAT clauses. To restrict complexity, we fixed |Ψ| = k = 4 which leads to bπ = 2(⌈(6 log 6)/2⌉ - 5) = 6. We also fixed n = 40 and increased the rate m/n in steps of 0.2. For each value of m, we generated 100 instances of PSAT, and computed the percentage of satisfiable instances (%SAT) and the average time of computation in seconds. We then obtained the graphic illustrated in Figure 1.

Figure 1 clearly illustrates a phase transition behaviour, with the transition point around 4. We know that when k = 0, PSAT becomes SAT, with phase transition point around 4.3. As k is increased, it is expected that the rate of satisfiable formulas decreases for a given m/n, so the phase transition point is supposed to dislocate to the left, as observed. With more experiments, we could increase k and expect the phase transition point to move even further to the left. However, due to the high complexity of the translation, experiments with k = 6 were almost impractical around the transition point. This is why we turn to other algorithms for PSAT solving.

4 A Logic-Algebraic PSAT Solver

Traditional algebraic PSAT solvers extend an exponentially large linear program with m + k + 1 new variables (since m clauses in Γ have probability 1) of the form

which is solved iteratively by the simplex algorithm; at each iteration step i, Fact 2.2 allows for storing A(i) with m+k+1 columns and a column generation method is employed in which an auxiliary problem generates a column that replaces some column in A(i) and decreases the objective function. Vector c selects only the new variables in π, so c′π = 0 iff the PSAT problem is satisfiable. Figure 2 presents the results of an implementation of this method for exactly the same instances of Figure 1, showing no phase transition and much greater decision times, mainly explained by each formula α ∈ Γ having to be dealt with a restriction P (α) = 1.

We propose the following logic-based modifications of that method that inputs a normal form PSAT instance, with

• (a) a much smaller basis A(i) of order k + 1, by Lemma 2.5;
• (b) a different initial feasible solution at step 0;
• (c) a new objective function;
• (d) a new SAT-based auxiliary problem.

We now detail (b), (c) and (d) and present our algorithm. We first establish some terminology. A matrix A that satisfies conditions (3) is a feasible solution for Ψ.

We will further assume that the input probabilities p1, . . . , pk in (3) are in decreasing order. By Lemma 2.5, 〈Γ,Ψ〉 has a solution iff there is a partial solution A satisfying (3) such that if πj > 0 then a1,j, . . . , ak,j are Γ-consistent valuations for 1 ≤ i ≤ k, 1 ≤ j ≤ k + 1. We usually abuse terminology calling Aj a Γ-consistent column.

4.1 Initial and Further Feasible Solutions

Given 〈Γ,Ψ〉, consider 〈∅,Ψ〉 obtained by ignoring Γ. As the elements of p are in decreasing order, consider the {0, 1}- matrix I ∗ = [ai,j]1≤i,j≤k+1 where ai,j = 1 iff i ≤ j, that is, I ∗ is all 1's in and above the diagonal, 0's elsewhere. As p is in decreasing order, I ∗ satisfies 〈∅, Ψ〉 and is called a relaxed solution for 〈Γ,Ψ〉. Clearly, I ∗ is a feasible for Ψ.

Example 4.1 The relaxed solution to normal form of Problem 1.2 in Example 2.4 is such that all columns are Γconsistent, this decides positively Problem 1.2 by Lemma 2.5.

The relaxed solution is the initial feasible solution of our method. Further feasible solutions are obtained by generating new {0, 1}-columns and substituting them into a feasible solution, as shown by the following.

Lemma 4.2 Let A be a feasible solution satisfying (3) and let b = [1 b1 · · · bk]′ be a {0, 1}-column. Then there always exists a column j such that A[j := b] is a feasible solution. □

Lemma 4.2 is a well-known fact that comes from the pivoting in the simplex algorithm. Its proof actually gives us an algorithm to compute a new feasible solution from a previous one, so let merge(A, b) be a function that computes it.

Our method moves through feasible solutions, at each step generating a column b that decreases the value of the objective function.

4.2 The Objective Function

In a feasible solution A such that Aπ = p and π ≥ 0, some columns may not be Γ-consistent. Let J = {j|Aj is Γ-inconsistent and πj > 0}; J is the set of column indexes in A corresponding to Γ-inconsistent columns with non-null associated probability; clearly |J| ≤ k + 1. If J = ∅, we call A a (total) solution.

By Lemma 2.5, a positive decision for the PSAT instance 〈Γ,Ψ〉 is reached iff J = ∅. Thus, a candidate objective function is simply |J|. Lemma 4.2 guarantees that if we only generate Γ-consistent columns, |J| never increases. However, it is not guaranteed that, if a solution exists, we can find a path in which |J| decreases at every step s. If this were true, we would have a solution in at most k + 1 steps, which is unfortunately not the case.

A second candidate objective function is the sum of probabilities of Γ-inconsistent columns, f = ∑j∈J πj . Note that f and |J| become 0 at the same time, which occurs iff a positive decision is reached. The simplex algorithm with appropriate column generation ensures that, if there is a solution, it can be obtained with finitely (but possibly exponentially) many steps of non-increasing f-values. We propose a combined objective function 〈|J|, f〉 ordered lexicographically. In minimising this combined objective function, we first try to minimise the number of Γ-inconsistent columns; if this is not possible, then minimise f, keeping J constant. We thus have the following program

So the PSAT instance 〈Γ, Ψ〉 associated to program (4) is satisfiable iff the objective function is minimal at 〈0, 0〉.

Assume there is a function GenerateColumn(A, p, Γ), presented at Section 4.3, that generates a Γ-consistent column that decreases the objective function, if one exists; otherwise it returns an illegal column of the form [-1 · · · ]. Algorithm 4.1 presents a method that decides a PSAT instance by solving problem (4).

Algorithm 4.1 starts with a relaxed solution for 〈Γ,Ψ〉 (line 2), and via column generation (line 4) generate another feasible solution (line 6), decreasing the objective function, until either the search fails (line 5) or a solution is found; the latter only occurs with the termination of the loop in lines 38, when the objective function reaches 〈0, 0〉.

4.3 SAT-Based Column Generation

A Γ-satisfiable column b that never increases the value of the objective function is obtained by solving at most k + 1 SAT problems as follows. Consider x1, . . . , xk over {0, 1} and

where a1, . . . , ak, c ∈ Q; (5) can be seen as a propositional formula LR, in the sense that a valuation v : xi ↦→ {0, 1} satisfies LR iff v makes (5) a true condition. Such a formula ΔLR can be obtained from LR in time O(k) [Warners, 1998].

Suppose 1, . . . , q ≤ k+1 are the Γ-inconsistent columns of feasible solution A. First, we try to eliminate a Γ-inconsistent Algorithm 4.1 Logic-algebraic PSAT solver

Input: A normal form PSAT instance 〈Γ, Ψ〉.

Output: Total solution A; or "No", if unsatisfiable.

• 1: p := sortDecrescent({1} ∪ {pi|P (yi) = pi ∈ Ψ};
• 2: A(0) := I ∗ ; s := 0; compute 〈|J(s)|, f(s)〉;
• 3: while 〈|J(s)|, f(s)〉 ̸= 〈0, 0〉 do
• 4: b(s) = GenerateColumn (A(s) , p, Γ);
• 5: return "No" if b(s) 1 < 0; /* instance is unsat */
• 6: A(s+1)=merge(A(s), b(s) );
• 7: increment s; compute 〈|J(s)|, f(s)〉;
• 8: end while
• 9: return A(s); /* PSAT instance is satisfiable */

column Aj associated to πj > 0. By linear algebraic manipulation, a new column b = [1 y1 . . . yk]′ to substitute Aj must satisfy the set of linear inequalities:

A substitution b for Aj is obtained by a valuation that satisfies the formula Θj = Γ ∧ ∧k+1 i=1 ΔLRij . Clearly, if Θj is satisfiable, A[j := b] is Γ-consistent and decreases |J|.

Suppose every Θj is unsatisfiable, 1 ≤ j ≤ q, and let fπ = ∑qj=1 πj. A column b = [1 y1 . . . yk]′ that substitutes some Aj and enforces a decreasing fπ similarly satisfies

A substitution b for Aj is obtained by a valuation that satisfies the formula Θf = Γ ∧ ΔLRf . If Θf is satisfiable, A[j := b] is Γ-consistent and fπ never increases.

The algorithm that computes GenerateColumn(A, p, Γ) faster in practice is as follows. First, send Θf(y1, . . . , yk) to a SAT-solver. If it is unsatisfiable, return invalid column [-1 0 . . . 0]′ ; in this way we have an early failure. Otherwise there is a vf , vf(Θf) = 1. If bf = [1 vf(y1) . . . vf (yk)]′ substitutes some Γ-inconsistent column, return bf , which decreases |J| and maybe f as well. Otherwise store bf . For each Γ-inconsistent Aj submit Θj(y1, . . . , yk) to a SATsolver; if it is satisfiable with valuation v, return b = [1 v(y1) . . . v(yk)]′ , decreasing |J|. If all Θj are unsatisfiable, return bf , so f does not increase. As the SAT solver is deterministic and generates answers in a fixed order, by Bland's rule the termination of the whole process is guaranteed.

Example 4.3 Apply Algorithm 4.1 to the presentation of Problem 1.2 in Example 2.4. At step 0, the relaxed solution

is such that the two columns on the left are Γ-inconsistent. Column generation tries to substitute the column 1, generating the inequalities -y1 + y2 ≥ 0, y2 - y3 ≤ 0, 3y1 + 2y3 ≤ 3, y1 ≤ 0 which, when translated to logic and input to a SAT solver jointly with Γ produces the valuation y1 = 0, y2 = 1, y3 = 1. At step 1, we substitute column 1 by [1 0 1 1]′ ,

Now only column 2 is Γ-inconsistent; Θf produced by column generation is unsatisfiable Θf and so is the problem. That is, the drunks are lying. □

4.4 Results: Another PSAT Phase Transition

We implemented Algorithm 4.1 in C++, also employing the zchaff SAT solver, thus obtaining a much faster PSAT solver. We generated uniformly distributed normalised random PSAT instances in normal form with k probability assignments, n variables y1, . . . , yk, xk+1, . . . , xn and m 3SAT clauses. We obtained the graphic illustrated in Figure 3 by fixing k = 12, n = 150, m/n increases in steps of 0.1 and 200 PSAT instances for each value of m.

Again, Figure 3 displays an unequivocal phase transition behaviour, with a phase transition point at Pt ≈ 3.9. The phase transition behaviour can be credited to the use of PSAT normal form and to the fact that, unlike in program (2), only Γ-consistent columns were generated in a small basis of size k + 1. The increase in efficiency is mainly due to the small basis, and also to the use of an efficient SAT solver to and to the smaller size of formulas submitted to the SAT solver than in the reduction algorithm.

By generating large instances over the "flat zones" of Figure 3, we were able to obtain a satisfiable instance with n = 400,m = 400, k = 50 and decision time 0.76s; and an unsatisfiable instance with n = 200,m = 800, k = 100 and decision time 29.4s. This gives an idea of the capabilities of the method.

5 Conclusion

We have shown that a combination of logic and algebraic techniques can be very fruitful to the study of algorithms of PSAT solvers. The logic part appear to be crucial to reveal a phase transition behaviour in this case.

Further work involves the exploration of efficient PSAT fragments using the algorithm and techniques developed here, and the study of PSAT-based methods and applications that employ the algorithms presented here.