# classical_generalized_probabilistic_satisfiability__198c2132.pdf

Classical Generalized Probabilistic Satisfiability

Carlos Caleiro SQIG - Instituto de Telecomunicac oes DMath, Instituto Superior T ecnico Universidade de Lisboa, Portugal carlos.caleiro@tecnico.ulisboa.pt

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

Andreia Mordido INOV INESC Inovac ao, Portugal andreia.mordido@inov.pt

We analyze a classical generalized probabilistic satisfiability problem (GGen PSAT) which consists in deciding the satisfiability of Boolean combinations of linear inequalities involving probabilities of classical propositional formulas. GGen PSAT coincides precisely with the satisfiability problem of the probabilistic logic of Fagin et al. and was proved to be NP-complete. Here, we present a polynomial reduction of GGen PSAT to SMT over the quantifierfree theory of linear integer and real arithmetic. Capitalizing on this translation, we implement and test a solver for the GGen PSAT problem. As previously observed for many other NP-complete problems, we are able to detect a phase transition behavior for GGen PSAT.

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 Ge TFun: Generalizing Truth-Functionality.

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 (Gen PSAT) 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 Gen PSAT problem to allow Boolean combinations of probabilistic formulas as well as present a solver for this more expressive problem.

PSAT Pr(φ) b SAT

GPSAT Pr(φ) b

GGen PSAT ai Pr(φ) b

Gen PSAT ai Pr(φ) b

Satisfiability problem of the Probabilistic Logic [Fagin et al., 1990]

Figure 1: Inclusion diagram of several fragments of the probabilistic logic

In this paper, we present the classical generalized probabilistic satisfiability problem GGen PSAT, 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 GGen PSAT are precisely the formulas in the probabilistic logic by Fagin et al. We develop an algo-

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

rithm for the GGen PSAT 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 GGen PSAT and SMT problems, which then allows the implementation of a provably correct solver for GGen PSAT. With the GGen PSAT 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 GGen PSAT 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 GGen PSAT 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 LCPL ::= P | LCPL | LCPL LCPL . 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: PAt ::= Q Pr(LCPL) + . . . + Q Pr(LCPL) Q . The set of probabilistic formulas is defined as a Boolean combination of probabilistic atoms as follows: Prob ::= PAt | Prob | Prob Prob . 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: π q1 Pr(φ1) + . . . + qℓ Pr(φℓ) q iff ℓ i=1 ( qi ( 2n

j=1 vj(φi) πj )) q;

π δ 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 2n

j=1 (vj(c) πj) q .

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

V π p πi = 1 π 0

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 Gen PSAT Problem In [Caleiro et al., 2016a], probabilistic satisfiability was extended to handle linear inequalities involving assignments of values to propositional formulas. An instance of Gen PSAT 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 Gen PSAT instance (Γ, Σ) if it satisfies the set of probabilistic atoms

Ξ(Γ,Σ) = Σ {Pr(γ) = 1 | γ Γ} . (1)

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

3 The GGen PSAT Problem We now aim to extend the Gen PSAT problem in order to cope with Boolean combinations of probabilistic atoms. An instance of GGen PSAT 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 GGen PSAT instance (Γ, Ψ) if it satisfies the set of probabilistic formulas

Ξ(Γ,Ψ) = Ψ {Pr(γ) = 1 | γ Γ} . (2)

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

Despite the similarities between a Gen PSAT and a GGen PSAT instance, the latter allows more expressive probabilistic formulas by allowing Boolean combinations of probabilistic atoms. Definition 3 (GGen PSAT problem). Given a GGen PSAT instance (Γ, Ψ), the Classical Generalized Probabilistic Satisfiability problem consists in determining if there exists a probability distribution π over V that satisfies (Γ, Ψ). GGen PSAT extends the scope of PSAT and Gen PSAT 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: Pr(x) = 0 Pr(x) = 1 . 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 GGen PSAT: 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 Gen PSAT instance is also a GGen PSAT instance. Notice that GGen PSAT 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]). GGen PSAT is NPcomplete.

4 Reducing GGen PSAT 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 Gen PSAT 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 GGen PSAT 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 GGen PSAT problem.

On the details of the GGen PSAT instance: Assume we are given a GGen PSAT 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 q1 Pr(ψ1) + . . . + qℓ Pr(ψℓ) q ,

where { , , <, >, =, =}.

