JP7048032B2 - Data generator, data generation method, and program - Google Patents

Description

The present invention relates to a knowledge composition that expresses a logical function in a compact and easy-to-use form.

Knowledge compilation is a field related to methods for expressing logical functions in a compact and easy-to-use form. Here, "easy to handle" means that a query related to a logical function (hereinafter referred to as a query) and a logical operation with another logical function can be performed at high speed under the expression form.

Such expressions have long been used in the logical design and verification of integrated circuits, and are also used in mathematical optimization such as probability inference by Bayesian networks and maximization of reliability of communication networks. Many such phenotypes have been proposed, but among them, the Sentential Decision Diagram (hereinafter referred to as SDD) of Non-Patent Document 1 has both compactness and ease of handling, and has a wide range of application fields in recent years. It is actually used in.

Adnan Darwiche. SDD: a new canonical representation of propositional knowledge bases. In Proceedings of the Twenty-Fifth AAAI Conference on Artificial Intelligence, pp. 819-826, 2011. Randal E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, Vol. C-35, pp. 677-691, 1986.

The expression form of a logical function that can be considered in knowledge compilation is that once a logical function is expressed, the operation of solving a query related to that logical function or combining it with another logical function is the expression form. You can do it as it is. However, it is generally unknown how large a logical function will be when expressed in its phenotype.

In fact, depending on the logical function, there is an example in which the size of the expression becomes very large and cannot be stored in the memory of the computer. Moreover, even if it is stored in the memory, it may take a long time to perform a combination operation with various queries and logical functions due to the large size of the expression. Therefore, a technique for creating a phenotype that is as small as possible and that makes the operation of solving a query or combining with other logical functions faster is being studied.

The SDD of Non-Patent Document 1 generalizes the structure of the binary decision diagram (hereinafter referred to as BDD) of Non-Patent Document 2 and has the same functionality as BDD (combination with queries and other logical functions). It is a data structure that realizes a smaller size than BDD while providing (corresponding to). However, there are many logical functions whose size is still large even with SDD. Therefore, there is a need for a phenotype that has the same functionality as SDD but realizes a smaller expression than SDD.

The present invention has been made in view of the above points, and an object of the present invention is to provide a technique for obtaining a phenotype that realizes a smaller expression than SDD in a method for expressing a logical function in a compact and easy-to-use form. do.

According to the disclosed technique, it is a data generator that generates graph structure data expressing the decomposition of a logical function according to a predetermined tree structure.
Based on the order tree that specifies the variable order when decomposing the logical function, when a plurality of substructures representing the same decomposition are specified in the decomposition of the logical function, the plurality of substructures are specified. As a representative substructure, one substructure selected from the above is used as a representative substructure.
The graph structure data corresponding to the logical function is shared so that the remaining data in the graph structure corresponding to the parent node of the same partial structure shares the graph structure data corresponding to the representative partial structure by the pointer. A data generation device including a building unit for generating is provided.

According to the disclosed technique, there is provided a technique for obtaining a phenotype that realizes a smaller expression than SDD in a method for expressing a logical function in a compact and easy-to-use form.

It is a figure for demonstrating SDD. It is a block diagram of the data structure conversion apparatus 100 in 1st Embodiment. It is a figure which shows the example of the hardware composition of a device. This is the overall processing flow of the preprocessing unit M02. It is a figure which shows the example of the operation in 1st Embodiment. It is a figure which shows the example of the algorithm in step S023. It is a figure which shows the example of the algorithm corresponding to the operation of the conversion unit M03. It is a figure which shows the example of the syntax tree. It is a block diagram of the data structure conversion apparatus 100 in 2nd Embodiment. It is a figure which shows the example of the algorithm corresponding to the operation of the construction part M13. It is a figure which shows the example of the algorithm corresponding to the operation of the construction part M13. It is a figure which shows the example of the algorithm corresponding to the operation of the construction part M13. It is a figure which shows the example of the algorithm corresponding to the operation of the construction part M13. It is a figure which shows the example of the algorithm corresponding to the operation of the construction part M13. It is a figure which shows the example of the model count algorithm.

Hereinafter, embodiments of the present invention (the present embodiments) will be described with reference to the drawings. The embodiments described below are merely examples, and the embodiments to which the present invention is applied are not limited to the following embodiments.

(About SDD)
Since the present embodiment provides a structure in which the structure of the SDD is improved, the SDD will be described first.

First, a logical function is a function that takes a variable that takes a binary value of true (true) or false (false) as a plurality of arguments and returns either a true or false value. Assuming that the variables taken by the logical function f as arguments are X and their divisions are Y and Z, f consists of only the variables of the partial logical functions p ₁ , ..., P _n and Z consisting only of the variables of Y. It can be decomposed as follows using the partial logic functions s ₁ , ..., s _n .

f (X) = [p ₁ (Y) ∧ s ₁ (Z)] ∨ ・ ・ ・ ∨ [ _pn (Y) ∧ s _n (Z)]
Here, A∧B is a logical product (A and B), and A∨B is a logical sum (A or B). Especially here, the truth of the variables i ≠ j and Y such that p ₁ , ..., _pn are relatively prime, that is, p _i (Y) and p _j (Y) are true at the same time. Let us consider a decomposition in which no allocation exists. It should be noted that such decomposition is always possible.

