domain: info math

text:
Daniel Goossens
email: danielgoos.ia@gmail.com

Graphs of Bipartitions with Dimensions : a tool for interacting with virtual Boolean lattices. Working document

This document describes a Boolean knowledge representation and reasoning formalism called Graphs of Bipartitions. A Graph of Bipartitions is a knowledge storage framework that interacts with a virtual Boolean hypercube. It groups equivalent expressions, removes contradictory expressions, and memorizes logical implications using polynomially bounded reasoning. It thus maintains a uniqueness principle to continuously growing substructures. This formalism and its management operations have been applied to a demonstration of a natural language interaction on a micro-universe.

This document formalizes this previously experimented proposition for managing Boolean knowledge. One important mechanism is the deduction of modulo 2 linear equations, in connection with the calculation of dimensions of the virtual hypercube. These equations gradually extend a linear system within Boolean knowledge. Gaussian elimination combined with propagations of Boolean values constitutes a polynomially bounded reasoning. This reasoning is protected from any combinatorial explosion. It is locally complete to intertwined substructures in constant expansion and in potentially exponential number, where it reduces to set operations on finite sets of dimensions.

Introduction

This working document deals with the problem of memorizing Boolean knowledge in a database while maintaining a principle of uniqueness: two different but equivalent Boolean expressions must be stored in the same place. We can also wish for a principle of complete classification: using Boolean implication as a primitive, two expressions x and y such as x ⇒ y must be stored so that there is a path of implications from x to y.

If these principles are maintained, the places where Boolean expressions are stored are vertices of a virtual hypercube. Two equivalent expressions are represented by the same vertex of the hypercube. The hypercube is partially represented by a directed graph whose arcs are implications. As the Boolean implication is insufficient to represent Boolean constraints between the vertices of this partial graph, it is completed by a system of linear equations modulo 2.

To maintain the principles, reasoning may be based on a complete Boolean satisfiability test. For example, when a Boolean expression is created, it must be compared for equivalence or implication with each stored expression. However, if the test is triggered too often, the storage time for new knowledge becomes prohibitive with the increase in the size of the database. We must either limit and compartmentalize the triggering of the complete test while maintaining the completeness of the reasoning, or do without it and accept that the principles of uniqueness and classification be complete only locally to substructures.

The incremental construction of the hypercube, by polynomially bounded operations, formalizes an intuitive notion of navigation in a virtual hypercube, and an intuitive notion of inter-classification of knowledge.

The context

The problem of maintaining a uniqueness principle on a knowledge base is ubiquitous in logic. Recognizing the same concept under different descriptions is a crucial understanding skill. Also, gathering the equivalent expressions in a single place of the virtual hypercube and maintaining the Hasse diagram of the implications between vertices, as one memorizes knowledge, simplifies all subsequent reasoning, unlike a solution which would content itself with accumulating the expressions without inter-classifying them.

In the Boolean world, the uniqueness principle concerns things as diverse and fundamental as distributive lattices, the hypercube, partial orders, propositional knowledge bases or the word problem on algebraic structures. It does not have a dedicated bibliography. On the other hand, we can cite the state of the art in generalist complete Boolean reasoning, namely SAT-solving.

Sat-solving [START_REF]Handbook of Satisfiability[END_REF] is currently the most efficient complete satisfiability test for Boolean reasoning. In the field of decision problem solving, in artificial intelligence, this general-purpose technique currently dominates other approaches, in particular local search strategies, classes of expressions of polynomial complexity, BDDs [START_REF] Bryant | Graph-based algorithms for boolean function manipulation[END_REF] and their successors, or order encodings by bit vectors (see for example [START_REF] Aït-Kaci | Efficient implementation of lattice operations[END_REF]). To manage the inescapable difficulty of reasoning at order 0, higher-order logical approaches often ultimately rely on a complete Boolean satisfiability test performed by a SAT-solver, for example [START_REF] Ramachandran | Compact propositional encoding of first-order theories[END_REF], [START_REF] Sebastiani | Handbook of Satisfiability, chapter 32. SAT Techniques for Modal and Description Logics[END_REF] or [START_REF] Giunchiglia | Sat-based answer set programming[END_REF]. However, this complete test is exponential in the worst case. In practice, it is too costly for the reasoning needed by the management of Boolean knowledge considered here. It should be used sparingly.

The inter-classification of Boolean expressions in a propositional knowledge base is analogous to the inter-classification of knowledge in [START_REF] Baader | The Description Logic Handbook: Theory, Implementation and Applications[END_REF] description logics, by subsumption links.

Main objectives

Knowledge storage and maintenance operations must be protected from any combinatorial explosion or too long calculation times. The main objective is to separate these operations, based on incomplete reasoning, from those oriented towards problem solving and based on a complete satisfiability test. It is then a question of determining conditions under which the Boolean reasoning is complete locally to substructures.

To obtain storing operations that verify the uniqueness principle via a complete Boolean reasoning, another objective is to reduce and compartmentalize the use of the complete satisfiability test.

A longer-term goal is the automation of understanding abilities based on symbolic reasoning, in micro-worlds that lend themselves to Boolean modeling.

Actual state

This document formalizes what was experimented in [START_REF] Goossens | Modélisation d'une forme simple de compréhension[END_REF], an incomplete and polynomially bounded Boolean reasoning, augmented here with a reasoning on the dimensions of a virtual hypercube. This reasoning aims to locally maintain the principles of uniqueness and complete classification on a Boolean knowledge base. This maintenance stores knowledge in Graphs of Bipartitions. A Graph of Bipartitions is a partial representation of a virtual hypercube. This maintenance of a partial representation of a virtual hypercube acts as a cache that memorizes the simplest and most frequent deductions.

A Graph of Bipartitions combines an implication graph and a system of modulo 2 linear equations on Boolean variables. The linear system is progressively enriched by deduction of new equations. These equations are deduced by reasoning on the dimensions of the virtual hypercube. This continually increases the deductive power of Gaussian elimination, an efficient polynomial reasoning and therefore immune to any combinatorial explosion. The particular role of the linear component in Boolean knowledge, since [START_REF] Stone | The representation of boolean algebras[END_REF], is evident in T.J. Schaefer's dichotomy theorem [START_REF] Thomas | The complexity of satisfiability problems[END_REF] and in its treatment by Gaussian elimination in SAT-solving [START_REF] Baumgartner | The taming of the (x)or[END_REF] .

The tools and reasoning described here are programmed in C++ and Objective-C under MAC OS. All the diagrams in this document were produced with the interactive editor. The Boolean reasoning presented here is a construction site that allows to study all kinds of combinations capable of providing a usable solution to manage Boolean knowledge.

The main result is the local completeness proof of a polynomially bounded Boolean reasoning, the propagation of valuations expressed as systems of modulo 2 linear equations. The Boolean reasoning that ensures the storage of knowledge in a Graph of Bipartitions gradually develops substructures, where the Boolean operators are reduced to set operations on finite sets of dimensions of the virtual hypercube. These substructures are intertwined and in potentially exponential number, therefore not enumerable. However, locally at each substructure, the Boolean reasoning is complete and polynomially bounded.

A demonstration of the use of Graphs of Bipartitions to model a simple understanding in the microuniverse of the intuitive geometry of elementary school level quadrilaterals, is presented in [START_REF] Goossens | Modélisation d'une forme simple de compréhension[END_REF]. This document formalizes the solutions experimented in this demonstration and adds the machinery related to the dimensions of the virtual hypercube.

Document outline

The 2 paragraph recalls some prerequisites and establishes a link between the dimensions of the hypercube and Boolean reasoning, which is used in the 5 paragraph. The 4 paragraph presents the Graphs of Bipartitions. The paragraph 5 presents the polynomial reasoning on Graphs of Bipartitions. It analyzes the spontaneous development of substructures where Boolean reasoning is locally complete. It describes the computation of dimensions from linear equations and linear equations from dimensions. The paragraph 6 presents propagation-like polynomial reasonings and demonstrates their completeness, locally to these substructures. The paragraph 7 cites some achievements and perspectives and the paragraph 9 concludes.

Preliminaries

Graphs of bipartitions combine a graph of implications and a system of modulo 2 linear equations over Boolean variables. They induce Boolean hypercubes. Therefore, some terminology from graph theory, modulo 2 linear equations and Boolean hypercubes is needed.

Graphs

A graph is a couple S, A where S is a set of vertices and A is a set of edges. Each edge of A is a pair of vertices of S. A chain from a vertex x to a vertex y is a finite sequence of consecutive edges connecting x to y. An directed graph is a graph where the edges, renamed arcs, are oriented. An arc from a vertex x to a vertex y is written x → y. A path from vertex s 1 to vertex s n is a finite sequence of arcs {s 1 → s 2 , s 2 → s 3 , . . . , s n-1 → s n }.