When ghosts attack: Driven by Gen PSAT 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 Inside Pr(δ) LCPL all the propositional formulas occurring inside the probabilistic formula δ Prob, which is defined inductively on the structure of δ: Inside Pr(q1 Pr(ψ1)+. . .+qℓ Pr(ψℓ) q) = {ψ1, ..., ψℓ}; Inside Pr( δ) = Inside Pr(δ); Inside Pr(δ1 δ2) = Inside Pr(δ1) Inside Pr(δ2). This notion is extended for a set of probabilistic formulas as usual, Inside Pr( ) = δ Inside Pr(δ). 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, Rel F defined by:

Rel F = Γ Inside Pr(Ψ) .

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

G = {pψ | ψ Rel F} .

Furthermore, we will use the real [0, 1]-variable αψ to represent the probability of ψ Rel F. For ease of notation, we denote by Gi the i-th element of G and ψi the corresponding propositional formula in Rel F. 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 Gen PSAT, we express the probabilistic assertions about the elements in Rel F algebraically as follows:

V π = α πj = 1 π 0 (3)

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

V = [Vij] is a matrix of size |G| 2n, where Vij is defined from the jth 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 system with |G|+1 linear inequalities has a solution iff it has a solution with |G|+1 nonnegative entries. Furthermore, if a GGen PSAT 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 π: {Hπ = α π 0 . (4)

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 B(k) = {x(k) | x P} {p(k) | p G} . 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 e 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 ψ Inside Pr(Ψ), 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 Pr To LIRA, can be inductively extended to probabilistic formulas (which are Boolean combinations of probabilistic atoms): Pr To LIRA(q1 Pr(ψ1) + . . . + qℓ Pr(ψℓ) q) is the assertion q1 αψ1 + . . . + qℓ αψℓ q; Pr To LIRA( δ) is the assertion Pr To LIRA(δ); Pr To LIRA(δ1 δ2) is the assertion Pr To LIRA(δ1) Pr To LIRA(δ2).

All together now: To verify the satisfiability of the GGen PSAT instance, we will need to satisfy the following constraints: (hard constr) φ Γ αφ = 1;

(soft constr) δ Ψ Pr To LIRA(δ);

(cons) hik = 1 G(k) i for each i {1, ..., |G|}, k {1, ..., |G| + 1};

(val1) |G|+1 j=1 bij = αψi for each i {1, . . . , |G|};

(val2) (0 bij hij) (hij 1 + πj bij πj) for each i {1, . . . , |G|}, j {1, . . . , |G| + 1};

(sums1) |G|+1 j=1 πj = 1;

(prop prob) |G|+1 k=1 ( G(k) i ψ(k) i ) for each i {1, ..., |G|}.

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 e B. With this, we can conclude that the presented procedure translates a GGen PSAT instance into a problem in QF LIRA of polynomial size.

The solver: We test the satisfiability of a GGen PSAT 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; Pr To LIRA( ) 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 GGen PSAT instance.

Algorithm 1 GGen PSAT solver based on SMT QF LIRA

1: procedure GGen PSAT( {xi}n i=1, Γ, Ψ) 2: assume: G = {pψ | ψ Rel F}

3: declare: propositional variables: e B = |G|+1 k=1 B(k)

4: declare: binary variables: hij 5: declare: [0, 1]-variables: αψi, πj, bij 6: for i = 1 to |G| do 7: assert( j bij = αψi) (val1)

8: assert( k(G(k) i ψ(k) i )) (prop prob) 9: for j = 1 to |G| + 1 do

10: assert(hij = 1 G(j) i ) (cons) 11: assert(0 bij hij) (val2) 12: assert(hij 1 + πj bij πj) (val2)

13: assert( φ αφ = 1) (hard constr) 14: assert( δ Pr To LIRA(δ)) (soft constr) 15: assert( πi = 1) (sums1) 16: return qf lira solver()

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

Proposition 1. A GGen PSAT instance (Γ, Ψ) is satisfiable iff Algorithm 1 returns Sat. Proof. Assume that a GGen PSAT 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 ev over the extended set of propositional variables e B. For each pψ G, let α ψ be the probability of the propositional variable pψ induced by the probability distribution ρ in the following manner:

v:v(ψ)=1 ρ(v) . (5)

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

V π = α πj = 1 π 0 (6)

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 jth 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 {Hπ = α

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 ev of the variables in e B inherent to the QF LIRA model is defined in the following manner:

ev(x(k) i ) = vk(xi); ev(p(k) i ) = vk(ψi). This implies that (prop prob) is satisfied since the valuation ev 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 GGen PSAT 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 ev of the variables in e 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 ev, reduce it to valuations over B, and finally define the probability distribution ρ. Since ev is a valuation over e B = |G|+1 k=1 B(k), define its reduct to each copy of B, vk(p) = ev(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: { ρ(vi|P ) = π i for each i {1, . . . , |G| + 1} ρ(v) = 0 otherwise

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 ev(ψ(i)) = ev(ψ(j)). Since ev satisfies (prop prob), this means that ev(p(i)) = ev(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 Inside Pr(Ψ). In fact, the probability of ψ

v V v(ψ) ρ(v) =

v W v(ψ) ρ(v)

j=1 vj(ψ) π j =

j=1 ev(ψ(j)) π j

j=1 h ij π j =

j=1 b ij = α i . by (val2)

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 GGen PSAT 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 GGen PSAT problem. With this in hands, we generate batches of random GGen PSAT instances and study the behavior of the implemented solver, in terms of time and satisfiability.

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

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 GGen PSAT 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 GGen PSAT. The embedding of PSAT and Gen PSAT 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 Gen PSAT, [Caleiro et al., 2016b]. This is not unexpected since the translation used here for the GGen PSAT problem is much more natural and concise than the one used for Gen PSAT. 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.

Figure 2: 3SAT as a GGen PSAT instance, with n = 200.

As expected, being an NP-complete problem, the full GGen PSAT problem also exhibits a phase transition behavior. We generated the random GGen PSAT 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.

Figure 3: Random GGen PSAT instances with n = 30 and k = 2 (above) and n = 20 and m = 10 (below).

In summary, the developed tool (due to the size of the translation) is able to solve reasonably sized instances, surpassing as well the Gen PSAT 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 Future Work In this paper, we aimed to study a generalization of the probabilistic satisfiability problem. The GGen PSAT 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 GGen PSAT 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 GGen PSAT 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.

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

References [Barrett et al., 2016] C. Barrett, P. Fontaine, and C. Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2016. [Bona et al., 2015] G.D. Bona, F. G. Cozman, and M. Finger. Generalized probabilistic satisfiability through integer programming. Journal of the Brazilian Computer Society, 21(1):1 14, 2015. [Boole, 1853] G. Boole. Investigation of The Laws of Thought On Which Are Founded the Mathematical Theories of Logic and Probabilities. 1853. [Caleiro et al., 2016a] C. Caleiro, F. Casal, and A. Mordido. Generalized probabilistic satisfiability. In LSFA 2016 - 11th Workshop on Logical and Semantic Frameworks, with Applications, 2016. [Caleiro et al., 2016b] C. Caleiro, F. Casal, and A. Mordido. Gen PSAT solver, 2016. Available online at https://github.com/fcasal/genpsat.git. [Caleiro et al., 2016c] C. Caleiro, F. Casal, and A. Mordido. GGen PSAT solver, 2016. Available online at https://github.com/fcasal/ggenpsat.git. [Chv atal, 1983] V. Chv atal. Linear programming. Macmillan, 1983. [Cook, 1971] S. A. Cook. The complexity of theoremproving procedures. In Proceedings of the third annual ACM symposium on Theory of computing, pages 151 158. ACM, 1971. [De Moura and Bjørner, 2011] L. De Moura and N. Bjørner. Satisfiability modulo theories: introduction and applications. Communications of the ACM, 54(9):69 77, 2011. [Dutertre, 2014] B. Dutertre. Yices 2.2. In Armin Biere and Roderick Bloem, editors, CAV 2014, volume 8559 of Lecture Notes in Computer Science, pages 737 744. Springer, 2014. [Fagin et al., 1990] R. Fagin, J. Y. Halpern, and N. Megiddo. A logic for reasoning about probabilities. Inf. Comput., 87(1-2):78 128, 1990. [Finger and Bona, 2011] M. Finger and G.D. Bona. Probabilistic satisfiability: Logic-based algorithms and phase transition. In IJCAI, pages 528 533. IJCAI/AAAI, 2011. [Finger and Bona, 2015] M. Finger and G.D. Bona. Probabilistic satisfiability: algorithms with the presence and absence of a phase transition. Annals of Mathematics and Artificial Intelligence, 75(3):351 389, 2015. [Gent and Walsh, 1994] I. P. Gent and T. Walsh. The hardest random SAT problems. Springer, 1994. [Georgakopoulos et al., 1988] G. Georgakopoulos, D. Kavvadias, and C. H Papadimitriou. Probabilistic satisfiability. Journal of Complexity, 4(1):1 11, 1988. [King, 2014] T. King. Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic. Ph D thesis, Courant Institute of Mathematical Sciences New York, 2014.

[Nilsson, 1986] N. J. Nilsson. Probabilistic logic. Artif. Intell., 28(1):71 88, 1986.

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)