SDD has realized a compact and easy-to-use phenotype by recursively performing such decomposition. At this time, it is a tree structure called vtree that determines how the variables are divided. In vtree, each of the lowest nodes (hereinafter referred to as leaves) corresponds to one variable, and each of the other nodes (hereinafter referred to as internal nodes) is connected by an edge to the lower node (hereinafter referred to as "leaf"). , Called a child node) is a tree structure that has exactly two. Each internal node represents dividing the variable into a variable corresponding to the leaves below the left child node and a variable corresponding to the leaves below the right child node. The vtree node may be referred to as a "node".

An example of vtree is shown in FIG. 1 (a). This vtree first divides the four variables {A, B, C, D} into the left {A, B} and the right {C, D}, then the left {A, B} further {B}. And {A}, and {C, D} on the right side is further divided into {D} and {C}. Each node of vtree is numbered as shown in FIG. 1 (a).

Using vtree, SDD and the logical functions it represents can be recursively defined as follows. "SDD according to vtree v" is one of the following three types. Here, for SDD α, the logical function represented by α is represented as <α>.

は、それ自体がＳＤＤである。ここで、

Is itself an SDD. here,

すなわち恒真関数、

That is, a tautological function,

すなわち恒偽関数である。これらのＳＤＤは以下では定数とよぶ。

That is, it is a constant false function. These SDDs are referred to below as constants.

-For variable X, if v is the leaf corresponding to variable X, then X and ￢X are SDDs that follow v. <X> = X (function true if X is true, false otherwise), <￢X> = ￢X (function false if X is true, true otherwise). These SDDs are referred to below as literals.

• p ₁ , ..., _pn are SDDs that follow the left child node and below of v, <p ₁ >, ..., < _pn > are relatively prime, and s ₁ , ..., s _n are v. Let SDD follow the child nodes to the right of. At this time, {(p ₁ , s ₁ ), ..., ( _pn , s _n )} in which these are paired are SDDs according to v. This SDD represents a logical function (<p ₁ > ∧ <s ₁ >) ∨ ... ∨ (< _pn > ∧ <s _n >). Such SDDs are hereinafter referred to as decomposition nodes.

On the computer, constants and literals are expressed as data of constant length, and the decomposition node is the node number of the _vtree to follow and the array ( _p'1 , s'1), ..., ( _p'n , s'. It is expressed as a pair with _n ). Here, each element of the array (p'i, s'i _{) represents one pair of decompositions (pi i, s i), if p i or s i is a constant or literal} SDD. Is stored in _p'i or _s'i as it is, and if it is a decomposition node, _p'i or _s'i is a pointer to that node.

FIG. 1 (b) illustrates an example of an SDD according to vtree in FIG. 1 (a), which represents the logical function f = (A∧B) ∨ (B∧C) ∨ (C∧D). In the figure, each decomposition node is represented by a circle, and the node number of the vtree that it follows is written in the circle. In addition, each pointer pair of the decomposition node is represented by an arrow extending from the circle. In FIG. 1 (b), the pair of two squares at the tip of each arrow extending from each decomposition node corresponds to a pair ( _{pi, s i )} . Of the two squares, the square on the left side corresponds to _{pi, and the square on the right side corresponds to s i .}

In the SDD of FIG. 1 (b), the function f first takes the form of ((￢A∧B) ∧C) ∨ ((A∧B) ∧true) ∨ (￢B∧ (C∧D)) {A , B} and {C, D}. Similarly, FIG. 1 (d) is an example of an SDD according to vtree in FIG. 1 (c) representing the logical function f = (A∧B) ∨ (C∧D).

SDD can perform the following operations. For the logical function f, the total number of methods of assigning true and false to variables such that f is true is called the model count of f. Given an SDD, the model count of the logical function represented by that SDD can be calculated in a time proportional to the SDD size. The model count of a logical function has applications such as probability inference by Bayesian network and estimation of network reliability.

Next, it is also possible to combine the logical functions f and g by operations such as logical sum ∨ and logical product ∧ with the SDD as it is. More specifically, given an SDD α representing a function f and an SDD β representing a function g, as long as α and β follow the same vtree, the SDDs representing functions such as f∨g and f∧g are α and β. Can be made efficiently from. This operation can be used directly when creating an SDD from a logical function, and is also frequently used in the logical design and verification of systems such as integrated circuits.

One of the points where SDD achieves a small expression is that even if multiple identical logical functions appear as partial functions in the middle of decomposition, only one SDD representing that logical function needs to be created. Can be mentioned. This is called partial structure sharing. In the SDD of FIG. 1 (d), the decomposition node numbered 6 represents the logical function C∧D, but this node is referenced from two places (by a pointer). This means that the function C∧D appears twice in the middle of decomposing the logical function, but even in this case, only one decomposition node representing C∧D is required.

However, as mentioned above, there are many logical functions whose size is still large even with SDD. Therefore, there is a need for a phenotype that has the same functionality as SDD but realizes a smaller expression than SDD. Hereinafter, a technique for providing such a phenotype will be described as an embodiment of the present invention.

(Outline of embodiment)
In this embodiment, when considering the structure of SDD, in addition to causing sharing of substructures when the exact same logical function appears, the same logical function is expressed by replacing a specific kind of variable. Improve the phenotype so that the partial structure is shared even when it becomes. As a result, the number of places where the partial structure can be shared increases as compared with the conventional SDD, so that the expression of the logical function smaller than that of the SDD can be obtained.