The Cartesian product [START_REF] Imrich | Topics in Graph Theory: Graphs and Their Cartesian Product[END_REF] of two graphs G = S g , A g and H = S h , A h is the graph G H = S, A , where:

S = S g × S h A = {{g 1 × h 1 , g 2 × h 2 } | g 1 ∈ S g ∧ g 2 ∈ S g ∧ h 1 ∈ S h ∧ h 2 ∈ S h ∧ (((g 1 = g 2 ) ∧ ({h 1 , h 2 } ∈ A h )) ∨ ((h 1 = h 2 ) ∧ ({g 1 , g 2 } ∈ A g )))}
Therefore, the vertices of G H are the elements of the Cartesian product of the vertices of G and H and two vertices of G H have an edge if and only if the vertices of which they are the products have an edge in G or H. The graph G H therefore contains as many copies of G as there are vertices in H and vice versa.

Modulo 2 Linear Equations

Graphs of Bipartitions use systems of linear equations over the two-element field F 2 . The addition on F 2 is denoted ⊕ and corresponds to the Boolean connector XOR. Each linear equation on F 2 can be put in the form ( n i=1 v i ) = constant, where the v i are Boolean variables and constant ∈ {0, 1}. A system of equations is homogeneous if and only if constant = 0 for all equations. The ⊕ operation is associative and commutative. The variables can thus be rearranged freely in a polynomial. It also verifies for all x the identity x ⊕ x = 0. Monomials in an equation can be moved to either side of the = sign. For example, the equation x ⊕ y = 0 is the same as x = y. Also, the equation x ⊕ y = 1 is x = y.

Adding two equations e1 = e2 and e3 = e4 gives the implied equation e1 ⊕ e2 = e3 ⊕ e4, which is also e1 ⊕ e2 ⊕ e3 ⊕ e4 =0. This addition is the basic operation of Gaussian elimination for solving a system of equations. Gaussian elimination is complete for the deduction of the equations 0 = 0 (tautology), 1 = 0 (contradiction), x = 0 or x = 1 (valuation). It is also complete for the deduction of the equations x = y (equivalent vertices), which can also be in the form (x = V ) ∧ (y = V ) and for the equations x = y (i.e.

x ⊕ y = 1), which can be in the form (x = V ) ∧ (y = (V ⊕ 1)).

The Boolean Hypercube Q n

The n-dimensional hypercube graph Q n has 2 n vertices. Each vertex represents one of the 2 n subsets of the set {1 . . . n}. The subset v x associated with a vertex x is its characteristic vector.

Each edge of the graph connects two vertices x and y such that v x and v y differ in a single element. Their symmetric difference is a singleton. This singleton is the atomic dimension of the edge. We write a ⊕ b for the symmetric difference of two sets a and b of dimensions, rather than a∆b, in accordance with modulo 2 linear equations. We orient the edge as the arc x → y if v x ⊂ v y and y → x otherwise. On the diagrams, the arc x → y is drawn by a line from the top of x's bounding rectangle to the bottom of y's bounding rectangle. The dimension of any pair of vertices {a, b} is the set v a ⊕ v b . We write it dim(a, b). The lower bound or inf of Q n is the vertex ⊥ such that v ⊥ = ∅. Its upper bound or sup is the vertex such that v = {1 . . . n}.

In the Boolean hypercube, all the chains between two vertices where each atomic dimension appears only once have the same length k and the same dimension. They correspond to the k! permutations of the sequence 1 . . . k . Consider three vertices a, b, c of

Q n . We have dim(a, c) = v a ⊕ v c = v a ⊕ v b ⊕ v b ⊕ v c = dim(a, b) ⊕ dim(b, c).
The dimension of a pair of vertices is therefore the sum ⊕ of the atomic dimensions of the edges on any chain between the two vertices. It is also the set of atomic dimensions of the edges on a chain where all the edges are of different dimensions. See figure 1. Two dimensions E and F are orthogonal, denoted E ⊥ F , if and only if E ∩ F = ∅. For more flexibility, we interpret in the following the n of Q n not as an integer but as a set of atomic dimensions. Q n is then the Boolean hypercube of dimension |n|, with 2 |n| vertices, whose arcs are labeled with the elements of the set {1 . . . n}, written n. For example, Q {1,3,5} represents a "copy" of Q 3 where arcs are labeled with the dimensions 1, 3 and 5. The Cartesian product of Q n and Q m is still written Q n+m but the operation + is the union of two sets n and m, which are necessarily disjoint.

By the definition of the dimension of a pair of vertices, two copies

Q dim(a,b) and Q dim(c,d) in Q n of a Boolean hypercube Q e , i.e. verifying dim(a, b) = dim(c, d) = e, also verify (v a ⊕ v b ) = (v c ⊕ v d ), and therefore ((v a = v b ) = (v c = v d ))
. This principle is implicit in the proof of proposition 1.

The vertices of Q n are Boolean variables and its arcs are implications between these variables. In a Boolean hypercube, the Boolean implication x → y between any two vertices x and y is equivalent to the fact that there is a path from x to y.

A Graph of Bipartitions, like any Boolean formalism, can be interpreted as a toolbox for navigating in a virtual Boolean hypercube. The objective here is to relate the dimensions of the virtual hypercube to a Boolean reasoning on a Graph of Bipartitions. To do this, we use this recursive definition of the Boolean hypercube Q n , which allows all possible decompositions into Cartesian products: Note: The hypercube Q 0 , or Q {} , reduced to 1 vertex, is not useful for defining Graphs of Bipartitions. The hypercube Q n+m contains 2 |m| copies of Q n and 2 |n| copies of Q m . The vertices of each copy of Q m are the 2 |m| copies of one of the 2 |n| vertices of Q n and symmetrically, the vertices of each copy of Q n are the 2 |n| copies of one of the 2 |m| vertices of Q m (Figure 2).

Dimensions and Boolean reasoning

The hypercube Q n is a Boolean lattice. That is, some subsets of its vertices are generators from which every other vertex may be represented as a Boolean expression (Figure 3). For any pair of vertices x and y, the equivalence "x and y have the same Boolean value", noted x = y, defines an equivalence relation on Q n : two vertices s and t are equivalent if and only if dim(s, t) ⊆ dim(x, y). The quotient hypercube by this equivalence relation is Q n\dim(x,y) (Figure 4). The proposition 1 uses these properties and conversely, from the inclusion or the disjunction of dimensions of paths, we deduce Boolean implications. The proof is a simple translation between the set-theoretic language of dimensions and the Boolean language. The set ∅ corresponds to the Boolean value 0 (false) and the set n of dimensions of Q n to the value 1 (true). To the characteristic vector v s of vertex s corresponds the Boolean variable s.

Proof. Let us prove the two properties separately:

To prove (1), By the definition of the dimension of a pair of vertices,

(dim(a, b) ⊆ dim(c, d)) ⇐⇒ ((v a ⊕ v b ) ⊆ (v c ⊕ v d )). As a → b and c → d, (v a ⊕ v b ) = (v b \ v a ) and (v c ⊕ v d ) = (v d \ v c ). In Boolean language, (dim(a, b) ⊆ dim(c, d)) ⇐⇒ ((v b \ v a ) ⊆ (v d \ v c )) is written: (dim(a, b) ⊆ dim(c, d)) ⇐⇒ ((a ∧ b) =⇒ (c ∧ d)). To prove (2), If dim(c, d) is disjoint of dim(a, b) then it is included in its complement : (dim(a, b) ⊥ dim(c, d)) ⇐⇒ (dim(c, d) ⊆ (n \ dim(a, b))) ⇐⇒ ((v c ⊕ v d ) ⊆ (n \ (v a ⊕ v b )))
We replace in (2):

((v c ⊕ v d ) ⊆ (n \ (v a ⊕ v b ))) ⇐⇒ ((a ∧ b) =⇒ (c = d)) (3)
If (a ∧ b) then v a = ∅, v b = n and (n \ (v a ⊕ v b )) = (n \ (∅ ⊕ n)) = (n \ n) = ∅. ((v c ⊕ v d ) ⊆ (n \ (v a ⊕ v b ))) becomes ((v c ⊕ v d ) ⊆ ∅) then ((v c ⊕ v d ) = ∅) and then (v c = v d ),
which is written in Boolean language c = d (c and d have the same Boolean value).

Similarly, (a

∧ b) is (v b \ v a ) = (n \ ∅) = n, which is written 1 (true) in Boolean language.
By replacement by these equivalences, the equivalence (3) becomes:

(c = d) ⇐⇒ (1 =⇒ (c = d)), i.e. (c = d) ⇐⇒ (c = d), which is a tautology. Otherwise, ((a → b) ∧ ¬(a ∧ b)) implies a = b, so dim(a, b) = ∅. (dim(a, b) ⊥ dim(c, d)) is true and (a ∧ b) is false. The equivalence (2) becomes (1 ⇐⇒ (0 =⇒ (c = d))), which simplifies to 1 ⇐⇒ 1.
From the equivalence (1) of the proposition 1, we deduce:

(dim(a, b) = dim(c, d)) ⇐⇒ ((a ∧ b) ⇐⇒ (c ∧ d)) ⇐⇒ ((a = b) ⇐⇒ (c = d))
This last equivalence allows to determine which implications have the same dimension in a Graph of Bipartitions. More generally, the proposition 1 links a Boolean reasoning on the vertices of a hypercube, to a set reasoning on the dimensions of the paths of this hypercube. It is exploited in the paragraph 5 in the computation of the dimensions of the implications of a Graph of Bipartitions and the deduction of linear equations modulo 2.

The Graphs of Bipartitions

A Graph of Bipartitions (GB) is a substructure of the graph of a hypercube Q n . The GB induces this Q n , i.e. is completed in this Q n using Boolean operators. This idea starts in [START_REF] Goossens | Automatic Node Recognition in a Partitioning Graph: Restricting the Search Space While Preserving Completeness[END_REF], where Boolean expressions are represented with bipartitions as Boolean operators. In [START_REF] Goossens | Automatic Node Recognition in a Partitioning Graph: Restricting the Search Space While Preserving Completeness[END_REF], each bipartition x = y + z is equivalent to the Boolean expression (x = (y ∨ z)) ∧ ¬(y ∧ z). The bipartitions used until [START_REF] Goossens | Boolean reasoning with graphs of partitions. version longue du papier court "A Dynamic Boolean Knowledge Base[END_REF] become more abstract in [START_REF] Goossens | Modélisation d'une forme simple de compréhension[END_REF]. This makes it possible to recover the symmetry of the dual operators ∧ and ∨ and to considerably simplify the graphs.

Each bipartition is now a quadruple x, y, x ∨ y, x ∧ y . A bipartition is built with four implications and a linear equation modulo 2. It is a representation of the Boolean hypercube Q 2 , or of the tautology (x ⊕ y ⊕ (x ∧ y) oplus(x ∨ y)) = 0. See figure 6.

The vertices of the GB, called nodes, represent vertices of Q n . The arcs of the GB represent paths of Q n . Each arc is therefore an implication between its two vertices and its dimension is that of the path it represents.

For the implication between two nodes x and y of a GB, we must distinguish three cases:

1. x → y is deducible from the GB without a path of implications from x to y. We write it x ⇒ y. This case is possible when reasoning is incomplete.

2. There is a path of implications from x to y. We write it x → y.

3. The GB contains an arc x → y. We explicitly mention the "arc" or the "implication" x → y.

The dimensions of the implications of a GB and the characteristic vectors of its vertices are theoretical objects, too expensive to calculate in extension. One can on the other hand calculate constraints of inclusion and disjunction between these dimensions. This calculation can be done from a Boolean propagation, using the two equivalences of proposition 1. If the valuation (a = 0 ∧ b = 1) propagates (c = 0 ∧ d = 1), we can note that (dim(a, b) ⊆ dim(c, d)), and if it propagates (c = d), we can note that (dim(a, b) ⊥ dim(c, d)). This collected information can in turn be used to extend a valuation.

Let a, b, c, d be four nodes of a GB. The constraint dim(a, b) Definition 3. A Graph of Bipartitions (GB) is a triple N, I, S , where N is a set of nodes, I a set of implications between these nodes and S is a set of linear equations modulo 2 on these nodes. It is also the conjunction I ∧ S , where I is the conjunction of the implications of I and S is the conjunction of the equations of S. It is constructed using the rules:

= dim(c, d) is also written (v a ⊕ v b ) = (v c ⊕ v d ). As the nodes a, b, c, d represent the characteristic vectors v a , v b , v c , v d ,
1. The implication ⊥ → is a GB. It is the triple {⊥, }, {⊥ → }, {} .

2. Given two nodes x and y of a GB G, such that x → y, then divide(x, y, G) is a GB.

3. Given two nodes x and y of a GB G, such that ¬(x → y), then cross(x, y, G) is a GB. 4. Given three nodes x, y and z of a GB G, such that x → y and y → z, then complement(x, y, z, G) is a GB.

The nodes ⊥ and of the base case 1 are respectively the inf and the sup of the GB. They are conserved by the other construction rules.

The operation divide(x, y, G) adds to G the path (x → z) ∧ (z → y), where z is a new node. In other words, divide(x, y, G) = G ∧ (x → z) ∧ (z → y). The node z is not a Boolean function of the nodes of G. There is no need to check if it already exists or if it has to be connected by implications to other nodes in the GB. This operation is used to construct a graph of implications between nodes.

The operation cross(x, y, G) adds to G the bipartition x, y, a, b . The two added nodes a and b are respectively x ∨ y and x ∧ y. The operation complement(x, y, z, G) adds to G the bipartition y, c, z, x . The created node c is the complement of y between x and z, ie c = ((z ∧ y) ∨ x). The operations cross and complement only add Boolean functions of the nodes of G.

The operations cross and complement

The operation cross constructs or recognizes the expressions x ∨ y and x ∧ y from two nodes x and y. The complement operation constructs or recognizes the local complement of a node x between two nodes y and z. These constructions are done by adding a bipartition to the GB. These operations eventually recognize the nodes already present and they classify the created nodes. They update the relations of inclusion and disjunction between the dimensions of the implications of GB. See figure 7.

Figure 7: The GB G2 is divide(0, 1, G1). G3 is divide(0, 1, G2). Despite appearances, G3 is not a representation of the square Q 2 because the node 1 is not x ∨ y and the node 0 is not x ∧ y. GBs are not partial order diagrams that statically indicate sups and infs. The GB G4 is cross(x, y, G3). The GB G5 is G4 with 6 local complements added. the GB G6 (whose 11 equations are hidden for more readability) is the completion of G5 by cross or complement. G6 is a representation of the hypercube Q 4 . G3 is therefore a partial representation of Q 4 . Definition 4 (cross). Let G be a GB and let x and y be two nodes of G such that there is no path from x to y. cross(x, y, G) = 1. Build the bipartition x, y, a, b , where a and b are two new nodes. The bipartition makes a = x ∨ y and b = x ∧ y.

2.

For each s such that (x → s) and (y → s), add the implication (a → s) to G For each s such that (s → x) and (s → y), add the implication (s → b) to G 3. Classify a and b in G.

Definition 5 (complement). Let G be a GB and let x y and z be three nodes of G such that x → y and y → z. complement(x, y, z, G) = 1. Build the bipartition c, y, z, x .

Classify c in G.

Classifying a node n in a GB G consists in connecting it with implications to its most general implicants and its most precise implicates already constructed : Definition 6. Classify a node n in a GB G = For any node x of G such that (n ⇒ x) with no path from n to x, add the implication (n → x) to G. For any node x of G such that (x ⇒ n) with no path from x to n, add the implication (x → n) to G.

Delete, Merge, Forget

Some linear equations deduced from a non-valuated GB transform it. The equations x = 0 make x a contradictory node, which must be deleted. The equations x = y merge the nodes x and y into a single node. Also, a node that can be rebuilt if needed, may be forgotten.

After these operations modify the GB, it is necessary to update the dimensions of its implications. The complexity of these operations may be significant since they trigger Gaussian eliminations. It remains polynomially bounded because the number of nodes to delete or pairs of nodes to merge is bounded by the number of nodes of the GB.

Removing a conflicting node

To remove a conflicting node x:

1. Add x and its descendants in the graph of implications, to a queue of nodes to be deleted. Remove implications whose nodes are both in the queue.

2. Remove queued nodes.

3. If nodes have been deleted, solve the linear system, which may add nodes to the queue, and return to 2.

To remove a queued node x:

1. Remove implications x → y.

2. Simplify linear equations containing x, by replacing x with 0.

3. Free isolated node x.

Merging two equivalent nodes

To merge two equivalent nodes x and y:

1. Remove the implication x → y or y → x if it exists.

2. Replace y with x in implications y → n and n → y. If it creates a circuit in the graph of implications, remove the nodes from the circuit.

3. Replace y by x in linear equations containing y, simplify them and solve the linear system.

4. Free isolated node y.

Forgetting a reconstructible node

GBs can become dense. A forget operation that deletes a node and its links, which can be rebuilt if necessary, is a useful tool for controlling their size.

