SDD Beginning-User Manual Version 1.1
Contents
1. int sdd_node_is_true SddNode node int sdd_node_is_false SddNode node Queries and Transformations SddNode sdd_conjoin SddNode node1 SddNode node2 SddManager manager SddNode sdd_disjoin SddNode node1 SddNode node2 SddManager manager SddNode sdd_negate SddNode node SddManager manager SddNode sdd_condition SddLiteral lit SddNode node SddManager manager SddNode sdd_exists SddLiteral var SddNode node SddManager manager SddNode sdd_forall SddLiteral var SddNode node SddManager manager SddModelCount sdd_model_count SddNode node SddLiteral sdd_minimum_cardinality SddNode node SddNode sdd_minimize_cardinality SddNode node SddManager manager int sdd_variables SddNode node SddManager manager File I O void sdd_save const char fname SddNode node void sdd_save_as_dot const char fname SddNode node SddNode sdd_read const char filename SddManager manager Memory Management void sdd_ref SddNode node SddManager manager void sdd_deref SddNode node SddManager manager SddRefCount sdd_ref_count SddNode node SddId sdd_id SddNode node int sdd_garbage_collected SddNodex node SddSize id 18 D License Copyright c 2013 Regents of the University of California All rights reserved Redistribution and use in source and binary forms with or without modification are permitted provided that the following conditions are met R2. sdd_equiv sdd_manager_literal A m sdd_manager_literal B m m alpha sdd_disjoin alpha sdd_manager_literal B m m alpha sdd_imply sdd_manager_literal faulty1 m alpha m delta sdd_conjoin delta alpha m Once we have incorporated all sentences we can start performing queries on our model using the final SDD that we constructed 5 4 Querying SDDs Given an SDD representation of our knowledge base A we can begin to assert observations in our model and make inferences about them In our diagnosis example we would like to observe some system behavior and then diagnose the possible faults First we can condition an SDD on a literal using the following function SddNode sdd_condition SddLiteral lit SddNode node SddManager manager For example we can assert the observation that input A is high and output C is low delta sdd_condition A delta m delta sdd_condition C delta m Conditioning a knowledge base A on a literal X denoted by A X replaces each instance of literal X in A by true and each instance of literal X in A by false Analogously conditioning A on a literal X denoted by A X replaces X by false and X by true In our example the SDD for A A C is then B faulty2 B faulty First we want to test whether our observation A A C is normal all components can be healthy or abnormal there exists a fault In particular we wan
3. 842 849 2012 3 A Choi and A Darwiche Dynamic minimization of sentential decision diagrams in Proceedings of the 27th AAAI Conference on Artificial Intelligence AAAI pp 187 194 2013 11 A Code Sample With Garbage Collection Disabled include lt stdio h gt include lt stdlib h gt include sddapi h returns an SDD node representing node1 gt node2 SddNode sdd_imply SddNode node1 SddNode node2 SddManager manager return sdd_disjoin sdd_negate nodel manager node2 manager returns an SDD node representing node1 lt gt node2 SddNode sdd_equiv SddNode node1 SddNode node2 SddManager manager return sdd_conjoin sdd_imply node1 node2 manager sdd_imply node2 nodel manager manager int main int argc char argv set up vtree and manager SddLiteral var_count 5 int auto_gc_and_minimize 0 SddManager m sdd_manager_create var_count auto_gc_and_minimize SddLiteral A 1 B 2 C 3 faulty1 4 faulty2 5 SddNode delta sdd_manager_true m SddNode alpha CONSTRUCT KNOWLEDGE BASE faulty1 gt A lt gt B alpha sdd_equiv sdd_manager_literal A m sdd_manager_literal B m m alpha sdd_imply sdd_manager_literal faulty1 m alpha m delta sdd_conjoin delta alpha m faultyl gt A lt gt B v B alpha sdd_equiv sdd_manager_literal A m sdd_manager_literal B
4. AA C we would like to reason about the health states that are consistent with that observation Any such health state is further called a diagnosis 5 The SDD Library In this section we will highlight the core components of the SDD library using a running example for the diagnostic application we just discussed In particular we will show how to construct an SDD that represents the knowledge base A We will then show how to manipulate this SDD to obtain answers to diagnostic queries 5 1 The SDD Manager The construction and manipulation of SDDs is done via an SDD manager Hence a typical program using the SDD library will have the following structure where the first thing to do is create an SDD manager and the last thing to do is free the manager include lt stdio h gt include lt stdlib h gt include sddapi h int main int argc char argv initialize manager SddLiteral var_count 5 initial number of variables int auto_gc_and_minimize 0 disable 0 or enable 1 auto gc amp auto min SddManager manager sdd_manager_create var_count auto_gc_and_minimize CONSTRUCT MANIPULATE AND QUERY SDDS fae free manager sdd_manager_free manager return 0 An SDD manager keeps track of all its associated SDDs Hence by freeing the SDD manager one also frees the memory of all SDDs created within that manager When we create an SDD manager we declare an initial number of variable
5. T This SDD corresponds to the sentence faulty A faulty V faulty which has three models faulty A faulty afaulty A faulty faulty A faultyg Often we are interested in the minimum cardinality diagnoses ones with a minimal number of faults The SDD package supports this type of query as well SddNode x min_diagnosis sdd_minimize_cardinality diagnosis m More generally the cardinality of a model is the number of positive literals that appear in the model The models of the SDD returned by sdd_minimize_cardinality are precisely the minimum cardinality models of the input SDD In our example this function gives the following SDD faulty faulty2 faulty1 faulty2 which represents the sentence faulty A faulty V faulty A faulty The SDD library provides a function for counting the models of an SDD For example the following code snippet counts the number of diagnoses and minimum cardinality diagnoses in our example SddModelCount count sdd_model_count diagnosis m SddModelCount min_count sdd_model_count min_diagnosis m Here we have 3 diagnoses and 2 minimum cardinality diagnoses The functions sdd_model_count sdd_minimum_cardinality and sdd_minimize_cardinality are with respect to the variables that a given SDD essentially depends on More formally we say that a Boolean function f and analogously an SDD essentially depends on a varia
6. faulty2 0 min_diagnosis sdd_conjoin tmp min_diagnosis sdd_manager_literal faulty2 m m sdd_ref min_diagnosis m sdd_deref tmp m free variables count the number of minimum cardinality diagnoses and minimum cardinality SddModelCount min_count sdd_model_count min_diagnosis m SddLiteral min_card sdd_minimum_cardinality min_diagnosis printf sdd model count 4 PRImcS n count printf sdd model count min PRImcS n min_count printf sdd cardinality 4 PRI1itS n min_card SAVE SDDS printf saving sdd and dot n sdd_save output circuit kb sdd delta sdd_save output diagnosis sdd diagnosis sdd_save output diagnosis min sdd min_diagnosis sdd_save_as_dot output circuit kb dot delta sdd_save_as_dot output diagnosis dot diagnosis sdd_save_as_dot output diagnosis min dot min_diagnosis I 1 CLEAN UP sdd_manager_free m return 0 17 C SDD API Core Following are the core functions of the SDD library The advanced user manual describes the complete API SDD Manager SddManager sdd_manager_create SddLiteral var_count int auto_gc_and_minimize void sdd_manager_free SddManager manager Elementary SDDs SddNode sdd_manager_true const SddManager manager SddNode sdd_manager_false const SddManager manager SddNode sdd_manager_literal const SddLiteral literal SddManager manager
7. of the SDD represents the Boolean function f 5BA CAD V GAA B AC V AAB AT AA B V BAC V CAD C Figure 2 A simple circuit consisting of two inverters labeled 1 and 2 and three wires labeled A B and C SDDs are structured representations of Boolean functions which allow certain operations to be performed efficiently in practice if not also in theory For example one can conjoin and disjoin two SDDs efficiently One can also for example perform model counting in time that is linear in the size of the SDD For more on SDDs including theoretical and practical comparisons with OBDDs see 1 2 3 3 Preliminaries In the next section we shall highlight the core components of the SDD library using a running example based on a diagnostic application The source code for this example is included in the SDD package and also in Appendix A We will start though by showing how to compile a program with the SDD library 3 1 The Header File The functions and types used in the SDD library are declared in the header file sddapi h This manual however is based on a small subset of the functions declared in this file We call this the core API and summarize it in Appendix C 3 2 Compiling To compile the examples in this manual under Linux one can save a code sample say from Section A to a file circuit c in a directory which contains 1 a subdirectory include containing the header file sddapi h and 2 a subdirectory
8. SDD Beginning User Manual Version 1 1 Arthur Choi and Adnan Darwiche Automated Reasoning Group Computer Science Department University of California Los Angeles Email sdd cs ucla edu Download http reasoning cs ucla edu sdd November 7 2013 The Sentential Decision Diagram SDD is a canonical representation of Boolean functions The SDD package which is distributed as a C library called libsdd allows users to construct manipulate and optimize SDDs This manual describes the basics of the SDD package meant for users who are interested in immediately constructing SDDs and performing queries on them An advanced user s manual is also provided for those users interested in more fine grained access to some of the library s features The license terms for the SDD package are given at the end of this manual Q 4 y DIC FOL BRA FAL BJA PBL Figure 1 A graphical depiction of an SDD for the Boolean function f A B V BAC V CAD 1 Introduction The Sentential Decision Diagram SDD is a recently proposed representation of Boolean functions 1 2 3 The SDD can be thought of as a data structure for representing Boolean functions since SDDs are canonical and support a number of efficient operations for constructing and manipulating Boolean functions Figure 1 depicts an example SDD and the Boolean function it represents This manual p
9. a simple text format which is described in the file itself The file can be read in again using the code snippet SddLiteral var_count 5 SddManager manager sdd_manager_create var_count SddNode sdd sdd_read diagnosis min sdd manager To use the function sdd_read we need an SDD manager with a variable count that is large enough to cover all variables mentioned by the saved SDD The SDD library also allows us to visualize SDDs via the graph drawing system GraphViz available at http www graphviz org The SDDs illustrated in this manual were indeed generated by the dot program The following code snippet saves an SDD to dot format sdd_save_as_dot diagnosis min dot min_diagnosis We can then use the dot program to generate a graphical depiction of the SDD as a PNG image file using the following command dot Tpng odiagnosis min png diagnosis min dot Note that in the generated graphs variables with indices from 1 to 26 are mapped to letters from A to Z Higher indices simply have their index printed 6 Garbage Collection While constructing and manipulating SDDs one may construct many intermediate SDDs that are used once but can subsequently be discarded The SDD library itself produces auxiliary SDDs to perform certain operations For sufficiently complex programs these auxiliary SDDs will eventually exhaust a system s memory unless garbage collected The SDD library includes a gar
10. bage collector which is based on reference counts SDD nodes can be referenced and dereferenced using the following functions void sdd_ref SddNode node SddManager manager void sdd_deref SddNode node SddManager manager Any SDD node that is not currently referenced is subject to garbage collection which can be invoked manually or automatically by the SDD library as needed We will restrict our discussion here to automatic garbage collection leaving manual garbage collection to the advanced user manual Automatic garbage collection can be activated by creating an SDD manager as follows int auto_gc_and_minimize 1 disable 0 or enable 1 auto gc amp auto min SddManager manager sdd_manager_create var_count auto_gc_and_minimize When automatic garbage collection is activated the SDD library will occasionally try to minimize the size of existing SDDs an operation that is distinct from cardinality minimization which we discussed in the previous section Hence the structure of SDDs which can be visualized using dot may change over time although the logical content of such SDDs will remain the same In the example from Section 5 we can reference any SDD node as soon as soon as it is created We can also dereference an SDD node as soon as we know that we will no longer use it We can do this in a systematic way line by line Consider the following code snippet where we construct the first sentence of our k
11. ble X iff f X 4 f 7X We can see what variables an SDD depends on using the function int sdd_variables SddNode node SddManager manager If an SDD manager is associated with n variables then function sdd_variables returns an array of length n 1 where the i th entry is 1 if the SDD essentially depends on the i th variable and 0 otherwise The 0 th entry is unused Suppose that we had observed wires A and B to be high If we condition our knowledge base on this ob servation and then existentially quantify out variable C we get faulty Calling sdd_minimize_cardinality on this result also returns faulty However the minimum cardinality diagnoses with respect to variables faulty and faulty is faulty A faulty As the function representing our diagnoses does not essentially depend on variable faulty we should compensate for the absence of faulty in terms of the model count and minimum cardinality models For model counting we can multiply the model count obtained by 2 for each missing variable For minimum cardinality models we can conjoin the corresponding negative literal for each missing variable We perform such a check in our example in Appendix A 5 5 File I O We can save any SDD that we create to a file For example the following code snippet saves the SDD representing our minimum cardinality diagnoses to a file called diagnosis min sdd sdd_save diagnosis min sdd min_diagnosis The SDD file format is
12. edistributions of source code must retain the above copyright notice this list of conditions and the following disclaimer Redistributions in binary form must reproduce the above copyright notice this list of conditions and the following disclaimer in the documentation and or other materials provided with the distribution Neither the name of the University of California nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS AS IS AND ANY EXPRESS OR IMPLIED WARRANTIES INCLUDING BUT NOT LIMITED TO THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT INDIRECT INCIDENTAL SPECIAL EXEMPLARY OR CONSEQUENTIAL DAMAGES INCLUDING BUT NOT LIMITED TO PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES LOSS OF USE DATA OR PROFITS OR BUSINESS INTERRUPTION HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY WHETHER IN CONTRACT STRICT LIABILITY OR TORT INCLUDING NEGLIGENCE OR OTHERWISE ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE 19
13. eference any input SDDs that are no longer needed One can check the reference count of an SDD node using the following function SddRefCount sdd_ref_count SddNode node This can be useful for debugging purposes To aid further with debugging the following functions are provided by the SDD library SddId sdd_id SddNode node int sdd_garbage_collected SddNode node SddSize id 10 Every SDD node is assigned a unique ID when created Moreover when an SDD node is garbage collected its structure is not freed Instead it is added to a special list called the gc list allowing this structure to be reused for newly created SDD nodes When this structure is reused though it will be assigned a new ID Hence to test whether a node has been garbage collected one must supply both a pointer to the node and its ID The following code snippet shows how to test whether a node has been garbage collected SddId id sdd_id alpha Th ae CONSTRUCT MANIPULATE AND QUERY SDDS if sdd_garbage_collected alpha id alpha has been garbage collected 7 Beyond the Manual This manual covered only the core concepts for getting started with the SDD library The advanced user manual covers a number of additional topics that would become important for applications that require finer grained control of the machinery underlying the SDD library These include topics such as e manual garbage collection and minimization T
14. faulty1 variables faulty2 missing_health_vars health_vars health_vars_count count lt lt missing_health_vars multiply by 2 missing_health_vars free variables find minimum cardinality diagnoses SddNode min_diagnosis sdd_minimize_cardinality diagnosis m variables sdd_variables min_diagnosis m adjust for missing faults if variables faulty1 0 min_diagnosis sdd_conjoin min_diagnosis sdd_manager_literal faulty1 m m if variables faulty2 0 min_diagnosis sdd_conjoin min_diagnosis sdd_manager_literal faulty2 m m free variables count the number of minimum cardinality diagnoses and minimum cardinality SddModelCount min_count sdd_model_count min_diagnosis m SddLiteral min_card sdd_minimum_cardinality min_diagnosis printf sdd model count PRImcS n count printf sdd model count min PRImcS n min_count printf sdd cardinality 4 PRI1itS n min_card SANE SDDS printf saving sdd and dot n sdd_save output circuit kb sdd delta sdd_save output diagnosis sdd diagnosis sdd_save output diagnosis min sdd min_diagnosis sdd_save_as_dot output circuit kb dot delta sdd_save_as_dot output diagnosis dot diagnosis sdd_save_as_dot output diagnosis min dot min_diagnosis 13 CLEAN UP sdd_manager_free m return 0 14 B Code Sample With Garbage Collect
15. have the three functions SddNode sdd_manager_true const SddManager manager SddNode sdd_manager_false const SddManager manager SddNode sdd_manager_literal const SddLiteral literal SddManager manager We next illustrate how we can use the SDDs returned by these functions to create more complex SDDs 5 3 Constructing SDDs from Elementary SDDs Our goal here is to construct an SDD representing the following knowledge base faulty gt A lt 7B Az faulty As B V B afaulty gt Bs C faulty BSC v Ac We can construct each of the four sentences from elementary SDDs one at a time We can then compose these four sentences together giving us an SDD for the knowledge base A We start with a vacuous knowledge base represented by a true SDD SddNodex delta sdd_manager_true manager Using the following functions we can conjoin two SDDs disjoin two SDDs or negate an SDD SddNode sdd_conjoin SddNode node1 SddNode node2 SddManager manager SddNode sdd_disjoin SddNode node1 SddNode node2 SddManager manager SddNode sdd_negate SddNode node SddManager manager Using these functions as primitives we can create our own functions that perform other operations on SDDs For example given an SDD representing a function a and an SDD representing a function 8 we can construct an SDD representing the sentence a 8 which is logically equivalent to sa V 2 SddNode sdd_imply SddN
16. he function sdd_manager_create initializes an SDD manager that can perform automatic garbage collection and SDD minimization by default For certain applications however the user may want to have control on when garbage collection and minimization are invoked The SDD library includes support for this by providing primitives for manual garbage collection and SDD minimization e vtrees and vtree search A vtree is a full binary tree with its leaves labeled with variables Every SDD manager has a vtree associated with it which also determines the size and structure of its SDDs The SDD library includes functions for specifying these vtrees It also includes functions which allow the user to search for good vtrees i e ones that try to minimize the size of corresponding SDDs The SDD package comes with its own algorithm for vtree search The source code of this algorithm is distributed with the package Acknowledgements Special thanks to the members of the Automated Reasoning Group at UCLA and in particular to Guy Van den Broeck for many helpful suggestions References 1 A Darwiche SDD A new canonical representation of propositional knowledge bases in Proceedings of the 22nd International Joint Conference on Artificial Intelligence IJCAI pp 819 826 2011 2 Y Xue A Choi and A Darwiche Basing decisions on sentences in decision diagrams in Proceedings of the 26th Conference on Artificial Intelligence AAAI pp
17. in tmp delta alpha m sdd_ref delta m sdd_deref tmp m sdd_deref alpha m faulty1 gt A lt gt B v B alpha sdd_equiv sdd_manager_literal A m sdd_manager_literal B m m sdd_ref alpha m alpha sdd_disjoin tmp alpha sdd_manager_literal B m m sdd_ref alpha m sdd_deref tmp m alpha sdd_imply sdd_manager_literal faulty1 m tmp alpha m 15 sdd_ref alpha m sdd_deref tmp m delta sdd_conjoin tmp delta alpha m sdd_ref delta m sdd_deref tmp m sdd_deref alpha m faulty2 gt B lt gt C alpha sdd_equiv sdd_manager_literal B m sdd_manager_literal C m m sdd_ref alpha m alpha sdd_imply sdd_manager_literal faulty2 m tmp alpha m sdd_ref alpha m sdd_deref tmp m delta sdd_conjoin tmp delta alpha m sdd_ref delta m sdd_deref tmp m sdd_deref alpha m faulty2 gt B lt gt C v C alpha sdd_equiv sdd_manager_literal B m sdd_manager_literal C m m sdd_ref alpha m alpha sdd_disjoin tmp alpha sdd_manager_literal C m m sdd_ref alpha m sdd_deref tmp m alpha sdd_imply sdd_manager_literal faulty2 m tmp alpha m sdd_ref alpha m sdd_deref tmp m delta sdd_conjoin tmp delta alpha m sdd_ref delta m sdd_deref tmp m sdd_deref alpha m 1 PERFORM QUERY int variables SddLiteral health_vars 2 health_vars_count missing_health_vars make obse
18. ion Enabled include lt stdio h gt include lt stdlib h gt include sddapi h returns an SDD node representing node1 gt node2 SddNode sdd_imply SddNode node1 SddNode node2 SddManager manager SddNode neg_node1 sdd_negate node1 manager sdd_ref neg_nodel manager SddNode alpha sdd_disjoin neg_nodel node2 manager sdd_deref neg_nodel manager return alpha returns an SDD node representing node1 lt gt node2 SddNode sdd_equiv SddNode node1 SddNode node2 SddManager manager SddNode imply1 sdd_imply nodel node2 manager sdd_ref imply1 manager SddNode imply2 sdd_imply node2 node1 manager sdd_ref imply2 manager SddNode alpha sdd_conjoin imply1 imply2 manager sdd_deref imply1 manager sdd_deref imply2 manager return alpha int main int argc char argv set up vtree and manager SddLiteral var_count 5 int auto_gc_and_minimize 1 SddManager m sdd_manager_create var_count auto_gc_and_minimize SddLiteral A 1 B 2 C 3 faulty1 4 faulty2 5 SddNode delta sdd_manager_true m SddNode alpha SddNode tmp CONSTRUCT KNOWLEDGE BASE faulty1 gt A lt gt B alpha sdd_equiv sdd_manager_literal A m sdd_manager_literal B m m sdd_ref alpha m alpha sdd_imply sdd_manager_literal faulty1 m tmp alpha m sdd_ref alpha m sdd_deref tmp m delta sdd_conjo
19. lib including the library file Libsdd a Compile the code using the command gcc 02 std c99 circuit c Iinclude Llib lsdd lm o circuit Executing the command circuit will then run the program The sample program outputs dot files in an output sub directory which must also exist in the current directory These files can be converted to graphs using the GraphViz dot program 4 Diagnosing Failures in Digital Circuits Consider Figure 2 which depicts a simple digital circuit consisting of two inverters labeled 1 and 2 and three wires labeled A B and C We can specify a knowledge base modeling this digital circuit using propositional logic faulty A lt s 7B faulty As B V B A rfaulty gt BSs C faulty BSC v Ac The knowledge base A is composed of four sentences two sentences for each inverter The first sentence specifies the normal operating behavior of an inverter the output of an inverter is the complement of its input The second sentence specifies the behavior of an inverter when it is faulty either it behaves as a buffer the output value is the same as the input i e A B or it behaves as if it is fixed to low i e B Variables faulty and faulty are called health variables and a term over all health variables is called a health state For example faulty A faulty is a health state where inverter 1 is faulty and inverter 2 is healthy Given an abnormal observation about the system e g
20. m m alpha sdd_disjoin alpha sdd_manager_literal B m m alpha sdd_imply sdd_manager_literal faulty1 m alpha m delta sdd_conjoin delta alpha m faulty2 gt B lt gt C alpha sdd_equiv sdd_manager_literal B m sdd_manager_literal C m m alpha sdd_imply sdd_manager_literal faulty2 m alpha m delta sdd_conjoin delta alpha m faulty2 gt B lt gt C v C alpha sdd_equiv sdd_manager_literal B m sdd_manager_literal C m m alpha sdd_disjoin alpha sdd_manager_literal C m m alpha sdd_imply sdd_manager_literal faulty2 m alpha m delta sdd_conjoin delta alpha m 1 PERFORM QUERY 12 int variables SddLiteral health_vars 2 health_vars_count missing_health_vars make observations delta sdd_condition A delta m delta sdd_condition C delta m check if observations are normal SddNode gamma gamma sdd_condition faulty1 delta m gamma sdd_condition faulty2 gamma m int is_abnormal sdd_node_is_false gamma printf observations normal s n is_abnormal abnormal normal project onto faults SddNode diagnosis sdd_exists B delta m diagnosis no longer depends on variables A B or C count the number of diagnoses SddModelCount count sdd_model_count diagnosis m adjust for missing faults variables sdd_variables diagnosis m health_vars_count variables
21. ned by function sdd_conjoin delta sdd_conjoin delta alpha m sdd_ref delta m sdd_deref alpha m Here we have dereferenced the input alpha which we will again no longer need Note that we do not need to dereference the input delta since it corresponds to the SDD for true which never needs to be dereferenced Consider the following code snippet from the previous section where we constructed the second sentence of our knowledge base A alpha sdd_equiv sdd_manager_literal A m sdd_manager_literal B m m alpha sdd_disjoin alpha sdd_manager_literal B m m alpha sdd_imply sdd_manager_literal faulty1 m alpha m delta sdd_conjoin delta alpha m we can also systematically augment this snippet line by line in a similar way alpha sdd_equiv sdd_manager_literal A m sdd_manager_literal B m m sdd_ref alpha m alpha sdd_disjoin tmp alpha sdd_manager_literal B m m sdd_ref alpha m sdd_deref tmp m alpha sdd_imply sdd_manager_literal faulty1 m tmp alpha m sdd_ref alpha m sdd_deref tmp m delta sdd_conjoin tmp delta alpha m sdd_ref delta m sdd_deref tmp m sdd_deref alpha m Appendix A contains the complete circuit diagnosis example where we have systematically incorporated referencing and dereferencing in the same way reference any SDD returned by a call to the library or a call to a function that calls the library and der
22. nowledge base A SddNode delta sdd_manager_true m SddNode alpha alpha sdd_equiv sdd_manager_literal A m sdd_manager_literal B m m alpha sdd_imply sdd_manager_literal faulty1 m alpha m delta sdd_conjoin delta alpha m For each function that returns an SDD we will immediately reference the returned SDD Moreover after we obtain that SDD we will dereference any SDD used to construct it if we know that it will be the last time we need to use that SDD It is not necessary however to reference or dereference elementary SDDs i e the SDDs for true false and for literals These SDDs will never be garbage collected Moreover referencing and dereferencing them has no effect First we reference the SDD returned by the function sdd_equiv alpha sdd_equiv sdd_manager_literal A m sdd_manager_literal B m m sdd_ref alpha m We do not need to reference or dereference any of the input SDDs here as they are SDDs for literals Next we want to reference the SDD returned by the function sdd_imply However we will want to dereference the input SDD that was returned by sdd_equiv as we will no longer need it after calling sdd_imply SddNode tmp alpha sdd_imply sdd_manager_literal faulty1 m tmp alpha m sdd_ref alpha m sdd_deref tmp m Here we have used a temporary pointer tmp to save the address of the input SDD alpha Finally we reference the SDD retur
23. ode node1 SddNode node2 SddManager manager return sdd_disjoin sdd_negate nodel manager node2 manager Using the above function as a primitive we can construct an SDD representing the sentence a 8 which is logically equivalent to a gt 8 A 8 gt a SddNode sdd_equiv SddNode node1 SddNode node2 SddManager manager return sdd_conjoin sdd_imply node1 node2 manager sdd_imply node2 nodei1 manager manager We are now prepared to construct an SDD for our knowledge base A Let us first construct an SDD for the sentence faulty A B We can first construct the SDD for the sub sentence A 7B using the SDDs for literals A and B We then take the resulting SDD and combine it with the SDD for literal faulty as we do in the following code snippet SddNode alpha alpha sdd_equiv sdd_manager_literal A m sdd_manager_literal B m m alpha sdd_imply sdd_manager_literal faulty1 m alpha m where we have used the abbreviated name m for the SDD manager We then conjoin this sentence with the SDD for our knowledge base which we initialized to true delta sdd_conjoin delta alpha m We can construct SDDs for each sentence similarly conjoining each with our knowledge base For example the following code snippet constructs an SDD for the sentence faulty gt A B V B and conjoins it with the SDD for our knowledge base alpha
24. rovides a brief introduction to the SDD library using a small set of library functions which are sufficient to do the following Construct complex SDDs from elementary SDDs corresponding to constants or literals Manipulate and query SDDs Read write SDDs from to a file Visualize SDDs as in Figure 1 An advanced manual is available for those users who want a richer interface with access to more of the machinery underlying the SDD library 2 SDDs Consider again Figure 1 which contains a graphical depiction of a Sentential Decision Diagram SDD along with the Boolean function that the SDD represents There are two types of nodes here circle nodes are called decision nodes and paired boxes p s are called elements A decision node represents a disjunction of its child elements and a paired box p s represents a conjunction p A s where a box can contain either a pointer to a decision node a constant T for true and L for false or a literal X or X Each node and paired box then corresponds to some sub function of the SDD with the root node representing the function itself For example in the bottom row of paired boxes we have from left to right the corresponding functions DAC D A L L BA 7A etc In the lower row of circular nodes we have from left to right the corresponding functions DAC V ADA L CAD BAAA V ABAL 7AAAB BA A V ABAL AAB The root node
25. rvations and project onto faults delta sdd_condition A tmp delta m sdd_ref delta m sdd_deref tmp m delta sdd_condition C tmp delta m sdd_ref delta m sdd_deref tmp m check if observations are normal SddNode gamma gamma sdd_condition faulty1 delta m sdd_ref gamma m gamma sdd_condition faulty2 tmp gamma m sdd_ref gamma m sdd_deref tmp m int is_abnormal sdd_node_is_false gamma printf observations normal s n is_abnormal abnormal normal sdd_deref gamma m project onto faults SddNode diagnosis sdd_exists B delta m sdd_ref diagnosis m diagnosis no longer depends on variables A B or C count the number of diagnoses SddModelCount count sdd_model_count diagnosis m adjust for missing faults variables sdd_variables diagnosis m health_vars_count variables faulty1 variables faulty2 missing_health_vars health_vars health_vars_count count lt lt missing_health_vars multiply by 2 missing_health_vars free variables 16 find minimum cardinality diagnoses SddNode min_diagnosis sdd_minimize_cardinality diagnosis m sdd_ref min_diagnosis m variables sdd_variables min_diagnosis m adjust for missing faults if variables faulty1 0 min_diagnosis sdd_conjoin tmp min_diagnosis sdd_manager_literal faulty1 m m sdd_ref min_diagnosis m sdd_deref tmp m if variables
26. s var_count We also disable or enable automatic garbage collection and SDD minimization In our example we have created a new SDD manager declaring that we want to have 5 variables We have further disabled automatic garbage collection and SDD minimization Some degree of memory management is integral for the construction of SDDs in practical applications In the SDD library memory management is based on garbage collection with reference counting We will however delay this discussion until Section 6 to simplify our introduction to the SDD library This is why we have disabled automatic garbage collection and SDD minimization for now 5 2 Variables Literals and Elementary SDDs In the SDD library variables are referred to by indices Since our manager has five variables their indices will be 1 2 3 4 and 5 Literals are referred to by signed indices For example the third variable has a positive literal 3 and a negative literal 3 The variables of our diagnosis example are A B C faulty and faulty In the code snippet below we associate each one of these variables with an index from 1 to 5 SddLiteral A 1 B 2 C 3 faultyl 4 faulty2 5 Here SddLiteral is an integer type that is defined by the SDD library in the header file sddapi h This type is used to specify literals variables or their negation The SDD manager maintains a unique SDD for each constant and literal To access these elementary SDDs we
27. t to test if the sentence A A A A C A faulty A faulty is consistent or inconsistent SddNode gamma gamma sdd_condition faulty1 delta m gamma sdd_condition faulty2 gamma m int is_abnormal sdd_node_is_false gamma If the resulting SDD gamma is false then our observations are abnormal otherwise they are normal We can test whether a given SDD is false or true using the following functions int sdd_node_is_false SddNode node int sdd_node_is_true SddNode node These functions return 1 if the given SDD node corresponds to the one being queried and 0 otherwise Next to compute our diagnoses we project our SDD onto the health variables faulty and faulty In particular we existentially quantify out all non health variables which is just variable B in this case SddNode diagnosis sdd_exists B delta m Given a knowledge base A and a variable X existential quantification is more formally defined as IX A A X V A X Similarly universal quantification is defined as VX A A X A A X The corresponding functions are used to existentially and universally quantify out a variable from an SDD SddNode sdd_exists SddLiteral var SddNode node SddManager manager SddNode sdd_forall SddLiteral var SddNode node SddManager manager In our diagnosis example we obtain the following SDD representing our diagnoses afaulty faulty2 faulty
Download Pdf Manuals
Related Search