In order to make this possible, in the present embodiment, the vtree node numbers that the SDD follows are managed differentially. With this technology, substructures with the same shape but different variable names, which could not be shared with conventional SDDs, can be shared and the size of the expression can be reduced. Moreover, the same functionality as SDD can be guaranteed. In particular, by introducing this technology, it is possible to solve queries related to logical functions or combine them with other logical functions without resolving (unraveling) the substructures that have newly been shared.

<About "Replacement of certain types of variables">
Here, "replacement of a specific type of variable", which is a point of the technique according to the present embodiment, will be described. For example, in the SDD of FIG. 1 (b), the node with the number 1 in the lower center represents the logical function A∧B, and the node with the number 5 on the lower right represents the logical function C∧D. ..

Further, in the vtree of FIG. 1 (a), the substructure of the node No. 1 and below (hereinafter, the substructure of the node and below of the node with vtree is referred to as the subtree of a node) and the subtree of the node No. 5 are other than variables. Has exactly the same structure, and by replacing B with D and A with C, the first subtree can be rewritten to the fifth subtree.

Here, if the same variable replacement is performed for the logical function A∧B, it becomes C∧D. Further, when the same variable is replaced (B → D, A → C) in the structure below the node with the number 1 in the lower center in the SDD of FIG. 1 (b), the node with the number 5 or less on the lower right is replaced. The structure itself is obtained. Thus, for two decomposition nodes, if the following vtree structures match and represent the same logical function under the variable substitutions derived from them, then those decomposition nodes are other than the name of the variable. It has exactly the same structure. Such two decomposition nodes will be referred to below as congruent. In the SDD of FIG. 1 (b), the lower center node No. 1 and the lower right node No. 5 are congruent.

<About VS-SDD>
The SDD improved to bring together the above-mentioned congruent decomposition nodes into one and cause sharing of the partial structure is the variable shift SDD (Variable Shift SDD, hereinafter referred to as VS-SDD) in the present embodiment. be. The VS-SDD technology is as follows.

In SDD, each decomposition node explicitly holds the number of the vtree node to follow, and each literal is kept as it is. However, the congruent decomposition nodes follow different vtree nodes, and the literals in the substructures below them are also different, so if you want to combine the congruent decomposition nodes into one, you should explicitly retain this information. It doesn't become. The technology to solve this is a method of "differentiately" holding the number of the vtree node to be followed, which is the prototype of the VS-SDD technology.

Hereinafter, the first embodiment and the second embodiment will be described as embodiments of the present invention. In the first embodiment, a procedure for converting a normal SDD into a VS-SDD will be described while first explaining the structure of the VS-SDD. In the second embodiment, a procedure for directly converting a logical function into a VS-SDD phenotype will be described.

(First Embodiment)
<Device configuration>
FIG. 2 is a functional configuration diagram of the data structure conversion device 100 according to the first embodiment. The data structure conversion device 100 is a device that converts a normal SDD into VS-SDD. As shown in FIG. 2, the data structure conversion device 100 includes an input unit M01, a preprocessing unit M02, a conversion unit M03, and an output unit M04. The operation of each part will be described later. In the first and second embodiments, since a certain data structure is converted to generate VS-SDD, it is called a "data structure conversion device", but VS-SDD which is data of a graph structure is referred to. Since it is a device for generating data, it may be referred to as a "data generation device".

The data structure conversion device 100 according to the first embodiment can be realized by, for example, causing a computer to execute a program describing the processing contents described in the present embodiment. The point that the data structure conversion device can be realized by the computer and the program in this way is the same in the second embodiment.

The data structure conversion device 100 can be realized by executing a program corresponding to the processing performed by the data structure conversion device 100 by using hardware resources such as a CPU and a memory built in the computer. be. The above program can be recorded on a computer-readable recording medium (portable memory, etc.), stored, and distributed. It is also possible to provide the above program through a network such as the Internet or e-mail.

FIG. 3 is a diagram showing an example of the hardware configuration of the computer according to the present embodiment. The computer of FIG. 3 has a drive device 1000, an auxiliary storage device 1002, a memory device 1003, a CPU 1004, an interface device 1005, a display device 1006, an input device 1007, and the like, which are connected to each other by a bus B, respectively.

The program that realizes the processing in the computer is provided by, for example, a recording medium 1001 such as a CD-ROM or a memory card. When the recording medium 1001 storing the program is set in the drive device 1000, the program is installed in the auxiliary storage device 1002 from the recording medium 1001 via the drive device 1000. However, the program does not necessarily have to be installed from the recording medium 1001, and may be downloaded from another computer via the network. The auxiliary storage device 1002 stores the installed program and also stores necessary files, data, and the like.

The memory device 1003 reads and stores the program from the auxiliary storage device 1002 when the program is instructed to start. The CPU 1004 realizes the function related to the data structure conversion device 100 according to the program stored in the memory device 1003. The interface device 1005 is used as an interface for connecting to a network. The display device 1006 displays a GUI (Graphical User Interface) or the like by a program. The input device 1007 is composed of a keyboard, a mouse, buttons, a touch panel, and the like, and is used for inputting various operation instructions.

<Operation of data structure conversion device 100>
Hereinafter, the operation of each part of the data structure conversion device 100 will be described.

