Background

Propositional logic, given its relatively simple sintax and semantics, offers an useful starting point for knowledge representation [5]. The basic syntatic element in this logic is the concept of propositional variable or atomic formula formula that can assume one of two values, true or false. A literal is either an atomic formula or its negation. In this text compound formulas are indicated by the greek letters $\phi$, $\psi$ and $\theta$ with or without indexes. A disjunction of literals is a clause. A Conjunctive Normal Form (CNF) is a conjunction of clauses, denoted by C1 $\wedge$ . . . Cr where Ci is a clause.

The semantics of any expression in propositional logic depends on a mapping that establishes a correspondence between the variables in the formula to facts in a target domain. A truth assignment is a vector assigning either value true or false to each propositional variable of an expression (these assignments are often called possible worlds [3]). If we have n propositional variables, there are 2 n truth assignments. A conjunctive formula is true if all its component formulas are true, otherwise it is false. A disjunctive formula is false only if all its component formulas are false, otherwise it is true. A negative formula is true (false) if its component formula is false (true).

A formula $\phi$ is satisfiable if it is true in some possible world $\omega$; then $\omega$ is a model for $\phi$ ($\mathcal{M}$($\phi$, $\omega$)). If $\phi$ has no model it is unsatisfiable. A formula $\psi$ entails a formula $\theta$ ($\psi$ $\models$ $\theta$) if every model for $\psi$ is a model for $\theta$. An inference $\psi$ $\vdash$ $\theta$ determines whether a premise $\psi$ entails a conclusion $\theta$. satisfiability problem (SAT) is: given a CNF $\psi$ with m clauses C1 , . . . Cm , is $\psi$ satisfiable? This question has a strong relationship to logic entailment and logic inference because $\psi$ $\models$ $\theta$ iff $\psi$ $\wedge$ $\neg$$\theta$ is unsatisfiable. That is, it is possible to approach inference as SAT problem. A particular kind of SAT problem is the k-SAT, a SAT which every clause has k literals.

An important limitation of propositional logic, from a point of view of knowledge representation, is its inability to deal with uncertainty. As stressed by Neapolitan [6]: ``We also must acknowledge that in some cases the truth of certain premisses may be suggestive of the truth of a conclusion, but not imply it conclusively.'' To overcome this difficulty, propositional probabilistic logic extends propositional logic by attaching probability assessments to formulas. In this context,

The counterpart of SAT in probabilistic logic is the probabilistic satisfiability problem (PSAT) [7]. The PSAT structure is similar to SAT but it poses the following question: is there a probability distribution satifying a set of $m$ assessments that assign probability interval to $\pr{\phi_i}$ for a set of formulas $\{\phi_i\}_{i=1}^m$ over $n$ propositions.

If the assessments are such that no probability distribution p over truth assignments can be specified, the assessments are inconsistent. The consistency problem of probabilistic satisfiability is: given a set of assessments, determine whether they are inconsistent or not. The inference problem of probabilistic satisfiability is: given a set of assessments and a formula $\phi$, obtain the infimum of $\pr{\phi}$ -- that is, the infimum value $\alpha$ such that the constraint $\pr{\phi}=\alpha$ and the assessments are consistent. The infimum is denoted by $\lpr{\phi}$ and called the lower probability of $\phi$. This infimum is attained because probabilitisc assessments on the logical formulas and constraints $\sum_{\omega} \pr{\omega} = 1$, $\pr{\omega} \geq 0$ define a bounded polyhedron in the space of probability measures over truth assignments.

Like SAT, PSAT is a NP-complete [7].