Classical Generalized Probabilistic Satisfiability

1 Introduction

The starting point of a deep analysis of the propositional satisfiability (SAT) problem was due to Cook in [Cook, 1971], where it was shown that this problem is NP-complete. Given its simplicity and expressiveness, the SAT problem has become the standard NP-complete problem to study and, because of that, SAT solvers became extremely efficient. Due to this, several extensions and generalizations have been developed, taking advantage of the referred solvers. An example of this is the satisfiability modulo theories problem (SMT) [De Moura and Bjørner, 2011] where instead of working in propositional logic, one tries to decide if a formula is valid in some specific first-order theory. This area has had a great impact in industry, especially in hardware and software verification. One other direction for generalization of propositional satisfiability consists in the introduction of probabilities into the classical reasoning, allowing one to express quantitative assertions about propositional formulas.

∗Work done under the scope of Project UID/EEA/50008/2013, financed by the applicable financial framework (FCT/MEC through national funds and when applicable co-funded by FEDER-PT2020) and partially supported by Fundac¸˜ao para a Ciˆencia e a Tecnologia by way of grant UID/MAT/04561/2013 to Centro de Matem´atica, Aplicac¸ ˜oes Fundamentais e Investigac¸˜ao Operacional of Universidade de Lisboa (CMAF-CIO). AM was supported by FCT under the grant SFRH/BD/77648/2011 and by the Calouste Gulbenkian Foundation under Programa de Est´ımulo `a Investigac¸ ˜ao 2011. FC acknowledges the support from the DP-PMI and FCT (Portugal) through scholarship SRFH/BD/52243/2013. CC acknowledges the support of EU FP7 Marie Curie PIRSES-GA-2012-318986 project GeTFun: Generalizing Truth-Functionality.

Filipe Casal

Andreia Mordido

INOV INESC Inovac¸ ˜ao, Portugal andreia.mordido@inov.pt

CMAF-CIO, Portugal DMath, Instituto Superior T´ecnico Universidade de Lisboa, Portugal filipe.casal@tecnico.ulisboa.pt

In this sense, there was an effort to extend propositional logic in order to handle probabilistic reasoning. Fagin et al. [Fagin et al., 1990] developed a widely used probabilistic logic and showed that its satisfiability problem is NPcomplete. Recently, several satisfiability solvers were proposed for fragments of this probabilistic logic. Finger and Bona developed a PSAT solver [Finger and Bona, 2011; 2015] in the context of the probabilistic satisfiability problem (PSAT) [Boole, 1853; Nilsson, 1986], which consists in deciding the satisfiability of a set of assignments of probabilities to propositional formulas. Afterwards, the PSAT problem was generalized to handle Boolean combinations of assignments of probabilities to propositional formulas leading to GPSAT in [Bona et al., 2015]. After that, in [Caleiro et al., 2016a], Caleiro et al. introduced the generalized probabilistic satisfiability problem (GenPSAT) which consists in deciding the satisfiability of linear inequalities involving probabilities of classical propositional formulas. Given this, it is only natural to think about the extension of this problem to Boolean combinations of probabilistic formulas. This is our goal for this paper: extend the GenPSAT problem to allow Boolean combinations of probabilistic formulas as well as present a solver for this more expressive problem.

In this paper, we present the classical generalized probabilistic satisfiability problem GGenPSAT, which consists in deciding the satisfiability of Boolean combinations of linear inequalities involving probabilities of classical propositional formulas. This problem was proved to be NP-complete in [Fagin et al., 1990]. We stress that the formulas expressible in GGenPSAT are precisely the formulas in the probabilistic logic by Fagin et al. We develop an algorithm for the GGenPSAT problem by constructing a polynomial reduction to the quantifier-free theory of linear integer and real arithmetic (QF LIRA) [Barrett et al., 2016; King, 2014]. We also provide an implementation of the algorithm and study its phase transition behavior.

As the main contribution of this work, we develop the theoretical framework that allows the translation between GGenPSAT and SMT problems, which then allows the implementation of a provably correct solver for GGenPSAT. With the GGenPSAT solver in hands, we are able to detect and study the phase transition behavior.

This paper is outlined as follows: in Section 2 we recall some basic notions on probabilistic satisfiability; in Section 3, we introduce the GGenPSAT problem; in Section 4, we present the polynomial reduction to SMT and prove the correctness of the algorithm; in Section 5, we describe the implemented tool and study the phase transition behavior of the GGenPSAT problem; finally, Section 6 concludes the paper and discusses avenues for further research.

2 Preliminaries

Let us begin by fixing a set of propositional variables P = {x1, . . . , xn}. The set of classical propositional formulas is defined, as usual, by

A propositional literal is either a propositional variable or its negation. A propositional clause is a non-empty disjunction of one or more propositional literals. A propositional valuation is a map v : P → {0, 1}, which is extended to propositional formulas as usual. A set of valuations V satisfies a propositional formula φ if, for each v ∈ V, v(φ) = 1. This notion is naturally extended to sets of propositional formulas. Let V ∗ = {v1, . . . , v2n} be the set of all valuations defined over variables of P. We define a probability distribution π over V ∗ as a probability vector of size 2n .

We recall from [Fagin et al., 1990] the set of probabilistic atoms (used herein to define probabilistic formulas) composed by linear inequalities of probabilities of propositional formulas with rational coefficients:

The set of probabilistic formulas is defined as a Boolean combination of probabilistic atoms as follows:

Observe that the other relational symbols {<,>,≤,=, ̸=} can be defined by abbreviation, as well as the logical connectives →, ∨, ↔.

To interpret probabilistic formulas, we consider a probability distribution π over V ∗ . The satisfaction relation is inductively defined as:

• π ⊩ ¬δ iff π ̸⊩ δ;
• π ⊩ δ1 ∧ δ2 iff π ⊩ δ1 and π ⊩ δ2,

where δ, δ1, δ2 ∈ Prob, q, qi ∈ Q and φi ∈ LCPL where i ∈ {1, . . . , ℓ}. A probability distribution π satisfies δ ∈ Prob if π ⊩ δ and satisfies a set of probabilistic formulas if it satisfies each one of them.

2.1 The PSAT Problem

A simple probabilistic formula is a probabilistic formula of the form Pr(c) ▷◁ q where q ∈ Q, 0 ≤ q ≤ 1, ▷◁ ∈ {=, ≤, ≥} and c ∈ LCPL is a propositional clause. Note that a probability distribution π satisfies a formula Pr(c) ▷◁ q if

We now recall the PSAT problem [Nilsson, 1986; Georgakopoulos et al., 1988; Finger and Bona, 2011].

Definition 1 (PSAT problem). Given a set of propositional variables P and a set of simple probabilistic formulas Σ = {Pr(ci) ▷◁ pi | 1 ≤ i ≤ k}, the Probabilistic Satisfiability problem (PSAT) consists in determining whether there exists a probability distribution π over V ∗ that satisfies Σ.

The PSAT problem for {Pr(ci) ▷◁i pi | 1 ≤ i ≤ k} can be formulated algebraically as the problem of finding a solution π for the system of inequalities

where V is the k × 2n matrix such that Vij = vj(ci), i.e., Vij = 1 iff the j-th valuation satisfies the i-th clause, p = [pi] is the k vector of all pi and ▷◁= [▷◁i] is the k vector of all ▷◁i.

A SAT problem can be modeled as a PSAT instance where the entries pi of the probability vector are all identical to 1. The PSAT problem was shown to be NP-complete [Georgakopoulos et al., 1988; Fagin et al., 1990], even when the clauses consist of the disjunction of only two literals, 2PSAT.

2.2 The GenPSAT Problem

In [Caleiro et al., 2016a], probabilistic satisfiability was extended to handle linear inequalities involving assignments of values to propositional formulas.

An instance of GenPSAT is a pair (Γ,Σ) where Γ is a set of propositional clauses (also called hard constraints) and Σ is a set of probabilistic atoms (soft constraints). We say that a probability distribution π satisfies a GenPSAT instance (Γ,Σ) if it satisfies the set of probabilistic atoms

Definition 2 (GenPSAT problem). Given a GenPSAT instance (Γ,Σ), the Generalized Probabilistic Satisfiability problem (GenPSAT) consists in determining if there exists a probability distribution π over V ∗ that satisfies (Γ, Σ).

3 The GGenPSAT Problem

We now aim to extend the GenPSAT problem in order to cope with Boolean combinations of probabilistic atoms.

An instance of GGenPSAT is a pair (Γ,Ψ) where Γ is a set of classical propositional formulas (also called hard constraints) and Ψ is a set of probabilistic formulas (soft constraints). We say that a probability distribution π satisfies a GGenPSAT instance (Γ, Ψ) if it satisfies the set of probabilis-

Despite the similarities between a GenPSAT and a GGenPSAT instance, the latter allows more expressive probabilistic formulas by allowing Boolean combinations of probabilistic atoms.

Definition 3 (GGenPSAT problem). Given a GGenPSAT instance (Γ,Ψ), the Classical Generalized Probabilistic Satisfiability problem consists in determining if there exists a probability distribution π over V ∗ that satisfies (Γ, Ψ).

GGenPSAT extends the scope of PSAT and GenPSAT by dealing with Boolean combinations of probabilistic formulas. In this way, we are not only able to assign values to probabilities of propositional variables or linear inequalities involving them, but also able to express powerful probabilistic assertions. For instance, we can easily model and reason about a framework where a variable x is either true or false with probability 1 but we do not know which is the case:

In this way, we can, in a sense, model the universal quantification of propositional formulas. To notice the impact of this generalization on the available models of a formula, consider the following example.

Example 1. Consider a game of Odds and Evens where players A and B play x, y ∈ Z2, respectively, and player A wins iff x ⊕ y = 0. We can easily study the effectiveness and existence of strategies for this game in GGenPSAT: the term Pr(¬(x ⊕ y)) represents the probability that player A wins the game; with this, we can determine that there is a strategy in which player B wins sometimes, Pr(x ⊕ y) > 0, and that player A wins twice as much as player B, Pr(¬(x ⊕ y)) ≥ 2 · Pr(x ⊕ y) by checking the satisfiability of such formulas.

However, if we additionally assume that player A always plays 0, Pr(x) = 0, and that player B always plays the same, Pr(y) = 0∨Pr(y) = 1, then the above formulas are no longer satisfiable.

In these examples, we studied the existence of strategies by determining the satisfiability of formulas. Additionally, we could also determine if some strategies are always better than others, by determining if a certain formula is valid. ♢

A GenPSAT instance is also a GGenPSAT instance.

Notice that GGenPSAT has been studied in the context of the decision problem for the probabilistic logic introduced by Fagin, Halpern and Megiddo in [Fagin et al., 1990]. Hence, the computational complexity of this problem is known and addressed in the following theorem.

Theorem 1 ([Fagin et al., 1990]). GGenPSAT is NPcomplete.

4 Reducing GGenPSAT to Satisfiability Modulo Theories

Our goal now is to effectively build a decision procedure for this problem. In [Caleiro et al., 2016a], Caleiro et al. constructed an effective procedure for the GenPSAT problem by a polynomial reduction to Mixed-Integer Programming (MIP). However, in that framework, one cannot handle Boolean combinations of linear inequalities, at least intuitively. A framework where this problem is naturally expressed is in Satisfiability Modulo Theories (SMT) with respect to the theory of Quantifier-Free Linear Integer and Real Arithmetic, QF LIRA, which is also in NP [Barrett et al., 2016; King, 2014]. We will now explore the NPcompleteness of GGenPSAT and provide a polynomial reduction to QF LIRA. The variables of the theory can be of one of three sorts: Boolean, integer or real, and the signature is composed of the function symbols F={0, 1,+, ·} and the usual predicates P={≥,≤,<,>,=, ̸=}. The atoms of the theory are either Boolean variables or linear inequalities involving real and integer variables.

We explore some preliminary steps that lead to an algorithm to solve the GGenPSAT problem.

On the details of the GGenPSAT instance: Assume we are given a GGenPSAT instance (Γ,Ψ), where Γ is a set of classical propositional formulas (hard constraints), Γ = {φ1, . . . , φk}, and Ψ is a set of probabilistic formulas (soft constraints), Ψ = {δ1, . . . , δs}. Recall that a formula δj is a Boolean combination of probabilistic atoms of the form

When ghosts attack: Driven by GenPSAT and PSAT developments, it is simpler to deal with probabilities of propositional variables than with probabilities of propositional formulas. To this end, we introduce propositional ghost variables which will represent the propositional formulas occurring inside the probabilistic formulas. Let us define the set of fresh variables that will be used. For this purpose, collect in InsidePr(δ) ⊆ LCPL all the propositional formulas occurring inside the probabilistic formula δ ∈ Prob, which is defined inductively on the structure of δ:

• InsidePr(q1·Pr(ψ1)+. . .+qℓ·Pr(ψℓ) ▷◁ q) = {ψ1, ..., ψℓ};
• InsidePr(¬δ) = InsidePr(δ);
• InsidePr(δ1 ∧ δ2) = InsidePr(δ1) ∪ InsidePr(δ2).

This notion is extended for a set ∆ of probabilistic formulas as usual, InsidePr(∆) = ∪δ∈∆ InsidePr(δ). According to this, and recalling that the propositional formulas in Γ need to be satisfied with probability 1, we consider the set of relevant propositional formulas, RelF defined by:

Consider the set of propositional ghost variables corresponding to each element of RelF:

Furthermore, we will use the real [0, 1]-variable αψ to represent the probability of ψ ∈ RelF.

For ease of notation, we denote by Gi the i-th element of G and ψi the corresponding propositional formula in RelF. We also denote by |G| the cardinality of a set G. The set of propositional variables of interest is B = P ∪ G.

Algebraic formulation: Motivated by the algebraic formulation of PSAT and GenPSAT, we express the probabilistic assertions about the elements in RelF algebraically as follows:

where:

• V = [Vij] is a matrix of size |G|×2n , where Vij is defined from the j th valuation vj ∈ V ∗ and from the ith propositional ghost variable Gi, by Vij = vj(ψi);
• π = [πj] is a vector of size 2n , where each πj is a real [0, 1]-variable representing the probability valuation vj ;
• α = [αi] is a vector of size |G| and each αi is a real [0, 1]- variable that represents the probability of ψi.

Using the following Lemma by Chv´atal [Chv´atal, 1983], we can take a step forward in the choice of the right valuations.

Lemma 1 ([Chv´atal, 1983; Fagin et al., 1990]). If a system of ℓ linear inequalities with integer coefficients has a nonnegative solution, then it has a nonnegative solution with at most ℓ positive entries.

Lemma 1 tells us that a systemwith |G|+1 linear inequalities has a solution iff it has a solution with |G|+1 nonnegative entries. Furthermore, if a GGenPSAT instance is satisfiable then system (3) has a solution. Let us collect in H = [hij ], the |G|+1 columns of V given by Lemma 1, where h|G|+1,j = 1 for each j, and consider the corresponding probability assignments in π:

When variables multiply: Inspired by the previous arguments, we consider |G| +1 copies of each propositional variable of interest in B. Each copy is intended to represent the valuations underlying the columns of matrix H. We represent them by

We extend this notation to propositional formulas as expected - given a propositional formula ψ, ψ(k) represents the formula ψ where each of its variables x was replaced by its appropriate copy, x(k) . Denote by ˜ B = ∪|G|+1 k=1 B(k) the set of all copies of all propositional variables.

Probabilistic formulas seen as linear restrictions: To handle probabilistic formulas in the QF LIRA formalism, we make use of linear inequalities. Since the variable αψ represents the probability of each ψ ∈ InsidePr(Ψ), we can represent a probabilistic atom q1·Pr(ψ1)+. . .+qℓ ·Pr(ψℓ) ▷◁ q as a linear arithmetic formula of the form q1 ·αψ1 +. . .+qℓ ·αψℓ ▷◁ q. This translation, denoted by PrToLIRA, can be inductively extended to probabilistic formulas (which are Boolean combinations of probabilistic atoms):

• PrToLIRA(q1 · Pr(ψ1) + . . . + qℓ · Pr(ψℓ) ▷◁ q) is the assertion q1 · αψ1 + . . . + qℓ · αψℓ ▷◁ q;
• PrToLIRA(¬δ) is the assertion ¬PrToLIRA(δ);
• PrToLIRA(δ1 ∧ δ2) is the assertion PrToLIRA(δ1) ∧ PrToLIRA(δ2).

All together now: To verify the satisfiability of the GGenPSAT instance, we will need to satisfy the following constraints:

All these restrictions amount to:

• 3 assertions from (hard constr), (soft constr) and (sums1);
• 2 · |G| · (|G| + 1) assertions from (cons) and (val2);
• 2 · |G| assertions from (val1) and (prop prob).

Hence, we have a total of O(|G| · (|G| + 1)) assertions, each of polynomial size on the length of (Γ, Ψ) over:

• |G| · (|G| +1) binary variables hij;
• |G| · (|G| +1) real variables bij;
• |G| real variables 0 ≤ αψi ≤ 1;
• |G| + 1 real variables 0 ≤ πj ≤ 1;
• (|G| + 1) · (|G| + n) propositional variables in ˜ B.

With this, we can conclude that the presented procedure translates a GGenPSAT instance into a problem in QF LIRA of polynomial size.

The solver: We test the satisfiability of a GGenPSAT instance (Γ,Ψ) by translating it to a QF LIRA problem and then solving the latter appropriately. The procedure presented in Algorithm 1, begins by initializing an empty QF LIRA problem and uses the following auxiliary procedures:

• assert(·) introduces an assertion to the QF LIRA problem;
• PrToLIRA(·) translates probabilistic formulas into QF LIRA assertions;
• qf lira solver() returns SAT or UNSAT depending on whether the problem is satisfiable or not.

When the resulting QF LIRA problem is satisfiable, we conclude that (Γ, Ψ) is a satisfiable GGenPSAT instance.

Algorithm 1 GGenPSAT solver based on SMT-QF LIRA

Proposition 1. A GGenPSAT instance (Γ,Ψ) is satisfiable iff Algorithm 1 returns Sat.

Proof. Assume that a GGenPSAT instance (Γ,Ψ) is satisfiable. Then, there exists a probability distribution ρ over the set of valuations V ∗ satisfying (Γ, Ψ). Our goal is to present a model for the QF LIRA problem obtained by the translation of (Γ,Ψ) describe above. We denote the obtained solutions by α∗ψ , π∗ j , b∗ij and h∗ij and construct a valuation ˜ v over the extended set of propositional variables ˜ B.

For each pψ ∈ G, let α∗ψ be the probability of the propositional variable pψ induced by the probability distribution ρ in the following manner:

Then, consider the algebraic formulation as in (3):

where now the vector α∗ = [α∗ψi ] is defined as in (5) and

• V = [Vij] is a matrix of size |G|×2n , where Vij is defined from the j th valuation vj ∈ V ∗ and from the ith propositional ghost variable Gi, by Vij = vj(ψi);
• π = [πj] is a vector of size 2n , where each πj is a real [0, 1]-variable representing the probability valuation vj .

Note that ρ∗ = [ρj] where ρj = ρ(vj) is a solution for (6). By Lemma 1, there exists a matrix H = [h∗ij ] composed by |G| + 1 columns of V such that

where h∗|G|+1,j = 1 for each j and π∗ corresponds to the appropriate entries of ρ∗ .

Since π∗ is also a probability distribution, the assertion (sums1) is satisfied and, considering b∗ij = h∗ij · π∗ j , the assertions (val1) and (val2) are also satisfied.

˜

The propositional valuation ˜ v of the variables in B inherent to the QF LIRA model is defined in the following manner:

• ˜ v(x(k) i ) = vk(xi);
• ˜ v(p(k) i ) = vk(ψi).

This implies that (prop prob) is satisfied since the valuation ˜ v atributes the same truth value to p(k) i and ψ(k) i . Furthermore, the assertion (cons) is also satisfied as the truth value of G(k) i is given by h∗ik .

Provided that the original probability distribution ρ satisfies the GGenPSAT instance, we immediately conclude that (hard constr) and (soft constr) are satisfied, which concludes the proof of the direct implication.

Reciprocally, assume that the associated QF LIRA problem is satisfiable, and consider the components of its model: a valuation ˜ v of the variables in ˜ B, and define by y∗ the value that the model gives to the variable y. Our aim, is to define a probability distribution ρ over the set of valuations V ∗ of the variables in P.

With this purpose, we will refine the valuation ˜ v, reduce it to valuations over B, and finally define the probability distribution ρ. Since ˜ v is a valuation over ˜ B = ∪|G|+1 k=1 B(k) , define its reduct to each copy of B, vk(p) = ˜ v(p(k) ) , for each p ∈ B. Let W = {v1, . . . , v|G|+1} be the set of such valuations. Then, consider the probability distribution π : W → [0, 1] defined as π(vk) = π∗ k . The probability distribution ρ : V ∗ → [0, 1] we seek is now easily defined recalling that B = P ∪G:

We now need to check that this valuation is well defined, i.e., that if vi|P = vj|P then π∗ i = π∗ j . We will do this by showing that if vi ̸= vj then vi|P ̸= vj|P : if for some x ∈ P, vi(x) ̸= vj(x) then obviously their reducts to P will also differ in x; on the other hand, if for every x ∈ P, vi(x) = vj(x), and there is a p ∈ G such that vi(p) ̸= vj(p) we obtain a contradiction - let ψ be the propositional formula corresponding to p. Since vi(x) = vj(x) for every x ∈ P, then vi(ψ) = vj(ψ) which means that ˜ v(ψ(i) ) = ˜ v(ψ(j) ). Since ˜ v satisfies (prop prob), this means that ˜ v(p(i) ) = ˜ v(p(j) ) and so vi(p) = vj(p).

Since (sums1) is satisfied, ρ constitutes a well-defined probability distribution. To conclude that the hard constraints are satisfied, observe that for each φ ∈ Γ, since α∗φ = 1 it follows that h∗ij = 1 for each j such that π∗ j > 0 and by (cons) and (prop prob) it means that ρ satisfies φ with probability 1. For soft constraints, the reasoning is similar - observe that (cons) and (prop prob) links the algebraic reasoning with the valuations. To show that ρ satisfies Ψ, i.e., the soft constraints, since the assertion (soft constr) is satisfied, it is enough to show that Pr(ψ) coincides with α∗ i , where ψ is the i-th formula of InsidePr(Ψ). In fact, the probability of ψ

We detail the second to last step of the deduction: either h∗ij is 0 and by the first (val2) assertion then b∗ij is also 0 and so h∗ij · π∗ j = 0 = b∗ij ; or h∗ij is 1 and by the (val2) assertions we obtain that b∗ij equal to π∗ j and so h∗ij · π∗ j = 1 · π∗ j = b∗ij .

This shows that ρ satisfies the formulas in Ψ and so it is a model for the GGenPSAT instance (Γ,Ψ).

5 Phase Transition

In this section we describe the open-source tool [Caleiro et al., 2016c] developed to implement the algorithm that solves the GGenPSAT problem. With this in hands, we generate batches of random GGenPSAT instances and study the behavior of the implemented solver, in terms of time and satisfiability.

For this, we measure the proportion of satisfiable instances as well as the average time the solver spent to solve them. The software was written in Python, and we used Yices [Dutertre, 2014], version 2.5.1, to solve the SMT problem. Our tool takes as input a GGenPSAT written in an (smt-lib)-style notation enriched with the probability operator (pr φ). As an example, the second problem from Example 1 can be formulated as follows:

(define x::bool) (define y::bool) (assert (>= (pr (not (xor x y))) (* 2 (pr (xor x y))))) (assert (> (pr (xor x y)) 0)) (assert (or (= (pr y) 0) (= (pr y) 1))) (assert (= (pr x) 0)) (check)

The machine used for the tests was a Mac Pro at 3.33 GHz 6-Core Intel Xeon with 6 GB of memory.

A phase transition behavior is characterized by a sharp transition between two clearly distinct states. Regarding satisfiability problems, these states correspond to states in which the problems are either satisfiable or not satisfiable. In [Gent and Walsh, 1994], this behavior was studied for random 3SAT problems and, heuristically, shown that the ratio m/n of number of clauses over the number of variables characterizes the phase transition. That is, there is a value (close to 4.3 on 3SAT) of m/n for which the random problems rapidly transition from being satisfiable to not being satisfiable. It is also noteworthy that the harder random instances lie in this critical area, as we can heuristically observe a peak in time taken to solve problems.

We now present some results regarding the behavior of random instances of 3SATwhen embedded in GGenPSAT. The embedding of PSAT and GenPSAT was also studied but not included due to size limitations. Besides revealing the phase transition behavior, our results show that the presented solver is more efficient than the solver for GenPSAT, [Caleiro et al., 2016b]. This is not unexpected since the translation used here for the GGenPSAT problem is much more natural and concise than the one used for GenPSAT.

We denote by n the number of variables and m the number of propositional clauses. In random 3SAT instances, we detect the phase transition when m/n is close to 4.3 as previously detected in [Gent and Walsh, 1994], see Figure 2.

As expected, being an NP-complete problem, the full GGenPSAT problem also exhibits a phase transition behavior. We generated the random GGenPSAT instances as follows: a random 3SAT instance with n variables and m clauses is generated and then, each variable xi is replaced by a problem Gi which is a conjunction of k random probabilistic atoms over n variables. The results are seen in Figure 3.

In summary, the developed tool (due to the size of the translation) is able to solve reasonably sized instances, surpassing as well the GenPSAT dedicated tool developed in [Caleiro et al., 2016a] for those instances. Given this, we are able to detect the phase transition behavior and heuristically determine parameters for which random instances are hard to solve.

6 Conclusions and FutureWork

In this paper, we aimed to study a generalization of the probabilistic satisfiability problem. The GGenPSAT problem naturally models Boolean combinations of linear inequalities involving probabilities of propositional formulas. We developed a satisfiability procedure by a polynomial reduction to the quantifier-free theory of integer and real arithmetic, and proved its correctness. We also implemented a tool that translates problems in GGenPSAT to QF LIRA and solves them with an off-the-shelf SMT solver such as Yices. With this tool in hands we are able to detect and study the phase-transition behavior of this problem. It is also worth noting that since the expressiveness of the GGenPSAT problem coincides with the probabilistic logic of Fagin et al. [Fagin et al., 1990], this tool also serves as a satisfiability procedure for the logic.

We believe the study of this problem and subsequent tool implementation provides a sound foundational basis to the development of applications where probabilistic reasoning is required. As future work, we aim to develop applications of this tool for the analysis of cryptographic protocols, specially related to the existence of side-channel attacks.