To forget a node n, we temporarily remove the implications i → n and n → s by replacing them with implications i → s, but without deleting n, which appears in linear equations. Then, we check if each valuation (i = 1) ∧ (n = 0) or (n = 1) ∧ (s = 0) is contradictory despite the absence of the implication i → n or n → s. If a single one is no longer contradictory, it means that we cannot reconstruct n and the hypercube induced by the GB is different. The node n may not be forgotten. Otherwise, n is reconstructible and the induced hypercube remains the same. We delete n and its implications are replaced by all the necessary implications between its direct implicants and implicates. [START_REF] Baader | The Description Logic Handbook: Theory, Implementation and Applications[END_REF] The reasoning on Graphs of Bipartitions

The Boolean completion of a GB

The cross and complement operations constitute a complete set of Boolean operators. The Boolean completion of a GB G with these operators is unique. It is a GB denoted by G n , which represents the hypercube Q n . Definition 8. The Boolean completion of a GB G is a GB noted G n , obtained from G by a finite sequence of applications of the operations cross and complement. G n is the fixed point, if it exists, of the cross and complement operations :

∀x, y nodes of G n , cross(x, y, G n ) = G n ∀x, y, z nodes of G n such that x → y ∧ y → z, complement(y, x, z, G n ) = G n
The cross and complement operations therefore do not change G n if the added nodes are recognized as already existing. This is always the case when the reasoning is based on a complete satisfiability test. Otherwise, the existence of the fixed point and its uniqueness must be proven on a case-by-case basis.

The GB G n is isomorphic to Q n , therefore to the powerset of the set of atomic dimensions of Q n . The set of atomic dimensions of Q n is called n. Each node x of G n represents a subset v x of n. The set v x is the characteristic vector of the node x: Definition 9. [characteristic vector] The characteristic vector of a node x of G n is the characteristic vector v x of the vertex of Q n represented by x. The characteristic vector of a node x of a GB G is the characteristic vector of x in G n .

G n verifies the uniqueness principle : For all x and y nodes of G n , (x = y) ⇐⇒ (v x = v y ). G n contains the nodes ⊥ and , which represent the vertices ⊥ and of Q n . It contains an implication x → y for each arc x → y of Q n and 2 n -(n + 1) linear equations modulo 2, which define 2 n -(n + 1) nodes of G n from to a basis of n + 1 nodes of G n . Some bases of n + 1 nodes linearly express the remaining 2 n -(n + 1) nodes. The basis shown in figure 8 is an example. The other possible bases are those that can be obtained by transforming the linear system with the operation of adding two equations. These are for example the n + 1 nodes of each of the n! paths from ⊥ to . In each of these bases, the other nodes are expressed with the single operation complement.

The 2 n -(n + 1) linear equations which define G n suffice to guarantee the fact that for any subset {x 1 . . . x k } of the nodes of G n whose sum ⊕ of the characteristic vectors cancels, the linear equation ( k i=1 x i ) = 0 is deducible from the linear system of G n . The number of variables of an equation is always even because all the equations of the linear system of G n and of a GB in general have an even number of nodes and this property is preserved on deducible equations. In the case where k is odd, the deducible equation contains the additional node ⊥, and v ⊥ = ∅. Proposition 2. For any subset {x 1 . . . x k } of nodes of G n such that ( k i=1 v i ) = ∅, with k even and where the v i are the characteristic vectors of the x i , the equation ( k i=1 x i ) = 0 is deducible from the linear system of G n . Proof. Each node x i is defined in G n by a linear equation x i = E i , where E i is a set of nodes each representing an atomic dimension of G n . The sum ⊕ of these k equations defining the x i is deducible from the linear system of G n . This is the equation Any GB G and its Boolean completion G n are equivalent, as Boolean expressions. This follows from the fact that the operations cross and complement only add Boolean functions of the nodes of G.

( k i=1 x i ) = ( k i=1 E i ). As ( k i=1 v i ) = ∅,

The deduction of linear equations

The cross and complement operations each add an equation to the linear system. These equations added to the implications are sufficient to construct all the Boolean expressions of a basis of nodes. However, the linear system thus obtained does not imply all the linear equations derivable from the entire GB, as illustrated in the figure 9.

Implications with equal dimensions

The equality dim(a, b) = dim(c, d) is rewritten (a ⊕ b) = (c ⊕ d). When we infer that two implications a → b and c → d of a GB have the same dimension, then the GB implies the equation (a ⊕ b ⊕ c ⊕ d = 0), which can be added to the linear system if it is not deducible from it.

( k i=1 (a i ⊕ b i )) ⊕ (c ⊕ d) = 0. Proposition 3. Let G be a GB. Let {(a 1 → b 1 ) . . . (a k → b k )} be implications of G, with mutually orthogonal atomic dimensions. Let c → d be an implication of G whose dimension is the set of dimensions of the a i → b i : dim(c, d) = ( k i=1 dim(a i , b i )). Then G =⇒ ((c ⊕ d) = ( k i=1 (a i ⊕ b i ))).

Proof. By simple application of the definition of dim.

This deduction of linear equations progressively increases the expressive power of the linear system and its capacity of inferring new Boolean constraints via Gaussian elimination, which is polynomially bounded, and efficient in practice.

Removing dimensions

New equations can also be deduced by using an equivalence relation which reduces the dimension of the GB.

If we remove atomic dimensions from a GB, we obtain a GB whose Boolean completion represents the hypercube of the remaining dimensions. The set E of deleted atomic dimensions defines an equivalence relation on the nodes of the GB. Two nodes x and y are equivalent if and only if (v x \ E) = (v y \ E). The nodes which are different only because of dimensions from E become equivalent under this relation.

For all E ⊆ n, we have

G n = G E G n\E .
The equivalence relation defined by the set E makes the nodes of each copy of G E in G n an equivalence class. If each class is reduced to its representative node, the copies of G n\E in G n reduce to G n\E (In figure 4, the copies of G E are the 8 blue squares, of dimension {1, 3}. The copies of G n\E are the 4 cubes of dimension {2, 4, 5}. Removing the dimensions {1, 3} gives the cube on the right). Each of the 2 |E| copies of G n\E in G n has as inf one of the 2 |E| nodes of G E . Each copy contains 2 |n\E| nodes and is isomorphic to G n\E (see figure 10).

Definition 10 (copy). Let E ⊆ n be a subset of the atomic dimensions of G n . The copy of G n\E associated with the node x of characteristic vector v x ⊆ E is the GB whose nodes represent the characteristic vectors of the form v x + F , for each F ⊆ (n \ E). The graph of implications of this copy is the subgraph of the graph of implications of G n induced by the nodes of the copy. The linear equations of the copy are the simplifications of the linear equations of G n by deleting the dimensions of E. The equations of G n and those that can be deduced from it, simplified by the removal of some arbitrary atomic dimensions, are deducible from the linear system of G n . Each atomic dimension of G n has an even number of occurrences in each equation (see Figure 8). Unlike G n , the equivalence classes of this relation on G are not Boolean completions. However, if each node x i of e is between a and b (a → x i and x i → b), then these nodes belong to the copy of G dim(a,b) in G n associated with v a . The characteristic vectors of the nodes of e all contain v a and are contained in v b . As the nodes of e are an even number, the v a disappear in the sum ⊕ and the equation deals with dimensions of G dim(a,b) , so it is deducible from G without the equivalence relation. If e is not deducible from the linear system of G, it can be added to it.

The GB of the dimensions of a GB

To each implication x → y of a GB, we associate a variable which represents the dimension v x ⊕ v y of the implication. The domain of this variable is the powerset of atomic dimensions of the induced hypercube. We then use a Boolean reasoning on the GB to calculate the relations of inclusion, disjunction and equality between these variables.

These variables are the nodes of a GB of dimensions, which is built separately. This GB is used to expand and accelerate the Boolean reasoning. The GB of dimensions is initialized to the implication ⊥ → between two new nodes ⊥ and . Each new dimension variable v is inserted between ⊥ and with the two implications ⊥ → v and v → . If v and w are two variables representing dimensions, the inclusion v ⊆ w is stored with an implication v → w. The disjunction v ⊥ w is stored with a bipartition v, w, v + w, ⊥ . The equality v = w causes the nodes v and w to be merged into a single node.

The nodes of the GB of dimensions which are implied only by the node ⊥, i.e. the minimal elements of the partial order of inclusion, are the atomic dimensions of the GB. These atomic dimensions are not those of the induced hypercube. They represent sets of atomic dimensions of the induced hypercube.

We calculate the relations of inclusion, disjunction and equality between the dimension variables with a Boolean reasoning based on proposition 1. It is assumed that the GB contains at least one implication of dimension d for each atomic dimension d. Definition 11. To calculate the dimension of an implication α → β of a GB G :

1. For each atomic dimension d of G, let x → y be an implication whose dimension is d.