The input unit M01 receives vtree v and SDD α from the outside. The input information is stored in a storage means such as a memory. The preprocessing unit M02 reads v from the storage means, renumbers each node of v, and detects the same subtree of vtree. The conversion unit M03 converts α read from the storage means into VS-SDD β by using v processed by the preprocessing unit M02. The output unit M04 outputs β.

Next, the processing of the preprocessing unit M02 will be described in more detail. FIG. 4 is a flowchart showing a procedure of processing executed by the preprocessing unit M02.

In step S021, the preprocessing unit M02 inputs the vtree v read from the storage means. As illustrated in FIG. 1 (a) and the like, v is a binary tree in which variables correspond to leaves.

In step S022, each node of vtree v is traced according to a certain rule, and numbers are assigned in order from 1 according to the traced order. Here, the "constant rule" in the present embodiment means that the following three operations are performed in the order determined by each node.

-(L) Recursively trace the subtree of the child node on the left.

-(R) Recursively trace the subtree of the child node on the right.

・ (N) Follow your own node.

In particular, the order obtained by operating each node in the order of (N) → (L) → (R) is called the destination order. As an example, the numbering of vtrees in FIG. 1 (a) according to the order of destination is shown in FIG. 5 (a) (left side). The following explanation will be given using the order of destinations, but any method other than the order of destinations may be used as long as the order is set under "certain rules". For example, a passing order or a returning order may be used.

When numbering according to such a rule, the point is that when considering the difference between the node numbers at both ends on each side of the tree (this is called difference numbering), the difference numbering is also the same for the same subtree. It means that it will be. For example, the right side of FIG. 5A depicts the difference numbering for the node numbers in the order of destination shown on the left side, but in the subtree of the order number 2 and the subtree of the order number 5, the difference number is drawn. It can be seen that the nodes are exactly the same.

In step S023, the pretreatment unit M02 detects a vtree portion having the same structure. More specifically, the same subtree of v is detected, for example, by executing a recursive procedure process for v as shown by Algorithm 1 shown in FIG.

The Algorithm 1 shown in FIG. 6 takes vtree v as an input and outputs an associative array e using the node of v as a key. For the vtree node w, the value of e (w) is the node of v having the smallest node number among those whose subtree structure matches the subtree of w.

e has the following properties. e is an associative array such that e (u) = e (v) only when the structures of the subtree of u and the subtree of v match for the two vtree nodes u and w in v. be. Inside the algorithm, another associative array called UniqTable is used. UniqTable is an associative array that returns a node whose subtrees match if it has already been processed. In FIG. 6, as shown in the 1st to 6th lines, as long as the v to be processed is not a leaf, Algorithm 1 is applied to the vtree of the left child node and the vtree of the right child node of v, and 7 As shown in the 9th line from the line, if the node whose subtree matches is already processed by UniqTable, that node becomes the value of e (v).

In step S024 of FIG. 4, the preprocessing unit M02 outputs the destination order numbering and associative array e of v acquired in steps S022 and S023. In the conversion unit M03, this newly numbered v is used.

Next, the processing of the conversion unit M03 will be described. Here, it is a key point of the present technology to use the difference of vtree node numbers.

First, the phenotype of VS-SDD generated by the conversion unit M03 is shown by converting from SDD step by step. Then, the pseudo code is shown. Both the operation of converting step by step and the operation based on the pseudo code are examples of the operation of the conversion unit M03.

First, instead of explicitly holding the vtree node number to be followed by each decomposition node, the conversion unit M03 follows each pointer pointing to the decomposition node with the vtree node number to be followed by the destination node and the original node to be pointed to. Have a difference in vtree node numbers. Next, instead of keeping each literal as it is, it has a difference between the vtree node number of the leaf corresponding to the variable of the literal and the vtree node number followed by the decomposition node having the literal as the decomposition. The vtree node number used here is based on the destination order numbering obtained by the preprocessing unit M02.

As a specific example of executing the above processing, FIG. 5 shows a structure in which the vtree numbers are differentiated in the SDD of FIG. 1 (b) after considering the vtree destination order numbering shown in FIG. 5 (a). Shown in (b). For example, in FIG. 5 (b), the difference "1" attached to the pointer in the middle row on the leftmost side is the vtree node number 2 followed by the decomposed node to be pointed to, and the vtree node number followed by the original node to be pointed to. It is the difference minus 1. Further, the literal B (FIG. 1 (b)) at the lower left end is the difference between the vtree node number 3 of the leaf corresponding to B and the vtree node number 2 followed by the decomposition node having the literal as the decomposition (element). Becomes one.

As shown in FIG. 5 (b), the structures below the nodes that were congruent in the original SDD are converted into exactly the same structure including the difference in the vtree node numbers introduced in the above procedure. For example, in FIG. 5B, the lower center and the lower right decomposition nodes were originally congruent, but after conversion, they are exactly the same including the structures below them. The conversion unit M03 achieves a reduction in the number of nodes by converting the data structure so as to share the same partial structure thus generated.

The structure obtained by sharing the same partial structure generated in FIG. 5 (b) is shown in FIG. 5 (c). As shown in FIG. 5 (c), in FIG. 5 (b), the two decomposition nodes at the tip of the pointer extending from each of the center and the right two elements (subtree root node) of the top decomposition node and their respective. In FIG. 5C, the four elements mentioned above share a structure consisting of one decomposition node and the two elements beyond it.

In this way, the structure obtained by performing conversion using the difference in vtree node numbers and sharing the same partial structure generated by the conversion is called VS-SDD.

