Assuming a Knowledge Base Σ expressed by a two Conjunctive Form (2-CF), we show that if the constrained graph of Σ is acyclic or if its cyles are independent one to the other, then it is possible to count efficiently the number of models of Σ. We determine a set of recurrence equations which allow us to design an incremental technique for counting models by a simple traversal of the constrained graph. One of the advantages of such technique, furthermore that it has linear time complexity, is that applying it backwards allows us to determine the exact number of the logical values (the charge) that each variable has in the set of models. The charge of each variable allow us to design an efficient scheme of reasoning, even in the case where the formula-based representation does not allow to do it. Indeed, we can compute the degree of belief for new information (a literal or a binary clause) efficiently.
The Artificial Intelligence 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 [
As it has been pointed out in [
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, for processing here we mean to compute the degree of belief, updating or doing belief revision.
In order to clarify a frontier between efficient and exponential-time reasoning, we start working with a Knowledge Base (KB) Σ in two Conjunctive Form (2CF), and we consider queries also in 2-CF. We want to compute the degree of belief that an agent has in a new piece of information F based on the conditional probability of F with respect to Σ, denoted as PF |Σ , and calculated as the fraction of models of Σ that satisfy F .
One important goal of research is to recognize the class of formulas for Σ and F where the degree of belief PF |Σ can be computed efficiently, and for this, the development of smart algorithms for solving the #SAT problem is key.
#SAT consists of counting the number of models of logical formulas. #SAT is
a classical #P-complete problem, and an interesting area of research has been the
identification of restricted cases for which #SAT can be solved efficiently. #SAT
remains #P-complete even if we consider only monotone or Horn propositional
formulas [
We focus toward the identification of structures on the constrained graph of formulas in 2-CF, such that these structures help us to compute #SAT efficiently. Furthermore our interest is to design procedures which count the number of models of a given formula in an incremental way, at the same time that we are traversing by the constrained graph of the formula.
Given our logical structure representation of a 2-CF, we propose procedures for determining 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.
We use υ(X ) to express the variables involved in the object X , where X could be a literal, a clause or a CF. For instance, for the clause c = {x1, x2}, υ(c) = {x1, x2}. Lit(F ) is the set of literals appearing in F , i.e. if X = υ(F ), then Lit(F ) = X ∪ X = {x1, x1, ..., xn, xn}. We 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 from F , and υ(F1) ⊂ υ(F ), 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 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 . 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. 3.
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(Σ).
In order to compute #SAT (Σ), first we should determine the set of connected
components of GΣ and this can be done in linear time. Then, #SAT (Σ) is
translated to compute #SAT (G) for each connected component G of GΣ [
Each edge has associated an ordered pair (s1, s2) of signs, assigned as labels. For example, the signs s1 and s2 for the clause {x ∨ y} are related to the signs of the literals x and y respectively, then s1 = − and s2 = + and the edge is denoted as: x − + y which is equivalent to the edge y + − x.
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 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 of x (y).
Let GΣ = (V, E, {+, −}) be a signed connected graph of an input formula Σ in 2-CF. Let vr be a node of GΣ 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}, where each back edge ci ∈ E marks the beginning and the end of a fundamental cycle.
Given any pair of fundamental 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 AΣ 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 DΣ, assigning an orientation to each edge {u, v} in AΣ by directing: u → v if v is the parent node of u in TG, see figure 2. We apply a topological sorting procedure on DΣ, obtaining an ordered number o associated with each node in DΣ such X 1 X 1
X2 X 8
X2 X8
X 5
X4
X 6
that o(u) < o(v) whenever u → v. This order number indicates the order for
processing the nodes in DΣ when we compute the value #SAT(Σ) in the next
subsection.
In previous papers, we have presented a set of recurrence equations to compute
#SAT(Σ) by traversing DΣ [
For each variable x ∈ υ(Σ) a pair (αx, βx) called the initial charge, is used for indicating the number of logical values: ’true’ and ’false’ respectively, that x initially took when the value #SAT(Σ) is being computed.
When we count models over a constrained graph DΣ, we use computing threads. A computing thread is a sequence of pairs (αi, βi), i = 1, . . . , m used for computing the number of models over a path of m nodes. A main thread, denoted by Lp, is associated with the spanning tree of DΣ. This thread is always active until the process of counting finishes completely. We sketch now the general procedure for computing #SAT(Σ).
Procedure Count M odels(Σ) Input: DΣ: a constrained graph of a 2-CF Σ Output: The charge (αy, βy) associated with the root node y, where #SAT(Σ) = αr + βr
Each node and edge of DΣ is visited according with the topological order, and at the same time a pair (αx, βx) is computed for each node x ∈ DΣ, in the following way: 1. (αx, βx) = (1, 1) if x is a leaf node in DΣ. 2. When there is an unique edge between two nodes, e.g. x s1 s2 y is an edge → with signs s1 and s2 then according with the signs (s1, s2) the pair (αy, βy) is computed from (αx, βx) (in parallel way it is done for all computing active thread), as:
⎧ (βx ,αx + βx) if (s1, s2) = (−, −) (αy, βy) = ⎨⎪⎪ (αx + βx,βx ) if (s1, s2) = (−, +)
(αx ,αx + βx) if (s1, s2) = (+, −) ⎪⎪⎩ (αx + βx,αx ) if (s1, s2) = (+, +) (1) We denote with → the application of anyone of the four previous rules in the recurrence (1). 3. If v is a parent node with a list of child nodes associated, i.e., u1, u2, ..., uk are the child nodes of v, as we have already visited all child nodes, then each pair (αui , βui ) i = 1, ..., k has been determined based on recurrence (1). And then, let αv = jk=1 αuj and βv = jk=1 βuj . We denote with the application of this multiplicative rule. 4. If the node y begins of a cycle C then a new computing thread LC is created.
The initial pair associated to the computing thread LC is (0, βy) if s1 = +, or (αy, 0) if s1 = −, where (αy, βy) is the current pair for the node y in the thread Lp and s1 is the sign of x in the back edge of the cycle C. 5. If y ends a cycle C, then the current pair (αyc , βyc ) in the the extra-computing thread LC is substracted to the current pair (αy, βy) of the main thread Lp, according with the sign s2 in the back edge of the cycle C, in the following way: if s2 = + then (αy, βy) = (αy, βy − βyc ) or (αy, βy) = (αy − αyc , βy) if s2 = −. We denote by ’ ’ the binary operation between the two active threads for computing the initial charge of the node which closes a cycle. 6. If y is the root node of DΣ then returns its computed charge: (αy, βy).
To illustrate this procedure, we apply it on the DAG of figure 2, assuming a monotone 2-CF, that is, all variable appear in nonnegative way and then the last rule of recurrence (1) is always applied, denoted by an arrow with a dotted line in figure 3, while the operator ’ ’ is shown by a line like an substracted operator. For this example, the topological order is: x3 → x6; x9 → x6; x6 → x4; x9 → x4; x4 → x5; x5 → x2; x4 → x2; x7 → x8; x8 → x2; x2 → x1; x7 → x1 . (2) (3)
In [
Computing the Charges of a 2-CF In this section, we present a novel method for computing the charge (αi, βi), i = 1, . . . , n for all variables xi, i = 1, . . . , n of a 2-CF Σ. Once the previous algorithm has been applied for computing #SAT(Σ) and the inital charges has been computed for all variables in Σ. In fact, the initial charge (αn, βn) for xn is also its final charge, that is, #SAT(Σ) = αn + βn.
Let A1, . . . , An be the sequence of initial charges obtained during the application of the procedure Count M odels. Given such sequence, we build a new sequence of pairs which represent the final charges (or just the charges) Bn, . . . , B1 where Bi is the charge for the variable xi ∈ υ(Σ), which is computed as: Bn = An
Bn−i = balance(An−i, Bn−i+1), i = 1, ..., n − 1 where balance(A, B) is a binary operator between two pairs, e.g if the edge x s1 s2 y exists, then A = (a, a ) is the initial charge of the variable x and B is → the charge of the variable y, then balance produces a new pair (αx, βx) which is the final charge for x, that is, #SAT(Σ) = αx + βx.
Let P1 = a+aa and P0 = a+aa be the proportion of the number of 1’s and 0’s in the initial charge of the variable x. Let µy = αy + βy. Then the charge (αx, βx) is computed, as: αx = αy · P1 + βy; βx = µy − αx if (s1, s2) = (+, +) βx = βy · P0 + αy ; αx = µy − βx if (s1, s2) = (−, −) βx = βy · P0 + αy ; αx = µy − βx if (s1, s2) = (+, −) αx = αy · P1 + βy; βx = µy − αx if (s1, s2) = (−, +)
Note that the essence of the recurrence balance consists in applying the inverse of the operation used at each step of the computation of #SAT(Σ), and following the inverse order used in the construction of the sequence A1, . . . , An. Thus, it follows an inverse topological order on the nodes of DΣ.
Futhermore, in the case of the bifurcation from a father node to a list of child nodes (operation ), the same equation remains valid since each branch has its respective pair of signs. The unique new operation to consider is the case where a cycle was processed, that is, when a back edge is found when computing the charges.
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 in Σ in polynomial time. 4.
An important result is that we can apply the inverse action realized in each step of the procedure Count M odels in order to propagate the final charge of the last visited variable to all other variables. Then, our polynomial procedures permit us also to know the number of models for the KB Σ and its inverse procedures allow us to propagate that final charge (the number of 1’s and 0’s into the set of models) associated with all variable in the KB.
Knowing the charge of each variable is 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 [
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.
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 [
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.
For example, if a 2-CF Σ codify the KB of an intelligent agent which has to take decision according with a set of options Q = {C1, . . . , Ck}. In order to take the best decision, the intelligent agent has to recognize which option maintain the maximum of consistency with his KB. In other words, it is essential to compute the degree of belief that the agent has over each option and to select the option assuring the maximum degree of belief.
In the rest of this paper, we present only one of the applications in which to built logical structure and the charges of a 2-CF are useful. We adresse 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
We assume 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 [
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, 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 [
Let F = ( jk=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: Indeed, for the case k = 1, an agent A believes in new information not related with its knowledge base with a reliability of 0.5. Since we extend the models of Σ for considering a new variable υ(l), half of those extension assignments have υ(l) true and the other half have υ(l) false. We have that the fraction of models of Σ which are consistent with {l} is 1/2 and the other half is consistent with {l}.
Note 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, the maximum of the time for computing Pl|Σ is spent for determining the position of υ(l) in the array vars pairs which can be done in a constant time.
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 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 computing Pc|Σ: 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
µ(Σ) 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:
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].
Note that a unit resolution rule can generate new unitary clauses. Furthermore, it 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Σ . Pc|Σ1 = 1 − 145 = 1115 .
Example 1 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. 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 (5), we have that
We have designed an appropriate logical structural representation of a 2-CF knowledge base. Our model-based reasoning system 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 provide 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 elements 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.