If (x ∧ y) =⇒ (α ∧ β) then d ∈ dim(α, β). Else, if (x ∧ y) =⇒ (α = β) then d ⊥ dim(α, β).
2. Let E = {1 . . . n} be the set of atomic dimensions in dim(α, β) calculated in 1. We must look for the subsets of E whose dimensions are mutually orthogonal and which are equal to dim(α, β) : Let {(a 1 → b 1 ) . . . (a n → b n )} be a set of implications, of respective dimensions 1 . . . n. For each subset F = {1 . . . k} of E of mutually orthogonal dimensions such that (

k i=1 (a i = b i )) ⇐⇒ (α = β), the equation ( k i=1 (a i ⊕ b i ) ⊕ (α ⊕ β) = 0) is deducible from G (proposition 3
). If it is not deducible from the linear system alone by Gaussian elimination, it must be added to the system. For each of these F , the equation obtained makes that dim(α, β) = F . All these F are different expressions of the dimension of the implication α → β.

The step 2 looks for subsets F of E, of atomic implications of mutually orthogonal dimensions. This amounts to searching maximal cliques in the graph of the relation ⊥ on the set {1 . . . n}. Finding a maximum clique in a graph is an NP-complete problem. The following incomplete method is based on Gaussian elimination : Definition 12 (Calculation of linear equations). Let E = {1 . . . n} be a set of atomic dimensions belonging to the dimension of an implication α → β. Let {(a 1 → b 1 ) . . . (a n → b n )} be a set of implications, of respective dimensions 1 . . . n. To calculate the linear equations of the subsets F of E whose dimensions are mutually orthogonal,

If n = 1, F = E = {1}. We add the equation (a 1 ⊕ b 1 ⊕ α ⊕ β = 0).
Otherwise, 1. Temporarily construct an implication of dimension i for each i ∈ E, between α and β, for example by constructing two implications α → x and x → β and forcing the dimension of x → β to be i with an equation relating x → β to an implication of G of dimension i, as in figure 11 .

f ocus(α, β, G)

3. Valuate α, Valuate β and all nodes x between α and β, i.e. such that α → x and x → β.

4. Solve the linear system and simplify the equations, in the presence of the equivalences added by f ocus but without simplifying via Boolean values.

5. Add to the linear system S of G any fully valued equation.

6. Remove any valuation and undo the construct.

7. Solve the linear system.

The operation f ocus(α, β, G) transforms into an equivalence each implication of G whose dimension is orthogonal to dim(α, β): and beta one implication per atomic dimension of the set E. For example, we copy the implication a 1 → b 1 of dimension 1 by constructing the two implications alpha → 1 and 1 → beta and by forcing the dimension of 1 → beta to be equal to that of a 1 → b 1 with the equation (a 1 ⊕ b 1 ⊕ 1 ⊕ beta = 0). If there is a subset of {1, 3, 5, 7} which equals the dimension of alpha → beta and which is detectable by linear reasoning, Gaussian elimination will detect it under the form of a linear equation.

Definition 13 (f ocus)

. Let G = N, I, S be a GB. Let {α, β} ⊆ N such that α → β. f ocus(α, β, G) = (G ∧ (∀(x → y) ∈ I, if (dim(x, y) ⊥ dim(α, β)) then x = y))
It is a way to cancel some dimensions which are not present between two nodes α and β such that α → β (that are not dimensions of G dim(α,β) ), in order to focus the linear reasoning on this area and deduce possibly new equations, to add to the linear system. This is an application of the reasoning described in paragraph 5.2.2.

Characterizable GBs

A characterizable GB is a GB on which a uniqueness principle can be guaranteed : it is possible to associate a unique characteristic vector with each node. The atomic dimensions of a characterizable GB must be mutually orthogonal. If the GB has n atomic dimensions, it induces Q n . Each characteristic vector is then a subset of the atomic dimensions of Q n .

Figure 12 shows three simple examples of characterizable GBs. The characterize operation (definition 14) associates vectors to the nodes of a GB. It is a nondeterministic operation. It can associate several different vectors to the same node. It associates a unique characteristic vector to each node only when the GB is characterizable. Definition 14 (characterize). Characterizing the nodes of a GB G defines as :

1. Pick a node n from G and set v n = ∅.

2. As long as there are modifications, (a) While it is possible, choose a node x such that v x is calculated and for any implication (x → y) or (y → x) of G such that dim(x, y) is a subset of the atomic dimensions of G, set v y = (v x ⊕ dim(x, y)).

(b) Solve the linear system using the characterized nodes as a basis. For each linear equation e : (x = ( k i=1 y i )) where only x is not characterized, set v x = ( k i=1 v yi ). 3. In order for the characteristic vectors to reflect the orientation of the GB, i.e. the set inclusion of the characteristic vectors, it is necessary to ensure that for any pair of nodes {x, y} such that there is a path from x to y, we have v x ⊂ v y and therefore dim(x, y) = (v y ⊕ v x ) = (v y \ v x ). For each implication (x → y), add the offset v x \ v y to a set E initially empty. Then replace v n by (v n ⊕ E), for each node n.

The step 2a propagates characteristic vectors wherever possible via implications whose dimensions are subsets of atomic dimensions. The step 2b is necessary because the graph of the implications alone of a characterizable GB can be unconnected (Figure 13).

The reasoning on characterizable GBs

A characterizable GB is a theoretical object. It needs a complete reasoning to detect all the characterizable GBs contained in a GB, for example based on a complete satisfiability test, exponential in the worst case. Moreover, any GB can contain an exponential number of interleaved characterizable GBs. It is therefore not possible to enumerate all those which can be detected and to construct the characteristic vectors of their nodes. What is possible is to define a polynomial reasoning on arbitrary GBs, which behaves as if the characteristic vectors were available locally to each characterizable GB satisfying certain properties. The Gaussian propagation, presented in the paragraph 6.3, is a complete reasoning locally to each characterizable GB, if this characterizable GB verifies the following 5 properties. In the rest of the paper, the term "characterizable GB" designates a GB whose graph of implications is connected and which has these 5 properties:

1. its atomic dimensions are mutually orthogonal, as calculated and stored in the GB of dimensions of G defined in paragraph 5.3.

2. its non-atomic dimensions, calculated by the definition 11, are sets of these atomic dimensions 3. G contains at least one implication of dimension d for each atomic dimension d of G

4. for each set of implications of G {a 1 → b 1 , . . . , a k → b k } such that ( k i=1 dim(a i , b i )) = ∅, the linear equation ( k i=1 (a i ⊕ b i )) =
0 is deducible from the linear system alone. 5. all chains of implications between two nodes have the same dimension.

A characterizable GB G of atomic dimensions D = {1, . . . , n} is completed in Q n by adding and classifying the missing vertices. To add the node s of characteristic vector v s ⊆ D, we check if it already exists. Otherwise, it is created and classified in such a way as to maintain the Hasse diagram structure of the inclusion relation on the nodes. This node s is a linear function of nodes already present in G since its characteristic vector is a set of atomic dimensions of G and there is at least one implication of each atomic dimension. If s is connected to a node t of G by an implication s → t or t → s by the operation classif y (Definition 6), its dimension v s ⊕ v t is always a set of atomic dimensions of G. This dimension is calculated by the operation which dimensions an implication (definition 11). By default, it retains the property 5. If this property is violated by a new construction, the propositions 4 and 5 indicate a method to restore it locally to all characterizable GBs.

Locally to a characterizable GB, Boolean reasoning is greatly simplified. Boolean operations are reduced to set operations on finite sets of atomic dimensions and they preserve the property of being characterizable.

Chains and dimensions

In a hypercube, the chains of implications between two vertices all have the same dimension. In a GB, on the other hand, the dimensions of the chains of implications between two nodes are possibly expressed differently.

To preserve the property 5 of a characterizable GB, a restorative equation (proposition 4) may be deduced, which removes the dimensions that differentiate two chains between two nodes (proposition 5). This restorative equation contains the nodes of a set of implications. If the dimensions of these implications are mutually orthogonal, the implications become equivalences.

Proposition 4 (restorative equation). Any linear equation

( n i=1 (a i ⊕ b i )) = 0 such that (∀i ∈ {1 . . . n}, a i → b i ) and (∀{i, j} ⊆ {1 . . . n}, (dim(a i , b i ) ⊥ dim(a j , b j ))) implies (∀i ∈ {1 . . . n}, a i = b i ).
Proof. The hypotheses :

h1 = (( n i=1 (a i ⊕ b i )) = 0), h2 = (∀i ∈ {1 . . . n}, a i → b i ), h3 = (∀{i, j} ⊆ {1 . . . n}, (dim(a i , b i ) ⊥ dim(a j , b j ))) Suppose a 1 = b 1 . ((a 1 → b 1 ) ∧ (a 1 = b 1 )) =⇒ (a 1 ∧ b 1 ).
By the equivalence (2) of the proposition 1, we have (∀i ∈ {2 . . . n}, a i = b i ).