The conversion unit M03 may simultaneously perform conversion to use the difference in vtree node numbers and share the same partial structure. FIG. 7 shows Algorithm 2 showing the processing procedure of the conversion unit M03 that executes such processing. It should be noted that the process of simultaneously converting to use the difference in vtree node numbers and sharing the same partial structure is essentially the same as the above process described with reference to FIG.

Here, for SDD α, the vtree node that α follows is represented as v (α), and for vtree node v, the number according to the order of destination is num (v).

As shown in FIG. 7, this algorithm takes SDD α as an input and outputs a structure obtained by converting α into VS-SDD. Inside the algorithm, the associative array e obtained by the preprocessing unit M02 is used. As described above, the associative array e has the smallest node number among the nodes whose value e (w) matches the node w whose subtree structure is w with respect to the node w of vtree v. It is an associative array as there is.

On the data structure converter 100 (that is, on the computer), the VS-SDD of the decomposition node is represented by an array {( _p'1 , s'1), ..., ( _p'n , _s'n ) _} . .. Here, each p'i is itself when the corresponding element p _i is a constant, a pair of a vtree node number difference and a flag indicating whether it is a negative literal (￢ ₎ in the case of a literal, and vtreee in the case of a decomposition node. A pair of node numbers and their pointers to VS-SDD. The same applies to _s'i .

In Algorithm 2, the sixth line is a process in which _p'i is a constant when the p _i of the corresponding element is a constant. The 7th and 8th lines are the processes of converting literals into differences in vtree node numbers. The "num (v (v (pi _{))-num (v (α))" used in the 7th and 8th lines corresponds to the vtree node number (that is, the literal) to which p i (} = literal) follows. It is the difference obtained by subtracting the number of the original vtree node pointing to pi (= literal) from the _vtree node number). The ninth line shows the process of setting the difference between the _vtree node numbers and the pair of the pointer (VS ( _pi )) to the VS-SDD of the decomposition node as p'i when p _i is the decomposition node.

As shown in FIG. 7, two associative arrays, ConvTable and UniqTable, are used inside the algorithm.

The ConvTable maintains a correspondence between the input SDD α node and the output VS-SDD node. UniqTable is an associative array that returns a pointer to the VS-SDD of the substructure if the congruent substructure has already been processed. Here, the associative array e created by the preprocessing unit M02 is used to determine whether the structure of the vtree subtree is the same. If the congruent substructure has not been processed yet (line 12), create a new decomposition node VS-SDD with CreateNewNode on line 13.

For example, when the SSD of FIG. ₁ (b) and the vtree of FIG. 5 (a) are input, {( _p'1 , s'1), ..., (p) as shown in FIG. 5 (c). Constants, differences, pointers and differences, etc. are set _in'n , _s'n )} (each of a pair of squares). Further, in the SSD of FIG. 1B, when the decomposition node according to vtree node number 5 is processed, it is congruent with the decomposition node on the left side thereof. Therefore, the VS-SDD corresponding to the decomposition node on the left side by UniqTable. A pointer to is returned. Therefore, as shown in FIG. 5C, a structure sharing a congruent structure can be obtained.

(Second embodiment)
<Outline of the second embodiment>
Next, a second embodiment will be described. In the second embodiment, a data structure conversion device 200 that directly converts a logical function into VS-SDD is provided.

In the second embodiment, the logical function is a constant (true or false) or variable, a negative operation (￢), a logical sum (∨), a logical product (∧), and an exclusive OR ("+". It shall be expressed in combination with a binary operation such as), and its syntax tree and vtree are given as input (note that in the text of this specification, the exclusive OR symbol (〇) is given for convenience of description. The symbol) with + inside is expressed as "+"). That is, it is assumed that the logical function is given in a state where the structure and order in which the various logical operations are applied are known.

For example, in the case of a logical function (A∧B) ∨ (B∧C) ∨ (C∧D), first take the logical product of A and B, and then B Take the logical product of C, then the logical product of C and D, then the logical product of A and B, the logical product of B and C, and finally the logical sum of all of them, and so on. It is assumed that you know that you should calculate.

Even if a logical function such as (A∧B) ∨ (B∧C) ∨ (C∧D) is given as a character string, the structure of the logical operation can be obtained by parsing the character string. Specifying the order is a common technique. Therefore, a logical function as a character string may be input to the data structure conversion device 200, the data structure conversion device 200 may perform parsing, calculate a syntax tree, and use the syntax tree.

Taking (A∧B) ∨ (B∧C) ∨ (C∧D) as an example, the data structure conversion device 200 processes in order from the lower layer to the upper layer according to the syntax tree of FIG. I do. That is, first, VS-SDDs of A∧B, B∧C, and C∧D are created, and then VS-SDD of (A∧B) ∨ (B∧C) is used using the VS-SDD. And finally create VS-SDD of (A∧B) ∨ (B∧C) ∨ (C∧D) using the resulting VS-SDD and VS-SDD of C∧D. In creating this VS-SDD, an algorithm (Algorithm 3 to 5) for logical operations described later is used. Since the VS-SDDs of A, B, C, and D are A, B, C, and D, for example, VS-SDD of A∧B is relative to VS-SDD of A and VS-SDD of B. It can be obtained by performing a logical operation described later.

