We design a novel model-based approach for reasoning, considering the reasoning process as the computation of the degree of belief of an intelligent agent. We assume a Knowledge Base (KB) expressed by a two Conjunctive Form (2-CF) Σ. We represent Σ using an appropriate logical structure. Our representation of a 2-CF is highly expressive since it supports efficient reasoning, even in the cases where the formula-based representation does not allow to do it. Indeed, we can compute the degree of belief with new information (a literal or a binary clause) efficiently, providing an efficient scheme of inductive reasoning. Exploiting this logical structure of a 2-CF, we propose a way to determine the relative value for every element in the KB which is an essential problem when new knowledge is aggregated and is necessary to maintain the consistency of the KB.
A widely accepted framework for reasoning in intelligent systems is the knowledgebased system approach. The main idea is to represent the knowledge in an appropriate structure or language with a well defined semantics assigned to the sentences [9]
The AI goal of providing a logic model of human agent capability of reasoning, in the presence of incomplete and changing information, has proven to be very difficult to achieve. For example, to decide whether a KB Σ implies a sentence α (denoted as K |= α) is a co-NP-Hard problem, even in the propositional case [9]. Many other forms of reasoning which have been developed to avoid, at least partly, these computational difficulties, have also shown to be hard to compute.
As it has been pointed out in [1, 4, 11, 13], an important problem to explore is the computational complexity of the reasoning methods. Although each method is clearly intractable in the general case, a precise determination of the complexity is left as an open issue. Furthermore, it is not clear under which restrictions such methods would become tractable.
In our case, we perform reasoning as the computation of the proportion of the number of models of Σ which remains after a new formula F is processed (here as processing we mean calculating a degree of belief, updating or a doing belief revision). In order to clarify a frontier between efficient and exponentialtime reasoning, we start working with a KB Σ in two conjunctive form (2-CF), and we consider queries also in 2-CF. We want to compute the degree of belief that an agent A has in a new piece of information F based on the conditional probability of F with respect to Σ and denoted as PF |Σ, and calculated as the fraction of models of Σ that satisfy F .
Computing the degree of belief leads us to count the number of models of a formula Σ (denoted as #SAT(Σ)) which is a classical #P-complete problem. #SAT looks harder than SAT problem, for example, the 2-SAT problem (SAT restricted to consider 2CF’s)is solved in linear time. However, the corresponding counting problem #2-SAT is #P-complete. #2-SAT remains #P-complete if we consider only monotone formulas or Horn formulas [14].
#SAT is of special concern to Artificial Intelligence (AI), and it has a direct relationship to Automated Theorem Proving, as well as to approximate reasoning [1, 3, 6, 10, 13]. An interesting area of research has been the identification of restricted cases for which #SAT can be solved efficiently.
We extend here some of the procedures presented in [2, 3, 7] for the #2-SAT problem and show how to apply them to the computation of the degree of belief. Furthermore, we show that our logical structure representation of the KB allows the efficient computation of the degree of belief for some classes of 2-CFs.
Given our logical structure representation of a 2-CF, we propose a way to determine the relative values for every element of the KB, which is an essential problem for performing reasoning in efficient way, for example in the area of update-belief revision, where is essential to know how to incorporate dynamically a single or a sequence of changes into an initial Knowledge Base. 2.
Let X = {x1, . . . , xn} be a set of n Boolean variables. A literal is either a variable xi or a negated variable xi. As usual, for each xi ∈ X, xi0 = xi and xi1 = xi.
A clause is a disjunction of different literals (sometimes, we also consider a clause as a set of literals). For k ∈ IN , a k-clause is a clause consisting of exactly k literals and, a (≤ k)-clause is a clause with at most k literals. A variable x ∈ X appears in a clause c if either x or x is an element of c.
A Conjunctive Form (CF) F is a conjunction of clauses (we also consider a CF as a set of clauses). We say that F is a monotone CF if all of its variables appear in unnegated form. A k-CF is a CF containing only k-clauses and, (≤ k)CF denotes a CF containing clauses with at most k literals. A kµ-CF is a formula in which no variable occurs more than k times. A (k, jµ)-CF ((≤ k, jµ)-CF) is a k-CF ((≤ k)-CF) such that each variable appears no more than j times.
We use υ(X) to express the set of variables involved in the object X, where X could be a literal, a clause or a Boolean formula. For instance, for the clause c = {x1, x2}, υ(c) = {x1, x2}. And Lit(F ) is the set of literals which appear in a CF F , i.e. if X = υ(F ), then Lit(F ) = X ∪ X = {x1, x1, ..., xn, xn}. We also denote {1, 2, ..., n} by [[n]].
An assignment s for F is a Boolean function s : υ(F ) → {0, 1}. An assignment can be also considered as a set of non complementary pairs of literals. If l ∈ s, being s an assignment, then s turns l true and l false. Considering a clause c and assignment s as a set of literals, c is satisfied by s if and only if c ∩ s = ∅, and if for all l ∈ c, l ∈ s then s falsifies c.
If F1 ⊂ F is a formula consisting of some clauses of F , then υ(F1) ⊂ υ(F ), and an assignment over υ(F1) is a partial assignment over υ(F ). Assuming n =| υ(F ) | and n1 =| υ(F1) |, any assignment over υ(F1) has 2n−n1 extensions as assignments over υ(F ).
Let F be a Boolean formula in Conjunctive Form (CF), F is satisfied by an assignment s if each clause in F is satisfied by s. F is contradicted by s if any clause in F is contradicted by s. A model of F is an assignment for υ(F ) that satisfies F .
Given F a CF, the SAT problem consists of determining if F has a model. The #SAT problem consists of counting the number of models of F defined over υ(F ). #2-SAT denotes #SAT for formulas in 2-CF. We also denote #SAT(F ) by µυ(F )(F ) or just µ(F ) when υ(F ) is clear from the context.
Up to now, the maximum subclass of 2-CF where #2SAT is solved efficiently is for the class (2, 2µ)-CF (formulas in 2-CF where each variable appears twice at most) [13, 14]. Here, we extend such class for considering the topological structure of the undirected graph induced by the formula. 3.
Computing the degree of belief of an agent is a hard task in general, even if the KB Σ of the agent is expressed by 2-CF’s. We design a logical structure for representing a 2-CF in a way that computing the degree of belief in new formulas can be done efficiently, for a restricted class of Boolean formulas.
An initial Knowledge Base (KB) is given by a 2-CF Σ. Σ is represented by a signed constrained directed graph GΣ. We compute, for every node x ∈ GΣ (variable of the formula Σ), a pair (αx, βx), where αx indicates how many times the variable x is ’true’ and βx indicates the number of times that the variable x can take value ’false’ in the set of models of Σ. We show in following sections that under this representation of Σ, we can compute efficiently the degree of belief in a literal or in a binary clause including variables not used previously in Σ, providing so an efficient inductive scheme of reasoning. 3.1.
The Graph Representation of the Knowledge Base Let Σ be a 2-CF, the constrained graph of Σ is the undirected graph GΣ = (V (Σ), E(Σ)), with V (Σ) = υ(Σ) and E(Σ) = {{υ(x), υ(y)} : {x, y} ∈ Σ}, that is, the vertices of GΣ are the variables of Σ, and for each clause {x, y} in Σ there is an edge {υ(x), υ(y)} ∈ E(Σ).
Each edge c = {υ(x), υ(y)} ∈ E is associated with an ordered pair (s1, s2) of signs, assigned as labels of the edge connecting the variables appearing in the clause. The signs s1 and s2 are related to the signs of the literals x and y respectively. For example, the clause {x ∨ y} determines the labelled edge: “x − + y” which is equivalent to the edge “y + − x”.
Some authors have considered the signs of the literals in the clauses of a 2-CF F by using orientation of the edge corresponding to the clause [13, 14], and then the problem of counting models of F is seen as counting the number of orientations in its respective constrained graph, which has no sink (vertex with out-degree zero).
A graph with labelled edges on a set S is a pair (G, ψ), where G = (V, E) is a graph, and ψ is a function with domain E and range S. ψ(e) is called the label of the edge e ∈ E. Let S = {+, −} be a set of signs . Let G = (V, E, ψ) be a signed graph with labelled edges on S × S. Let x and y be nodes in V . If e = {x, y} is an edge and ψ(e) = (s, s ), then s (s ) is called the adjacent sign to x (y).
Given a 2-CF Σ, a connected component of GΣ is a maximal subgraph such that for every pair of vertices x, y, there is a path in GΣ from x to y. We say that the set of connected components of Σ are the subformulas corresponding to the connected components of GΣ.
Let Σ be a 2-CF. If F = {G1, . . . , Gr} is a partition of Σ (over the set of clauses appearing in Σ), i.e. rρ=1 Gρ = Σ and ∀ρ1, ρ2 ∈ [[r]], [ρ1 = ρ2 ⇒ Gρ1 ∩ Gρ2 = ∅], we say that F is a partition in connected components of Σ if V = {υ(G1), . . . , υ(Gr)} is a partition of υ(Σ).
If {G1, . . . , Gr} is a partition in connected components of Σ, then:
µυ(Σ)(Σ) = µυ(G1)(G1) ∗ . . . ∗ µυ(Gr)(Gr)
(
In order to compute #SAT (Σ), first we should determine the set of connected components of Σ, this can be done in linear time. The different connected components of GΣ constitute the partition of Σ in its connected components, even if GΣ is disconnected. Then, computing #SAT (Σ) is reduced to compute µυ(G)(G) for each connected component G of Σ.
From now on, when we mention a formula Σ, we assume that Σ is a connected component graph. We say that a 2-CF Σ is a path, a cycle, a tree or a grid if its corresponding constrained graph GΣ is a path, a cycle, a tree, or a grid, respectively.
Notice that each connected component Gi is independent of any other Gj, i = j, since υ(Gi) ∩ υ(Gj) = ∅. Of course, if the number of models in any connected component is zero, then the total number of models in Σ is zero too.
Let GΣ = (V, E, {+, −}) be a signed connected graph of an input formula Σ in 2-CF. Let vr be the node of minimum degree in GΣ which is chosen to start a depth-first search. We obtain a spanning tree TG with vr as the root node and a set of fundamental cycles C = {C1, C2, ..., Ck} and where each back edge ci ∈ E marks the beginning and the end of a fundamental cycle.
Given any pair of cycles Ci and Cj of C, i = j, if Ci and Cj share edges, we call them intersecting cycles; otherwise, they are called independent cycles. Let AG be the depth-first search graph of GΣ formed by the spanning tree TG and the set of fundamental cycles C.
We translate AG to a Directed Acyclic Graph (DAG), denoted by DG, assigning an orientation to each edge {u, v} in AG by directing: u → v if v is the parent node of u in TG.
We apply a topological sorting procedure on DG, obtaining an ordered number o associated with each node in DG such that o(u) < o(v) whenever u → v. This order number indicates the order for processing the nodes in DG when we compute the value #SAT(Σ) in the next subsection. 3.2.
Computing the Number of Models on the Directed Acyclic Graph Let Σ be a simple path, we can compute the number of models of Σ applying on GΣ the following matrix operators:
T++ =
The subscripts ” + +”, ” + −”, ” − +”, and ” − −” correspond to the signs of
the literals associated to the source and target nodes, respectively. For example,
if Σ = {{x, y}, {y, z}, {z, w}} (see figure 1), then we use the operators given in
(
We begin with the 2-vector (
For example, the processing of the path illustrated in figure 1 is:
(
In order to count the number of models on simple cycles, we consider 2 ×
2matrices and the matrix operators Ψss defined on N4 for s, s ∈ {+, −}, as
follows:
Ψss
a b
c d
= Tss
a b
c d
(
Where “ ” is the Hadamard product ( (aij ) (bij ) = (aijbij) for (aij ) and (bij) m × n-matrices).
Then, the operators in (
Example 1 Let Σ = {{x, y}, {y, z}, {z, w}, {x, w}} be a simple cycle (see figure 2), then we proceed as follows. Therefore, Σ has 6 models.
x +y -z ++ w -+ -x +y z ++ w
Where υ1(F ) is the set of variables of F with degree 1, Tc denotes the operator Tss such that s is the sign of the variable x ∈ υ(c) of degree 1, and s is the sign of the variable y ∈ υ(c) \ {x}.
Example 2 Let Σ = {{x, y}, {y, z}, {z, w}, {y, u}, {z, v}} be a tree (see fig. 3). +
u x +- + y -- z ++ w + + v
+ 1 + + 2 + 3 - + - 4 - 5
Applying the algorithm Count M odels to Σ from example 2, we have:
1. qx = qy = qz = qw = qu = qv = (
Therefore #SAT (Σ) = 12, and according to the last step, there are 8 models where z has value true and 4 models where z has value false.
Given a connected graph GΣ, traversing GΣ in depth-first search leads to a tree that we denote as AΣ. We can express GΣ = AΣ +Ea, where Ea is the set of back edges that form the fundamental cycles found during the depth-first search. It is not difficult to follow the order given by the topological order procedure to compute #SAT (Σ).
For computing #SAT (Σ) for any general 2-CF Σ, we use Count M odels for pre-processing GΣ obtaining a new GΣ such that #SAT(Σ) =#SAT(Σ ) but in GΣ there is no node of degree 1. Then Count M odels updates the charges already computed on each node in Σ .
Now the processing continues on Σ . For each arc b = (s, t) which embraces an original fundamental cycle in GΣ, according to the signs in b, each column a in the current matrix M where b > 0 is translated to a 0 if s has sign b 0 bt ’+’ or such column is translated to a0t 0b if s has sign ’-’ and a > 0.
Notice that the number of the node t in which the cycle closes is used as subindex. Furthermore, if there are already subindexes in the current column such subindexes are preserved in the new columns aggregated to M .
Columns with similar subindexes are added in order to reduce them into a single column. The following example, allow to illustrate the processing of cycles. Example 3 Let us consider Σ1 = {{x1, x2}, {x2, x3}, {x3, x4}, {x4, x5}, {x1, x4}, {x3, x5}} whose constrained graph GΣ1 is illustrated in figure 4. Note that in each node 4 and 5 a cycle is closed. The computation of #SAT (Σ1) is done as follows. 1 0 T++ 1 14 T+− 15 0 14,5 0 Ψ+−T−+ 15 2 0 0 Ψ−−T−− 0 14 1 0 0 2 0 14 0 2 0 14 01 24 00 11 . Therefore #SAT (Σ1) = 9.
Although the procedures showed in this subsection have exponential time complexity for 2-CF’s in general, we have shown in [2, 7] that if the constrained graph GΣ associated with a 2-CF Σ does not contain intersecting cycles, then we can compute #SAT(Σ) in polynomial time. 3.3.
Computing the Charges of a 2-CF In this section, we present a novel method for computing the charges (αx, βx) for all variables x in a 2-CF Σ, assuming that the previous algorithm has been applied for computing #SAT(Σ).
Let A0, . . . , Am be the sequence of matrices obtained during the application of the above procedure for computing #SAT(Σ). Given this sequence, we build a new sequence of matrices Bm, . . . , B0 computed as:
Bm = Am
Bm−i = balance(Am−i, Bm−i+1), i = 1, ..., m
(
a b < a , b >→ c c
If a = a then the values c and c are the closest integers to the values r ·a and r · a respectively, and where r = (b + b )/(a + a ), or c = b otherwise. c b
Notice that the essence of the recurrence balance is to apply the inverse operation of that used in each step of the computation of #SAT(Σ), and following the inverse order used in the construction of the sequence A0. . . . , Am.
If initially the matrices A and B do not have the same dimensions, e.g A is a 2 × n1 matrix and B is a 2 × n2 matrix and n1 < n2, then we reduce the dimension (n2) of B to the dimension (n1) of A, summing columns and closing lines of computation according to the order in which they were extended (when a new cycle was found) during the computation of #SAT(Σ).
Therefore, let x0, . . . , xm be the topological order of the nodes in GΣ, we associate with each node xi, i = 0, . . . m the matrix Bi from the sequence Bm, . . . , B0. And then, the charge qi of the variable xi, i = 0, . . . , m is determined as: qi = aaii where ai and ai are the sum of the entries of the first and second row of Bi, respectively.
For example, let us consider the formula Σ1 showed at the end of section 3.2.
For this formula, we have:
Applying the recurrence (
It is not hard to propagate the computation of the charges for the nodes which were pre-processed by the Count M odels algorithm and that do not appear in GΣ , in fact, the same operator balance is applied for this task.
Notice that the computation of the charges of a 2-CF Σ has the same complexity order that the one used for computing #SAT(Σ). Thus, if the constrained graph of Σ does not contain intersecting cycles, then we compute all the charges of Σ in polynomial time. 4.
Independently that the computation of the charges of a KB Σ might require in the worst case an exponential time, knowing the charges as well as an evaluating order (GΣ ) are potentially useful in the area of propositional reasoning. For example in the field of model-based diagnosis, where is essential to determine all single assumptions (literals or clauses) that resolve an inconsistency, the evaluation order and the charges in Σ are useful for determining the best order in which the test of flaws in the digital circuits for consistency checking can be done [12, 8].
Other kind of applications where the charges can be useful is in the field of system planning, where the charges of a plan can be used for recognizing the frequency use of some operators, or in order to recognize which is the most frequently scenario of a trajectory that achieves some subgoals.
Other line of applications is in belief revision and updating knowledge bases. For example, consider an initial KB containing the clauses: {x} and {x, y}. One obvious implication of those clauses is the fact {y}. If a new information {y} has been observed by an intelligent agent, contradicting the assumption that y is true, so we will have to give up some (or all) of our previous beliefs, or it will lead to an inconsistent KB.
Many approaches for incorporating dynamically a single or a sequence of changes into an initial Knowledge Base (KB) have been proposed [1, 4, 6, 11]. Almost all of these proposals are plagued by serious complexity-theoretic impediments, even in the Horn case [4, 6]. More fundamentally, these schemes are not inductive, in the sense that they can lose in a single update any positive properties of the structure of the KB.
Even in the previous trivial example, it is not clear which approach should be taken. Usually, extra-logical factors should be taken into account, like the source and reliability of each piece of information or some kind of bias towards or against updates. For example, some methods for revision are based on some implicit bias, namely an a priori probability that each element of the domain theory requires revision [10].
Contrary to assign the probabilities to each element of the theory Σ by an expert or simply chosen by default, the charges of the variables provide a degree of their reliability in Σ. Furthermore, the dynamic updating of our representation of the KB gives the additional advantages that the relative values of the element of Σ can be adjusted automatically, in response to newly-obtained information.
In the rest of this chapter, we present only one of the applications in which the built logical structure and the charges of a 2-CF are useful. We try here the problem of computing the degree of belief of an intelligent agent on new information. 4.1.
Computing the Degree of Belief of an Intelligent Agent A generalization of deductive inference which can be used when a knowledge base is augmented by, e.i., statistical information, is to use the computation of a degree of belief, as an effort to avoid the computationally hard task of deductive inference.
If we assign an equal degree of belief to all ’basic situations’ that appear in a knowledge base Σ of an intelligent agent, then we can compute the probability that Σ can be satisfied. If Σ involves n variables, the probability to satisfy Σ, is: PΣ = P rob(Σ ≡ ) = #SA2nT (Σ) , where stands for the logical value true and P rob is used to denote the probability [13].
We are interested in the complexity of the computation of the degree of belief of a query (propositional formula) F with respect to Σ, which is considered as the fraction of models of Σ that are consistent with F , that is, the conditional probability of F with respect to Σ, denoted by PF |Σ and computed as: PF |Σ = P rob((Σ ∧ F ) ≡ |Σ ≡ ) = ##SASAT(TΣ(Σ∧F) ) .
We start assuming that the KB Σ is a satisfiable 2-CF, then #SAT(Σ) > 0 and PF |Σ = #SAT (Σ∧F ) is well-defined. One important goal of research is to #SAT (Σ) recognize the class of formulas for Σ and F where the computation of PF |Σ can be done efficiently, and for this, we need an appropriate representation of the knowledge base, as well as smart algorithms for solving #SAT.
Let Σ be a KB in 2-CF and let F be a query which is a unitary or binary clause, since for this case we have an inductive scheme for the incremental recompilation of knowledge which keeps the structure of the KB with updating actions. We assume that Σ has been processed by the procedures of the previous section and the charges of all variables in Σ have been stored in the array vars pairs.
Suppose that an agent A has to take an action according to a set of options Q = {l1, . . . , lk}. The classic deduction method suggests to choose the literals l ∈ Q which are consistent with Σ, that is, checking the satisfiability of (Σ ∪ l) for each l ∈ Q, recognizing equal value to all literals satisfiable with Σ.
But Pl|Σ provides more information than knowing that (Σ ∪ l) is satisfiable. Pl|Σ gives the proportion of the original models of Σ that remains models for (Σ ∪ l). This class of information is crucial when the agent A has to take an action depending on the strategic value of each alternative l ∈ Q. Indeed, A can decide its action according to the option l ∈ Q which maximizes its degree of belief. Then, we show now how to compute Pl|Σ and for this, we have two cases: 1. l ∈ Lit(Σ): As every variable xi ∈ υ(Σ) has associated its respective charge (αi, βi), we use v(l) as a pointer for the array vars pairs in order to recover (αυ(l), βυ(l)). Then, PF |Σ = µβ(υΣ(l)) if l is a negated variable or Pl|Σ = µα(υΣ(l)) otherwise. 2. l ∈/ Lit(Σ): Then we have new information not considered before and the original probability space for computing the conditional probability PF |Σ has to be extended.
When new pieces of information that did not originally appear in the sample space have to be considered, then we introduce in the area of updating the degree of belief by doing an extension of the original probability space [5]. Let consider here, a more general case.
k Let F = ( j=1 lj) be a conjunction of literals such that every variable of F does not appear in υ(Σ). Let | υ(Σ) |= n. There are 2n assignments defined over υ(Σ) and 2n+k assignments defined over υ(Σ) ∪ υ(F ), then we update the domain of the probability space for computing PF |Σ, as: µ(Σ∧F ) PF |Σ = P rPorb(oΣbΣ∧F ) = 2µn2(+nΣk) = µ2k(Σ·µ∧(ΣF)) . As GF and GΣ are two independent connected components and µ( l∈F l) = l∈F µ(l) = 1, then: PF |Σ = µ(Σ) · µ(F )
= 2k · µ(Σ)
µ(Σ)
2k · µ(Σ)
=
1
2k
(
Notice that in the first case, Pl|Σ is computed by one pointer access, one comparison and one division, then it has a constant time complexity. In general, least of the time for computing Pl|Σ is spent for determining the position of υ(l) in the array vars pairs. If we are not using hash techniques or pointers for ordering the variables, then in the worst case, we need a logarithmic time on the number of variables of the KB for determining the position of υ(l) in vars pairs (applying for instance a binary search).
Consider now the case when the set of options Q = {c1, . . . , ck} is a set of binary clauses and the agent A has to determine its future action based on the Pc|Σ: options codified by each clause. For example, A chooses its future action based on the clause c ∈ Q that maximizes its degree of belief with respect to the KB. Let c = {x, y} be any clause of Q, we have four cases for the computation of 1. x ∈/ Σ and y ∈/ Σ: There are three models out of the four assignments of υ(c) and, as the constrained graphs GΣ and Gc are independent, then Pc|Σ = µµ(Σ(Σ)·)µ·2(2c) = 3/4, since we extend the probability space with the new two variables: υ(x) and υ(y). This case is computed in constant time. 2. x ∈ Lit(Σ) and y ∈/ Lit(Σ): Then υ(x) is searched on the array vars pairs in order to retrieve (αυ(x), βυ(x)). According to the sign of x ∈ c we have that µ(Σ ∧ c) = 2 · αυ(x) + βυ(x) if x appears as unnegated variable in c, otherwise µ(Σ ∧ c) = 2 · βυ(x) + αυ(x). Then;
2·αυ(x)+βυ(x) if x appears as unnegated variable, Pc|Σ = 2·βυ(µx()Σ+)αυ(x) otherwise
µ(Σ) Notice that this case has a logarithmic time complexity over | υ(Σ) | since it mainly depends on retrieving the pair (αυ(x), βυ(x)) from the array of variables. 3. x ∈ Lit(Σ), y ∈ Lit(Σ) and c ∈ Σ: since c has been already computed in µ(Σ), µ(Σ ∧ c) = µ(Σ) and then Pc|Σ = 1. This case obtains the maximum possible value for Pc|Σ, so any alternative of action of the agent will take this option. 4. x ∈ Lit(Σ), y ∈ Lit(Σ) and c ∈/ Σ: Let consider for this option a more general situation, explained at once.
Let F = ( jk=1 lj) be a clause with k literals. Considering F as a set of literals, let A = {l ∈ F |υ(l) ∈/ υ(Σ)} be the literals in F whose variables do not appear in υ(Σ) and let F = F − A be the literals in F whose variables appear in υ(Σ), let t =| A |.
We compute µ(Σ ∧ F ) by extending the models of Σ with the new variables υ(A) and eliminating from this extended assignments those which falsify (Σ ∧F ), that is, µ(Σ ∧ F ) = µ(Σ) · 2t − µ(Σ ∧ F ), where F = ( jk=1 lj) = ( jk=1 lj).
As GA is a connected component independent of GΣ∪F , then F = A ∪ F
and µ(Σ ∧ F ) = µ(Σ ∧ F ) · µ(A) = µ(Σ ∧ F ) since µ(A) = 1, then:
PF |Σ = µ2(tΣ· µ∧(ΣF)) = µ(Σ) ·22tt ·−µ(µΣ(Σ) ∧ F )
µ(Σ ∧ F )
= 1 − 2t · µ(Σ)
(
We can consider F as a partial assignment on the number of variables in (Σ ∧ F ) since it consists of a set of literals. Let s = ( jk=1 lj) be an initial partial assignment defined over υ(Σ) ∪ υ(F ) which consists of 2n+t assignments. We can consider s as a partial assignment and try to extend it in order to count the total number of satisfying assignments for (Σ ∧ F ). If we consider s as a set of unitary clauses then s could be used in a unit reduction process with Σ, in order to build extended satisfying assignment s for (Σ ∧ F ).
We call the reduction of Σ by a literal l ∈ Lit(Σ) (also called f orcing l) and denoted by Σ[l] to the set of clauses generated from Σ by 1) removing all clause containing l (called subsumption rule), 2) removing l from all the remaining clauses (called unit resolution rule).
The unit reduction on a formula Σ consists of, given a unitary clause (l), performing a reduction of Σ for the literal of the unitary clause, that is, Σ[l]. Given the partial assignment s = ( jk=1 lj ), we define the reduction of Σ by s, as: Σ[s] = Σ[l1][l2] . . . [lk]. For short, we write Σ[l1, l2, . . . , lk] instead of Σ[l1][l2] . . . [lk]. We denote with Σ the resulting formula of applying unit reduction on Σ and s, that is, Σ = Σ[s].
Notice that a unit resolution rule can generate new unitary clauses. Furthermore, the unit resolution rule allows to extend the partial assignment s by the new unitary clauses appearing in this process, that is, s = s ∪ {u} where u is obtained by unit resolution rule in Σ[s]. If a pair of contradictory unitary clauses are obtained during this process then µ(Σ ∧ F ) = 0.
Unit Propagation U P (Σ, s) is the iterative process of doing unit reduction applying a set of unitary clauses (in our case s) over Σ until there are no more applications of unit reductions on the resulting formulas Σ .
When a subsumption rule is applied, we have to consider the set of variables in Σ which can be eliminated from Σ. For example, if we apply a subsumption rule on (x) ∧ (x ∨ y), both clauses are eliminated from Σ but if y has only one occurrence in Σ, then the subsumption rule eliminate y, but the total number of models for Σ has to consider that y can take any logical value. We introduce a new set Elim vars containing the eliminated variables by the application of the subsumption rule. Elim vars is checked in each application of the subsumption rule.
Then, the partial assignment s is applied on Σ in order to simplify the original KB by a more simple KB Σ , that is, Σ = U P (Σ, s) and then µ(Σ ∧ F ) = µ(Σ ) ∗ 2|Elim vars|.
If U P (Σ, c) generates the nil clause, then µ(Σ ∧ c) = 0 and this means that the initial clause c is logically deduced from Σ (Σ |= c), and then Pc|Σ = 1 − µµ(Σ(Σ∧)c) = 1. Furthermore, the generation of the nil clause in U P (Σ, c) takes a linear time on the number of clauses of Σ. Then, if we have the logical structure representation of Σ, the logical deduction task of proving Σ |= c for c a unitary or binary clause is solved in linear time.
Of course, if Σ c and υ(c) ⊂ υ(Σ) then there are cases where the computation of µ(Σ ∧ c) could require almost the same time that computing µ(Σ). However, as the resulting formula Σ of U P (Σ, s) is a subset of Σ, then GΣ is a subgraph of GΣ . In fact GΣ is formed by substructures of GΣ which are already computed during the computation of µ(Σ) and then, it is not necessary to re-compute such substructures. Thus, we only have to re-compute on the trajectories from x to y (the variables in c) what is modified from GΣ to GΣ . Example 4 Let Σ1 = {{x1, x2}, {x2, x3}, {x3, x4}, {x4, x5}, {x1, x4}, {x3, x5}, {x2, x6}} be an initial KB and the clause c = {x2, x5}. We want to compute Pc|Σ1 = 1 − 145 = 1115 .
Pc|Σ1. We know that µ(Σ1) = 15. F = (x2) ∧ (x5) and the partial
assignment to start the computation of µ(Σ1 ∧ F ) is s = F . Σ1 = Σ1[x2, x5] =
{{x3, x4}, {x4}, {x1, x4}, {x3}}, the clauses c1, c2 and c7 from Σ1 were subsumed
and then Elim vars = {x1, x6} are the eliminated variables in this iteration.
The new unitary clauses {x4} and {x3} are generated, extending the partial
assignment as s = (x2, x5, x4, x3) and such new unitary clauses are used in
the Unit Propagation procedure, then Σ2 = Σ1[x4, x3] = ∅. Then µ(Σ ∧ F ) =
µ(Σ2) · 2|Elim vars| = 1 · 22 = 4. And according to equation (
We can extend this process of deciding which action an intelligent agent has to take if the set of options are codified, for example, by a set of 2-CF’s, that is, Q = {F1, . . . , Fk} constitutes the set of alternative actions for an intelligent agent. Of course, for this latter case, the complexity time of computing PFi|Σ, i = 1, . . . , k is at least up to now, exponential and in this case, the previous knowledge about #SAT(Σ) and the charges of the variables may be not enough to reduce the time complexity of computing #SAT(Σ ∪ F ).
We have designed an appropriate logical structural representation of a 2-CF knowledge base. Our model-based system of reasoning includes cases where the formula-based approach does not support efficient reasoning. We show that using our logical structural representation, we can compute the degree of belief PF |Σ efficiently, when F is a query composed by literals or a binary clause which includes variables not appearing before in Σ. Indeed, for this case, we have an inductive scheme and the incremental recompilation of knowledge keeps the initial structure of the KB without losing with the updates, any positive properties of the structure of the KB, providing so, an efficient scheme of reasoning for an intelligent agent who has its knowledge base represented by a 2-CF.
Exploiting this logical structural representation of a 2-CF, we also propose a way to determine the relative value for all element in the KB which is an essential problem in some applications of deductive reasoning. Furthermore, the dynamic updating of our logical representation of the KB provides the additional advantage that the relative value of the elements of Σ could be adjusted automatically in response to newly-obtained information.