By simplifying in the equation h1, we obtain a 1 = b 1 . Contradiction.

If n = 1, we have the equations x = 0 or x = 1, which value the node x. If n = 2, we have the equations x ⊕ y = 0 or x ⊕ y = 1, ie x = y or x = y. If x → y, the equation x = y automatically transforms into the valuation (x = 0) ∧ (y = 1).

The conjunction G ∧ val expresses the application of the valuation val on the GB G.

The valuation of a GB reduces the dimension of the hypercube it induces. For example, a linear equation x = y removes from the induced hypercube the dimensions included in dim(x, y). The valuation of a GB is a temporary modification that must possibly be undone.

Basic propagation

A valuation of a GB may imply linear equations that are not deducible from the GB itself. This is the role of propagation. We note α β the fact that β is deduced from α by propagation. The simplest propagation exploits implications and linear equations: Definition 16 (propagation). The propagation of a valuation on a GB consists of applying the following rules wherever possible, until there are no more modifications: where e is an expression ( n i=1 x i ) and the x i are valued variables. Rules 1 and 2 propagate along implication paths. Rule 3 is triggered when a linear equation has a single unvalued variable. This propagation is analogous to the propagation called BCP on the clausal representation of Boolean knowledge [START_REF] Apt | Some remarks on boolean constraint propagation[END_REF]. It therefore has a linear complexity.

The basic propagation adds to this simple propagation the exploitation of the information compiled in the GB of the dimensions of a GB G, in accordance with proposition 1.

Gaussian propagation

Let G be a GB. When a valuation val is propagated over G, its linear system S can have partially or totally valued equations. This partially valued linear system can be solved by Gaussian elimination. Gaussian elimination is complete, locally to S, for the detection of the equations 0 = 0 (tautology), 0 = 1 (contradiction), x = 0, x = 1, x = y, x = y. Also, it suffices to value a set of nodes to infer by Gaussian elimination any equation implied by S whose all nodes belong to the set (it simplifies to 0 = 0) or except one node (it simplifies to x = constant) or two (x = y or x = y). Its complexity is in O(n 2 m), for n equations and m variables.

Gaussian propagation is a loop that alternates basic propagation and Gaussian elimination until there are no more changes. Since there are a maximum of m nodes to value, its complexity is in O(n 2 m 2 ).

Local completeness of Gaussian propagation

For each implication a → b of atomic dimension of a GB G, the Gaussian propagation of the valuation (a = 0 ∧ b = 1) values all the nodes of the characterizable GBs in G which contain a and b. It is the local completeness of the Gaussian propagation. This completeness avoids having to enumerate and construct the characteristic vectors of these interleaved GBs, which are potentially exponential in number, in order to have a complete Boolean reasoning locally to each characterizable GB. The implication graph of G then contains only implications x → y where x and y are valued or where x = y. As this graph is connected, all the nodes are valued by the basic propagation.

The probing propagation

Locally to a characterizable GB, the Gaussian propagation of the valuation of an implication of atomic dimension is complete. It is possible, at a higher cost, to make the propagation of any valuation complete, locally to these characterizable GBs. It suffices, once any valuation has been propagated, to test all the implications a → b not entirely valuated and of atomic dimension. We propagate a = b, that is to say (a = 0 ∧ b = 1), by Gaussian propagation, which is complete. If it is contradictory, we add a = b to the valuation, otherwise, a = b remains possible. This probing propagation is complete locally to the characterizable GBs which contain the nodes of the propagated valuation.

Proposition 7. In a characterizable GB, the probing propagation of any valuation is complete.

Proof. Let G be a characterizable GB and V al a valuation of G. Let x be a node of G such that (G ∧ V al) =⇒ (x = v), where v ∈ {0, 1}, but not deduced by the Gaussian propagation of V al. Let y be a node of G such that (y = v) ∈ V al. There is at least one because only a valuation containing a valued node v can imply x = v. In G, x and y are two different nodes. In G∧V al, x = y is deducible, but not by Gaussian propagation.

In the connected graph of implications of G, there is a chain of implications between x and y, some of which are equivalences in G ∧ V al. The probing propagation infers all these equivalences because the Gaussian propagation is complete on G (proposition 6). The sum ⊕ of the dimensions of the remaining implications is empty because x = y is deducible from G ∧ V al. By simplifying the equation e with these equivalences, we obtain the equation a 1 = b k , ie x = y. This equation is therefore derivable from the simplified linear system of G ∧ V al. Gaussian elimination is complete to deduce these equations. See figure 14 for an illustration.

Figure 14: This GB is characterizable. If it is contained in a larger GB, the probing propagation is complete locally to it. The calculation of the dimensions infers that its atomic dimensions {1, 2, 3, 5} are mutually orthogonal and that the dimension 4 is equal to {2, 3}. Note that the chains between x and y all have the same dimension {3, 5}. The valuation (y = 1) ∧ (z = 0) (green for 1 and red for 0) implies x = 1. The Gaussian propagation of this valuation does not deduce it. To deduce it, it suffices to test each atomic dimension by Gaussian propagation of an implication of this dimension. The implications of dimensions 3 or 5 become equivalences (in blue). There is an even number of the remaining dimensions in the two chains between x and y and therefore, their ⊕ sum is empty. The linear system, simplified by the equivalences, deduces x = 1 by Gaussian elimination. Note: it also derives the linear equation a ⊕ b = 1 (in purple), i.e. a = b, which differentiates the two equivalence classes in blue.

The probing propagation performs as many tests each triggering a Gaussian propagation as there are not entirely valuated implications. Its complexity is therefore in O(n 2 m 2 p), where p is the number of implications of the GB.

The complete classification

The characteristic vector v x of a node x of a GB is the characteristic vector of the corresponding vertex of the hypercube induced by the GB. It is a theoretical object, which is not available for the probing propagation but which allows to define a complete classification: Definition 17 (complete classification). A GB is completely classified if and only if for any pair of nodes {x, y},

((v x = v y ) ⇐⇒ (x = y)) ∧ ((v x ⊂ v y ) ⇐⇒ (x → y))
If for the Boolean reasoning used in all construction operations of a GB, a complete satisfiability test is used, every GB is completely classified. If we use the probing propagation, we can only guarantee the complete classification locally to the characterizable GBs contained in a GB : Proposition 8. In a GB constructed using probing propagation, all characterizable GBs are completely classified.

Proof. By the proposition 7, the probing propagation is complete locally to each characterizable GB contained in a GB. Let x and y be two nodes of a characterizable GB contained in a GB G. If (v x ⊆ v y ) in the hypercube induced by the characterizable GB, whatever the order of construction of x and y, the classif y operation (definition 6) infers the implication x → y. If moreover (v x = v y ), the probing propagation of {x = 0, y = 1} by the operation which adds the implication x → y to G (definition 7) detects a contradiction, which produces the merging of the two nodes.

The complete propagation

The propagation can be based on the complete Boolean satisfiability test, performed by a SAT-solver. It is then complete.

To extend a partial valuation to all the nodes whose value it implies, we proceed as follows : for each node n not valued, we apply the complete satisfiability test on the conjunction of the graph, of the partial valuation and of n = 1 or n = 0, translated into conjunctive normal form. If the test detects a contradiction, the value of n is reversed. We take advantage of the graph of implications to limit these costly tests. If x → y and if x = 1 has been tested non-contradictory, it is useless to test y = 1, and dually for y = 0 and x = 0.

The complete propagation actually uses the SAT-solver Glucose [START_REF] Simon | The glucose sat-solver[END_REF], an extension of MiniSat [START_REF] Eén | An extensible sat-solver[END_REF]. In practice, the computation times of this complete propagation increase exponentially with the size of the graph.

Achievements and Prospects

The tools and reasoning described here are programmed in C++ and Objective-C under MAC OS. All the diagrams in this document were made with the interactive editor of GBs.

The GBs are a construction site that allows to study all kinds of combinations capable of providing a usable solution to manage Boolean knowledge. This project will still require a lot of experimentation to improve this management, optimize calculation times and increase the deductive power of polynomial reasonings.

The construction of the GB of the dimensions of a GB or the probing propagation, for example, are polynomially bounded but in practice, they are expensive. One solution is to restrict to the equalities between dimension variables and the graph of the relation ⊥. Only the equations (a ⊕ b ⊕ c ⊕ d = 0) are added whenever it is inferred that two implications a → b and c → d have the same dimension. This solution uses Gaussian propagation, which itself uses basic propagation, which is less expensive than probing propagation.