In the data structure conversion device 200 according to the second embodiment, in order to efficiently perform the above processing, VS-SDD representing the denial of the logical function represented by α when VS-SDD α, β is given, or VS-SDD. VS-SDD, which represents the logical sum, logical product, and exclusive logical sum of the logical function represented by α and β, can be efficiently calculated while maintaining the expression form of VS-SDD.

<Device configuration and operation>
FIG. 9 shows a configuration diagram of a data structure conversion device 200 that directly converts a logical function into VS-SDD in the second embodiment.

As shown in FIG. 9, the data structure conversion device 200 has an input unit M11, a preprocessing unit M12, a construction unit M13, and an output unit M14.

The input unit M11 receives vtree v and a logical function f (here, in the form of a syntax tree). The input information is stored in a storage means such as a memory. The preprocessing unit M12 reads v from the storage means, renumbers each node of v, and detects the same subtree of vtree. The construction unit M13 converts f into VS-SDD α by using v processed by the preprocessing unit M12. The output unit M14 outputs α. Since the processing of the preprocessing unit M12 is exactly the same as the processing of the preprocessing unit M02 of the system that converts SDD to VS-SDD, the processing of the construction unit M13 will be described below.

Based on the output of vtree v and the preprocessing unit M12, the construction unit M13 has various logics as described above according to the structure and order of the logical operations in the logical function f (these are held as information of the syntax tree). Apply the operation repeatedly. Negation operations and binary operations will be described below as logical operations executed by the construction unit M13.

The construction unit M13 executes a negative operation in VS-SDD by Algorithm 3 in FIG.

As shown in FIG. 10, if the vtree node number that α follows is j _α for VS-SDD α, the result returned by Negate (α, j _α , true) is the negation of the logical function represented by α. It becomes VS-SDD to represent.

ConvTable in Algorithm 3 is an associative array for storing the calculation result, and ConvTable (α, true) stores a pointer to the VS-SDD node that represents the negation of α, and ConvTable (α, false) stores the pointer to the VS-SDD node. Saves a pointer to α.

UniqTable is an associative array that returns a pointer to a node that has already been calculated when the result of the calculation matches the node of the result that has already been calculated. The contents of Algorithm 3 shown in FIG. 10 are as follows in more detail.

First, in the first and second lines, if Negate (α ,,, flg) has already been calculated for the same α and flg, a pointer to the calculation result is returned. This prevents the same calculation from being performed more than once.

If not, the negative operation is actually performed in the fourth line and below. If the logical function f is decomposed into {(p ₁ , s ₁ ), ..., ( _pn , s _n )}, then the logical function ￢f is {(p ₁ , ￢s ₁ ) ,. ., (P _n , ￢s _n )}. That is, the negation of the original function can be calculated by performing the negation operation on the _si side while leaving the p _i side as it is.

First, the calculation on the _pi side is performed on the 6th to 9th lines. Since the pi side is left as it is, if it is a constant or literal, it is not changed, and if it is not, the same thing is returned as it is by executing Negate of flg ₌ false.

Next, the calculation on the _si side is performed on the 10th to 13th lines. If s _i is flg = false, it does not change like p _i , but if flg = true, if s _i is a constant or a literal, it calculates the negation as it is (line 11), otherwise. If so, the negation of the nodes below it is calculated recursively (line 13). Finally, on lines 15 and 16, if the congruent substructure has not already appeared, a new decomposition node VS-SDD is created. If the congruent substructure has been processed, a pointer to the corresponding VS-SDD is returned.

The construction unit M13 executes a binary operation such as a logical sum, a logical product, and an exclusive logical sum when two VS-SDDs are given, according to Algorithm 4 shown in FIGS. 11A to 11C.

As shown in FIGS. 11A to 11C, if the vtree node numbers to be followed for VS-SDD α and β are j _α and j _β , respectively, Apply (α, β, false, false, j _α , j _β , The result returned by 〇) is VS-SDD representing a logical function obtained by applying 〇 to the logical function represented by α and β. In addition, it is assumed that binary operations such as logical sum ∨, logical product ∧, and exclusive OR + are entered in 〇.

Two associative arrays are also used in Algorithm 4, ConvTable is used to store the operation result, and UniqTable is used to store the calculated nodes. In the pseudocode, the LCA on the third line is either when two vtree node numbers x and y are entered and the tree is traced from the node with the number x and the node with the number y to the root respectively. A function that returns the deepest node (recently common ancestor) to visit.

The Consistency on the 35th line is a function for determining whether or not the logical function represented by the input VS-SDD is not false, and its pseudo code is shown in Algorithm 5 (FIG. 12). The difference from the same operation (Apply operation) in normal SDD is that VS-SDD always tracks the vtree node number (j _α , j _β ) that the node (α and β) of interest follows. Is. The contents of Algorithm 4 shown in FIGS. 11A to 11C are as follows in more detail.

Lines 1-5 are preprocessing. Where v and ￢v represent literals. In lines 6-8, if α and β are both constants, one is a constant and one is a literal, or both are literals related to the same variable, the operation result α ○ β is returned immediately.

Further, in the 9th and 10th lines, if the same calculation has already been performed, a pointer to the calculation result is returned to prevent the exact same calculation from being performed twice or more. At this time, by using e _α and e _β calculated in the 4th and 5th lines instead of j _α and j _β as the 5th and 6th arguments of ConvTable, two substantially equivalent operations resulting from congruence can be performed. It also prevents doing more than once. If none of these apply, the actual calculation is performed from the 12th line onward.