The complete satisfiability test is too powerful for knowledge management tasks oriented towards modeling basic understandings. Used carelessly, it quickly becomes too costly. The computation time of a single test depends more on the type of circuit than on its size (some logic circuits are known to be difficult for the SAT test, like CNF formulations of the Pigeonhole principle, for example), but the computation times of the complete propagation, on the other hand, are systematically too high when the GBs reach a certain size, even if they are free of difficult sub-circuits. It is always possible to obtain more efficient and polynomially bounded solutions, from Gaussian propagation and reasoning about dimensions.

Boolean knowledge management should restrict to incomplete operations that are more efficient than complete reasoning based on a complete satisfiability test. This management has neither the capacity nor the vocation to solve the decision problems dealt with by SAT-solving. To solve a decision problem beyond the scope of management operations, specified in a partially valued GB, the GB is translated with its valuation into conjunctive normal form and a SAT-solver is used (actually the Glucose solver [START_REF] Simon | The glucose sat-solver[END_REF]). The complete satisfiability test remains an essential tool, to be triggered sparingly. We can for example trigger a single complete satisfiability test each time a node x ∨ y is created by the operation cross, if a unique sup n of x and y is present, to check if n = x ∨ y, and dually for x ∧ y.

Out of this construction site emerged the natural language interaction program presented in [START_REF] Goossens | Modélisation d'une forme simple de compréhension[END_REF]. This program models a simple understanding capacity in the micro-world of elementary school level quadrilateral geometry. The geometric knowledge is entirely expressed in Boolean logic. The challenge behind this demonstration, partially accomplished, was to manage all the sentences expressible with the words of a mini-dictionary, as a human would. The cases of failure concern phenomena that are outside the scope of the intended understanding, such as credulity, revision of beliefs, metaphors, second degree, etc., and also the limits of the expressive capacities of Boolean logic.

Acknowledgements

I thank Vincent Lesbros for his proofreading and corrections.

Conclusion

This document has presented and formalized Graphs of bipartitions, to manage Boolean knowledge, with the general objective to model understanding abilities based on symbolic reasoning.

This management is made of incomplete but efficient polynomial Boolean reasonings. These reasonings ensure a function of storage or inter-classification of Boolean knowledge, as close as possible to the induced Boolean hypercube. While knowledge is stored in the graph, they grow substructures where Boolean reasoning is complete and efficient. These intertwined substructures are potentially exponential in number. The reasoning is reduced, locally to each of these substructures, to set operations on finite sets of dimensions of the induced hypercube.

These substructures grow by deducing linear equations modulo 2 from reasoning on the dimensions. The resulting linear system is particularly useful because the associated polynomial reasoning, Gaussian elimination, is complete and efficient.

These advances in automatic Boolean knowledge management will benefit the modeling of simple forms of understanding, in natural language interaction on micro-universes described with Boolean knowledge, as illustrated in [START_REF] Goossens | Modélisation d'une forme simple de compréhension[END_REF]. These forms of understanding are based on symbolic reasoning, thus precise and rigorous. It is expected that they will resist approaches solely based on Large Language Models. LLMs bring noticeable progress in understanding natural language. Where purely symbolic approaches are rigid, too rigorous and difficult to apply on large volumes of knowledge, LLMs deal with approximate syntax and adequately model flexible interactions. However, they may fail even on intuitive knowledge focussing on structured topics. They will need to be combined with symbolic approaches and will come up against the same problems.

The language of Boolean expressions is very poor. It remains to understand how to lift the polynomial reasonings presented here, to higher orders. These reasonings are not based on an enumeration of models, in finite number at order 0 but infinite otherwise, contrary to the complete Boolean satisfiability test. This transition to higher orders is still a speculative but possible objective.

Figure 1 :

 1 Figure 1: The Boolean hypercube Q 3 . Each vertex displays its characteristic vector. Each arc displays its atomic dimension. The chains between any two vertices where each atomic dimension appears only once, are the permutations of the sequence of dimensions of their arcs.

Definition 1 .

 1 The Boolean hypercube. 1. Q {1} is the one-dimensional Boolean hypercube named 1. It has 2 1 = 2 vertices ⊥ and and an arc ⊥ → . v ⊥ = ∅ and v = {1}. 2. If Q n and Q m are two Boolean hypercubes, with n = ∅ and m = ∅, the Cartesian product of Q n and Q m is the Boolean hypercube Q n+m . Each vertex s of Q n has 2 |m| copies in Q n+m . Each of these copies has as characteristic vector the union of v s with one of the 2 |m| subsets of the set of atomic dimensions of Q m . Each edge of Q n+m connects two vertices x and y such that v x ⊕ v y is a singleton. The arc is x → y if v x ⊂ v y and y → x otherwise.

Figure 2 :

 2 Figure 2: The Boolean hypercube Q 5 is the Cartesian product of Q 3 and Q 2 . It contains 2 2 = 4 copies (in blue) of the cube Q 3 . These cubes are connected by 2 3 = 8 copies of the square Q 2 . Each square contains one vertex of each of the 4 cubes. The 4 vertices of a square are positioned identically in each of the cubes.

Figure 3 :

 3 Figure 3: The vertices a and b of the square Q 2 on the left express the other two (c = a ∨ b and d = a ∧ b). The vertices d, a and c of the middle square Q 2 express the local complement b = ((c ∧ a) ∨ d) of a between d and c. The vertices a, b and c of the cube Q 3 (on the right) express the other vertices, including (a ∨ b ∨ c), under the constraint (a ∨ b) = (a ∨ c) = (b ∨ c) = (a ∨ b ∨ c).

Figure 4 :

 4 Figure 4: The Boolean hypercube Q 5 (on the left) contains 8 copies (in blue) of the square induced by the vertices a and b. Each square is an equivalence class of the relation defined by a = b. The cube (on the right) is the quotient of Q 5 by this equivalence relation. The dimensions 1 and 3 have been removed from Q 5 , to obtain the cube of the remaining dimensions 2, 4 and 5.

Proposition 1 . 2 )Figure 5 :

 125 Figure 5: The dimension of the pair {a, b} is {1, 3}. The valuation (a = 0) ∧ (b = 1) "cancels" the dimensions 2, 4 and 5 everywhere in Q 5 and therefore transforms into equivalences all the arcs having these dimensions. Q 5 is the Cartesian product of Q {2,4,5} and Q {1,3} . Each copy of Q {2,4,5} in Q 5 has all its vertices equivalent. Vertices valued 1 are in green and vertices valued 0 in red.

  the constraint is also written as the modulo 2 linear equation (a ⊕ b) = (c ⊕ d), or (a ⊕ b ⊕ c ⊕ d) = 0. We express for example s = a ∨ b and i = a ∧ b from four implication paths, from a to s, from b to s, from i to a and from i to b, and with the equation (a ⊕ s) = (i ⊕ b). The complement d of b between a and c, assuming a → b and b → c, is expressed as d = (a ⊕ b ⊕ c). The graph of implications between nodes and the modulo 2 linear equations allow to construct all the Boolean expressions of a basis of nodes. The basic building block of a GB is the bipartition: Definition 2. A bipartition is a quadruple a, b, c, d , where a, b, c, d are Boolean variables verifying (a → c) ∧ (b → c) ∧ (d → a) ∧ (d → b) and a ⊕ b ⊕ c ⊕ d = 0. The constraints of the bipartition on its four variables a, b, c, d make that c = a ∨ b and d = a ∧ b. From two variables a and b, a bipartition thus expresses both a ∨ b and a ∧ b. Also, the variable b is the local complement of a between c and d. See figure 6.

Figure 6 :

 6 Figure 6: Unlike hypercubes (figure 3), the implications between the nodes of a GB are not enough to represent Boolean expressions. Linear equations are needed. The equation a ⊕ b ⊕ c ⊕ d = 0 in the two squares on the left is represented by the link consisting of a circle connected to the four variables of the equation. The dotted connection designates the defined variable of the equation in the solved system. These two squares on the left represent the bipartition a, b, c, d . The cube on the right contains 4 equations, which define linearly the nodes a, b, c and a ∨ b according to the basis of the nodes a.b, a.c, b.c and (a.b).c. The basis {a, b, c} is insufficient to define the other nodes linearly but sufficient to define them as Boolean expressions.

  Adding an implication to a GB G must preserve the Hasse diagram structure of the implication graph. This operation recognizes existing nodes and removes redundant implications : Definition 7. add the implication (a → b) to a GB G = If a ∧ b is contradictory, definitely impose the constraint a = b on G. Otherwise, if there is no path from a to b, add a → b to the set of implications of G and remove redundant implications to maintain the Hasse diagram.

  the nodes representing the atomic dimensions have an even number of occurrences in the E i . So ( k i=1 E i ) = 0 and the deducible equation becomes ( k i=1 x i ) = 0.

Figure 8 :

 8 Figure 8: The GB G 4 represents Q 4 . The basis {1, 2, 3, 4, ∅} is in red. The node ∅ is the inf of G 4 and its sup is the node 1234. The 2 4 -(4 + 1) = 11 nodes outside the basis are defined by the 11 linear equations. The node 12 is defined by the equation 12 = 1 ⊕ 2 ⊕ ∅. The node 124 is defined by the equation 124 = 1 ⊕ 2 ⊕ 4. All equations have a number of variables which is even and greater than or equal to 4.

Figure 9 :

 9 Figure 9: The reasoning on dimensions deduces a new linear equation. The operation cross(b, M ) on the left GB produces the middle GB, which has 3 linear equations. We then have ((a ∨ M ) ∧ (b ∨ M )) = M and ((a ∧ M ) ∨ (b ∧ M )) = M but this is not deductible linearly. Calculating the dimensions deduces an additional linear equation and produces the right GB, where the reasoning based on Boolean value propagation and Gaussian elimination is complete.

Figure 10 :

 10 Figure 10: The GB G {1,2,3,4} , or G 4 , is the Cartesian product of G {1,2} and G {3,4} . Each implication displays its dimension. Each node displays its characteristic vector, in red. The 4 copies of G {1,2} (in blue) are the equivalence classes of the relation defined by the dimension set {1, 2}. The 4 copies of G {3,4} , of dimensions 3 and 4, are associated with each of the 4 subsets of {1, 2}. The copy of G {3,4} in bold is associated with the singleton 2.

  If we remove the atomic dimensions of a set E, we remove an even number of each dimension from each equation and the remaining dimensions are always an even number in each equation. Each simplified equation is therefore deducible from G n , by the proposition 2. Each implication a → b of a GB G defines an equivalence relation on the nodes of G. This relation removes the dimensions out of dim(a, b), i.e. the set of atomic dimensions of n \ dim(a, b), where n is the set of dimensions of G n . Let e : ( k i=1 x i ) = 0 be a linear equation deducible from G and simplified by this equivalence relation. Each x i belongs to a different equivalence class.

Figure 11 :

 11 Figure 11: To calculate the dimension of the implication alpha → beta in the case n > 1, it suffices to copy between alpha

Figure 12 :

 12 Figure 12: Three characterizable GBs, whose dimensions are mutually orthogonal. The GB on the left is interpreted as a graph which stores the subsets of the set {a, b, c}. This set is a basis of atoms : (a ∧ b) = (a ∧ c) = (b ∧ c) = ∅. The middle graph is the dual construction, with the co-atom basis {a, b, c} : (a ∨ b) = (a ∨ c) = (b ∨ c) =1. The graph on the right is a mixed construction, without a basis of atoms or co-atoms but whose dimensions are mutually orthogonal.

Figure 13 :

 13 Figure 13: This GB is not characterizable. Dimensions 4 and 6 are orthogonal because they are on a common path but 4 and 3 are not orthogonal. The sub-GB containing the nodes {a, b, c, h, g, e} and their implications is characterizable. It contains the basis of mutually orthogonal dimensions {2, 4, 5, 6}, which makes it possible to characterize the nodes {a, b, c, h, g} and the node e is expressed linearly in this basis: e = a ⊕ c ⊕ g.

  1. (x → y ∧ x = 1) (y = 1) 2. (x → y ∧ y = 0) (x = 0) 3. ((x = e) and e evaluates to the constant c) (x = c)

  For any implication a → b of G, if a and b have the same Boolean value, then if a = b, any implication c → d of G such that dim(c, d) ⊆ dim(a, b) adds c = d to the current valuation. If a = 0 ∧ b = 1, for any implication c → d of G, if dim(c, d) ⊥ dim(a, b), we also add c = d and if dim(a, b) ⊆ dim(c, d), we add c = 0 ∧ d = 1 to the current valuation.

Proposition 6 (

 6 local completeness). In a characterizable GB, the Gaussian propagation of the valuation (a = 0 ∧ b = 1) of any implication a → b of atomic dimension values all the nodes of the GB. Proof. Let a → b be an implication of atomic dimension of a characterizable GB G, valued with (a = 0 ∧ b = 1). For any implication c → d of G : If dim(c, d) = dim(a, b), the equation (a ⊕ b ⊕ c ⊕ d = 0) is deducible from the linear system of G by the property 4 of a characterizable GB. The valuation (a = 0∧b = 1) simplifies this equation to c⊕d = 1, an equation for which the Gaussian elimination is complete. It is automatically transformed into the valuation (c = 0 ∧ d = 1) because c → d. If c → d has a different dimension: If it is an atomic dimension, dim(c, d) ⊥ dim(a, b) is noted in the GB of the dimensions G and the basic propagation deduces c = d. If it is a non-atomic dimension E = {d 1 . . . d k }, where the d i are mutually orthogonal atomic dimensions of G : By the property 3 of a characterizable GB, G contains a set {x 1 → y 1 . . . x k → y k } of implications of respective dimensions {d 1 . . . d k }. By the property 4, the equation e : ( k i=1 (x i ⊕ y i )) = (c ⊕ d) is deducible from the linear system of G, even if the Gaussian elimination is not complete to deduce it in all cases. If dim(a, b) ∈ E, one of the implications x i → y i has the same dimension as a → b. This implication verifies (x i ⊕ y i ) = (a ⊕ b). For the other x j → y j , the basic propagation deduces x j = y j . With these equalities, the equation e simplifies to (a ⊕ b) = (c ⊕ d). The valuation (a = 0 ∧ b = 1) simplifies it to (c ⊕ d) = 1. Gaussian elimination is complete to deduce these equations. It simplifies to (c = 0 ∧ d = 1). Otherwise, dim(a, b) ⊥ E. From the valuation (a = 0 ∧ b = 1) and from the GB of the dimensions of G, the basic propagation deduces ( k i=1 (x i = y i )). The equation ( k i=1 (x i ⊕ y i )) = (c ⊕ d) simplifies to c ⊕ d = 0, i.e. c = d, for which Gaussian elimination is complete.

  Let e : (( k i=1 (a i ⊕ b i )) = 0) be the equation where the a i → b i are the implications of the chain which are not equivalences in G ∧ V al. By the property 4 of a characterizable GB, e is derivable from the linear system of G because the sum ⊕ of its dimensions is empty. By ordering these implications a i → b i as they appear in the chain from x to y, we have in G ∧ V al the following equivalences: x = a 1 , b k = y and (∀i ∈ {1, . . . , k -1}, b i = a i+1 ).

The same reasoning from any (a i ∧ b i ) leads to the same contradiction. So (h1 ∧ h2 ∧ h3) =⇒ (∀i ∈ {1 . . . n}, a i = b i ) Proposition 5. In a characterizable GB, all the chains of implications between two nodes have the same dimension.

Proof. Let G be a characterizable GB. Let α and β be two nodes of G. Suppose that there are two implication chains in G between α and β, of dimensions E and F respectively. In other words, the dimension between α and β is calculated in two different ways. Let us show that E = F . Let {P, Q, R} be a tripartition of E ∪ F , with

The atomic dimensions in P , Q and R are all different and mutually orthogonal (property 1 of a characterizable GB). The dimensions of P are the only common dimensions of E and F . We have E = P + Q and F = P + R. By the property 3 of a characterizable GB, G contains at least one implication of dimension d for each atomic dimension

By the property 4 of a characterizable GB,

The sum of these two equations is : ((

Gaussian elimination is not complete for deducing a restorative equation, as described in proposition 4, when it is deducible from the linear system. As the proof of this proposition indicates, to check whether a characterizable GB satisfies the property 5, one must check for each of its implications a → b if the expression (a ∧ b) is contradictory, i.e. whether a = b is valid.

The propagation of valuations

The reasoning on the dimensions, which is used to deduce new equations and to classify the nodes created by the operations cross and complement, is based on Boolean reasoning. These reasonings are complete if we use a complete Boolean satisfiability test. To avoid the risks of combinatorial explosions, undesirable for knowledge base management operations, one can develop incomplete and polynomially bounded methods, which propagate constraints from valuations.

The Gaussian elimination is complete locally to what is expressed linearly from any basis of nodes of a GB. It is a linear reasoning that spontaneously detects linear equations that remove contradictory nodes and merge equivalent nodes.

To go further, we can trigger the propagation of a partial valuation of the GB. A valuation removes certain dimensions from the induced hypercube and allows deductions beyond the reach of linear reasoning.

Valuations

A valuation is a system of linear equations on the nodes of a GB: Definition 15. A valuation of a GB G is a set (or a Boolean conjunction) of linear equations modulo 2 of the form (( n i=1 x i ) = constant) with constant ∈ {0, 1}. The x i are nodes of G.