The VS-SDD of the operation result of α according to vtree v _α and β according to v _β follows vtree LCA (v _α , v _β ). Therefore, in the 12th to 23rd lines, the decomposition of α and β by LCA (v _α , v _β ) is stored in α'and β', and the subsequent calculations use α'and β'. And proceed.
After that, α'= {(p ₁ , s ₁ ), ..., ( _pn , sn) _} , β'= {(q ₁ , r ₁ ), ..., (q _m , r _m ) )}, The result of α'○ β'is {(p ₁ ∧ q ₁ , s ₁ ○ r ₁ ), ..., (p ₁ ∧ q _m , s ₁ ○ r _m ), ... , (P _n ∧ q ₁ , s _n ○ r ₁ ), ..., ( _pn ∧ q _m , s _n ○ r _m )}.

(P _i , s _i , f _{{p, i}} , f _{{s, i}} ) in each α'and (q _l , r _l , f _{{q, l}} , f _{{r, l} in β' _} ) Perform the necessary conversions on lines 26-30, 32, and 33, and calculate pi _{∧ q l on} line 34.

If p _i ∧ q _l becomes false, there is no point in calculating the corresponding _{si ○ r l ,} so judge this with the Consistent on the 35th line, and if it is not false, on the 36th line. s _i ○ r _l is calculated. The conversion is performed on the 37th to 40th lines, and (pi ∧ q _l , s _i ○ r _{l )} is added to the calculation result on the 41st line.

In lines 42-43, similar to Algorithm 3, a new decomposition node VS-SDD is generated if a congruent partial structure has not yet appeared. If the congruent substructure has been processed, a pointer to the VS-SDD is returned.

(About the effect)
The effect of VS-SDD is simply that the expression is more compact than SDD, and the processing such as various queries and combinations with other logical functions is speeded up accordingly. First, the size of VS-SDD will be described, and then the model count and the combination with other logical functions will be described.

First, regarding the size of VS-SDD, what is done by the algorithm for making VS-SDD from SDD (Algorithm 2 (Fig. 7)) shares the same partial structure as a result of considering the difference in vtree node numbers. Therefore, the size does not increase when converting SDD to VS-SDD. Further, there is also a logical function in which the size of the expression of VS-SDD is exponentially smaller than that of SDD.

Next, the model count in VS-SDD will be described. Given VS-SDD α, the model count of the logical function represented by α can be calculated by Algorithm 6 (FIG. 13). In Algorithm 6, for an integer j, num ^-1 (j) represents a vtree node such that the node number is j (in the order of destination). Also, for vtree node w, l (w) is the number of leaves present in the vtree subtree rooted at w. As described above, for vtree node v, v _l and v _r are child nodes on the left and child nodes on the right. In the model count in VS-SDD, the newly shared node is also scanned only once by considering the difference in vtree node numbers, so that the model count operates at a higher speed because the size is smaller than the model count in normal SDD.

Finally, the operation (Apply operation) in combination with other logical functions in VS-SDD will be described. The algorithm for taking the logical product, OR, exclusive OR, etc. of logical functions using VS-SDD is as shown in Algorithm 4 (FIGS. 11A to 11C). In the Apply operation in VS-SDD, as in the model count calculation, the new node is shared, which has the effect of reducing the part that was calculated more than once in the Apply operation in SDD to only once. It operates faster because of its smaller size.

(Summary of embodiments)
As described above, the present specification describes at least the devices, methods, data structures, and programs described in the following sections.
(Section 1)
A data generator that generates graph structure data that expresses the decomposition of logical functions according to a predetermined tree structure.
Based on the order tree that specifies the variable order when decomposing the logical function, when a plurality of substructures representing the same decomposition are specified in the decomposition of the logical function, the plurality of substructures are specified. As a representative substructure, one substructure selected from the above is used as a representative substructure.
The graph structure data corresponding to the logical function so that the remaining data in the graph structure corresponding to the parent node of the same partial structure shares the graph structure data corresponding to the representative partial structure by the pointer. A data generator, including a construction unit that produces.
(Section 2)
A node number is assigned to each node of the order tree according to a predetermined rule, and a structure is formed in the order tree based on the difference of the node numbers attached to the nodes at both ends of each side of the order tree. Further equipped with a pretreatment section that identifies the same subtree,
The data generation device according to paragraph 1, wherein the construction unit uses a subtree having the same structure specified by the pretreatment unit to specify a plurality of substructures having the same structure.
(Section 3)
The construction unit receives graph structure data representing the SDD corresponding to the logical function as an input.
If the input graph structure data contains data representing a literal, the difference between the node number corresponding to the literal and the node number of the root node of the subtree representing the decomposition corresponding to the decomposition node containing the literal. As well as replacing it with
If the input graph structure data includes a pointer to another decomposition node, the graph structure data that is a partial structure corresponding to the subtree whose structure specified by the preprocessing unit is the same has already been constructed. In this case, the data generation device according to the second paragraph, which changes the pointer so that the point pointed to by the pointer becomes the information storage destination of the graph structure data already constructed.
(Section 4)
The construction unit generates the graph structure data corresponding to the decomposition of each variable according to the order of decomposition of the variables specified by the order tree.
When the element of the decomposition is a literal, the graph structure data is the value of the difference between the node number corresponding to the literal and the node number of the root node of the subtree representing the decomposition corresponding to the decomposition node including the literal. Store and
If the element of the decomposition is a constant, store the constant and
When the element of the decomposition refers to another decomposition, if the graph structure data in which the structure specified by the preprocessing unit is a partial structure corresponding to the same subtree has already been constructed, the relevant The point pointed to by the pointer stores the information of the pointer pointing to the information storage destination of the already constructed graph structure data. If not, the graph structure data corresponding to the other decomposition is created and the other decomposition is performed. The data generation device according to Section 2, which is generated by storing information of a pointer pointing to an information storage destination of graph structure data corresponding to.
(Section 5)
It is a data generation method executed by a data generator that generates graph structure data that expresses the decomposition of a logical function according to a predetermined tree structure.
Based on the order tree that specifies the variable order when decomposing the logical function, when a plurality of substructures representing the same decomposition are specified in the decomposition of the logical function, the plurality of substructures are specified. As a representative substructure, one substructure selected from the above is used as a representative substructure.
The graph structure data corresponding to the logical function so that the remaining data in the graph structure corresponding to the parent node of the same partial structure shares the graph structure data corresponding to the representative partial structure by the pointer. A construction step, which includes a data generation method.
(Section 6)
It is a data structure of a graph structure that expresses the decomposition of a logical function according to a predetermined tree structure.
The value of the element corresponding to the leaf variable in the predetermined tree structure is the node number of the node in the predetermined tree structure corresponding to the leaf and the node number of the node in the predetermined tree structure followed by the node having the element. As a difference with
The value of the element having the pointer is the difference between the node number of the node of the predetermined tree structure followed by the node pointed to by the pointer and the node number of the node of the predetermined tree structure followed by the node having the element. The data structure used as the pointer.
(Section 7)
A program for making a computer function as each part of the data generation device according to any one of the items 1 to 4.

Although the present embodiment has been described above, the present invention is not limited to such a specific embodiment, and various modifications and changes can be made within the scope of the gist of the present invention described in the claims. It is possible.

100, 200 Data structure conversion device M01, M11 Input unit M02, M12 Preprocessing unit M03, M13 Conversion unit M04, M14 Output unit 1000 Drive device 1002 Auxiliary storage device 1003 Memory device 1004 CPU
1005 Interface device 1006 Display device 1007 Input device

Claims (6)

A data generator that generates graph structure data that expresses the decomposition of logical functions according to a predetermined tree structure.
Based on the order tree that specifies the variable order when decomposing the logical function, when a plurality of substructures representing the same decomposition are specified in the decomposition of the logical function, the plurality of substructures are specified. As a representative substructure, one substructure selected from the above is used as a representative substructure.
The graph structure data corresponding to the logical function is shared so that the remaining data in the graph structure corresponding to the parent node of the same partial structure shares the graph structure data corresponding to the representative partial structure by the pointer. A data generator with a building unit to generate. A node number is assigned to each node of the order tree according to a predetermined rule, and a structure is formed in the order tree based on the difference of the node numbers attached to the nodes at both ends of each side of the order tree. Further equipped with a pretreatment section that identifies the same subtree,
The data generation device according to claim 1, wherein the construction unit uses a subtree having the same structure specified by the pretreatment unit to specify a plurality of substructures having the same structure. The construction unit receives graph structure data representing the SDD corresponding to the logical function as an input.
If the input graph structure data contains data representing a literal, the difference between the node number corresponding to the literal and the node number of the root node of the subtree representing the decomposition corresponding to the decomposition node containing the literal. As well as replacing it with
If the input graph structure data includes a pointer to another decomposition node, the graph structure data that is a partial structure corresponding to the subtree whose structure specified by the preprocessing unit is the same has already been constructed. In this case, the data generation device according to claim 2, wherein the pointer is changed so that the point pointed to by the pointer becomes the information storage destination of the graph structure data already constructed. The construction unit generates the graph structure data corresponding to the decomposition of each variable according to the order of decomposition of the variables specified by the order tree.
When the element of the decomposition is a literal, the graph structure data is the value of the difference between the node number corresponding to the literal and the node number of the root node of the subtree representing the decomposition corresponding to the decomposition node including the literal. Store and
If the element of the decomposition is a constant, store the constant and
When the element of the decomposition refers to another decomposition, if the graph structure data in which the structure specified by the preprocessing unit is a partial structure corresponding to the same subtree has already been constructed, the relevant The destination pointed to by the pointer stores the information of the pointer pointing to the information storage destination of the already constructed graph structure data. If not, the graph structure data corresponding to the other decomposition is created and the other decomposition is performed. The data generation device according to claim 2, which is generated by storing information of a pointer pointing to an information storage destination of graph structure data corresponding to. A data generation method executed by a computer by causing a computer to execute a program in order to generate graph structure data expressing the decomposition of a logical function according to a predetermined tree structure.
Based on the order tree that specifies the variable order when decomposing the logical function, when a plurality of substructures representing the same decomposition are specified in the decomposition of the logical function, the plurality of substructures are specified. As a representative substructure, one substructure selected from the above is used as a representative substructure.
The graph structure data corresponding to the logical function is shared so that the remaining data in the graph structure corresponding to the parent node of the same partial structure shares the graph structure data corresponding to the representative partial structure by the pointer. A data generation method comprising, said computer -generated construction steps. A program for making a computer function as each part of the data generation device according to any one of claims 1 to 4.

Images