SDD Advanced-User Manual Version 1.1
Contents
1. Deactivates automatic garbage collection and automatic SDD minimization void sdd_manager_set_minimize_function SddVtreeSearchFunc func SddManager manager Instructs the SDD library to use the function func instead of the built in function sdd_vtree minimize during automatic SDD minimization This allows the user to define their own vtree search algorithm to be used during automatic SDD minimization The function func must behave similarly to sdd_vtree_ minimize The type SddVtreeSearchFunc is defined as Vtree func Vtree vtree SddManager manager void sdd_manager_unset_minimize_function SddManager manager Reverts back to sdd_vtree minimize as the vtree search algorithm for automatic SDD minimization 5 1 4 Size and Count SddSize sdd_manager_size const SddManager manager SddSize sdd_manager_live_size const SddManager manager SddSize sdd_manager_dead_size const SddManager manager SddSize sdd_manager_count const SddManager manager SddSize sdd_manager_live_count const SddManager manager SddSize sdd_manager_dead_count const SddManager manager Returns the size or node count of all SDD nodes in the manager For each size and count three versions are provided live dead and total live dead 5 1 5 Misc Functions void sdd_manager_print SddManager manager Prints various statistics that are collected by an SDD manager SddLiteral sdd_manager_var_count SddManager manager Returns the number2. the subs are distinct jh A B 5 1 5 AA AA Lb WN C D A B A B C D a right linear b left linear c balanced Figure 2 Different vtrees over the variables A B C and D A right linear vtree is one in which each left child is a leaf A left linear vtree is one in which each right child is a leaf An SDD can be constructed for a Boolean function as follows We first split the function variables into disjoint sets X and Y and then compute its unique compressed X Y partition The process is repeated recursively for each of the resulting primes and subs until reaching constants true and false or literals These are called terminal SDDs and correspond to the base cases of this recursive process Note that this process can yield different SDDs depending on how we split the variables of each considered function These splitting choices however can be fixed using the notion of a vtree leading to canonical SDDs 1 2 Vtrees A vtree stands for a variable vtree It is a full binary tree with its leaves labeled with the variables of a Boolean function Figure 2 depicts a few vtrees over variables 4 B C and D Suppose now that f is a non trivial Boolean function and let v be the lowest vtree node that includes the variables that function f depends on We will say in this case that function f is normalized for vtree node v For an example the function f B A D is normalized for node v 3 in Figure 2 a It is also norma
3. vtree sdd_vtree_read input opt swap vtree SddManager manager sdd_manager_new vtree initialize_manager_search_state manager done only once printf reading sdd from file n SddNode alpha sdd_read input opt swap sdd manager printf sdd size zu n sdd_size alpha ref perform the minimization and then de ref sdd_ref alpha manager printf minimizing sdd size minimize_sdd manager printf done lWn printf sdd size zu n sdd_size alpha sdd_deref alpha manager augment the SDD printf augmenting sdd n SddNodex beta sdd_disjoin sdd_manager_literal 4 manager sdd_manager_literal 5 manager manager beta sdd_conjoin alpha beta manager printf sdd size zu n sdd_size beta ref perform the minimization again on new SDD and then de ref sdd_ref beta manager printf minimizing sdd 26 minimize_sdd manager printf done lWn printf sdd size zu n sdd_size beta sdd_deref beta manager free_manager_search_state manager sdd_manager_free manager sdd_vtree_free vtree return 0 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 Arthur Choi and Adnan Darwiche Dynamic minimization of sentential decision diagrams In Proceedings of the 27th AAAI Con
4. Ge a eee pa Ae ee 5 4 Manual Garbage Collection ee 5 5 Manual SDD Minimization 2 0 0 00 000 02 ee 5 6 Weighted Model Counting 6 CNF DNF to SDD Compiler 7 Code Samples Gl A Gompiling sai A Aa ok VAL Pe Rh eA Bo A ee ee eke ato th ee ee 7 2 Example 1 Constructing a Simple SDD 0 200 000 0000 7 3 Example 2 Garbage Collecting an SDD o o e 7 4 Example 3 Minimizing an SDD e 7 5 Example 4 Rotating a Vtree Node a 7 6 Example 5 Swapping a Vtree Node with Limits e e 7 7 Example 6 Minimizing an SDD From Source 2 2 000000 0000002 References A License B SDD API 20 20 21 22 23 24 26 27 28 29 1 5 1 2 4 6 y B A D C D C DL BIA OBIL B A BL a A vtree b A graphical depiction of an SDD Figure 1 A vtree and a corresponding SDD for the Boolean function f AA B V BAC V CAD 1 Introduction The Sentential Decision Diagram SDD is a recently proposed representation of Boolean functions 2 5 1 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 b depicts an example SDD and the Boolean function it represents This manual
5. SDD library however SDDs are constructed in a bottom up fashion For example to construct an SDD for the function f AA B V BA C v CAD we first retrieve terminal SDDs for the literals A B C and D We then conjoin the terminal SDD for literal A with the one for literal B to obtain an SDD for the term AA B The process is repeated to obtain SDDs for the terms BAC and CA D The resulting SDDs are then disjoined to obtain an SDD for the whole function The SDD library provides primitives for retrieving terminal SDDs It also provides primitives for conjoining disjoining and negating SDDs These primitives are explained in Section 5 A code sample is given in Section 7 that uses these primitives to construct an SDD for this particular example 2 7 Canonicity The SDDs we discussed are canonical and have been called trimmed and compressed SDDs in 2 Another type of canonical SDDs was identified in 2 called normalized SDDs The SDD library supports only trimmed and compressed SDDs 3 Garbage Collection Suppose that two SDDs a and are conjoined to yield a third SDD y Given how the conjoin and other SDD operations work this process may yield additional SDD nodes that are not part of either a 8 or y The SDD library keeps these auxiliary SDD nodes in memory as they correspond to the results of intermediate computations that can be reused when performing further conjoin and disjoin operations While this strategy improves performance i
6. array var_order The contents of array var_order must be a permutation of the integers from 1 to var_count The type of a vtree may be right right linear left left linear vertical or balanced void sdd_vtree_free Vtree vtree Frees the memory of a vtree 14 5 3 2 Size and Count SddSize sdd_vtree_size const Vtree vtree SddSize sdd_vtree_live_size const Vtree vtree SddSize sdd_vtree_dead_size const Vtree vtree SddSize sdd_vtree_count const Vtree vtree SddSize sdd_vtree_live_count const Vtree vtree SddSize sdd_vtree_dead_count const Vtree vtree Returns the size or node count of all SDD nodes in the vtree see Section 2 5 For each size and count three versions are provided live dead and total live dead SddSize sdd_vtree_size_at const Vtree vtree SddSize sdd_vtree_live_size_at const Vtree vtree SddSize sdd_vtree_dead_size_at const Vtree vtree SddSize sdd_vtree_count_at const Vtree vtree SddSize sdd_vtree_live_count_at const Vtree vtree SddSize sdd_vtree_dead_count_at const Vtree vtree Returns the size or node count of all SDD nodes normalized for a vtree node see Section 2 5 For each size and count three versions are provided live dead and total live dead For example sdd_vtree_size vtree returns the sum of sdd_vtree_size_at v where v ranges over all nodes of vtree 5 3 3 File I O Vtrees can be read from and written to file When a vtree is saved to file a
7. at or below 1 2x s Hence before specifying a size limit one must declare the vtree v and initial size s that will be used for interpreting this limit Right rotation and swap take a third limit These operations compute a cartesian product which grow monotonically in size In what may only be pathological cases the size of this cartesian product may be exponentially large 5 The user can provide a limit on the size of this cartesian product A code sample is provided in Section 7 for illustrating the use of these limits 4 4 Roots Consider the vtree on the left of Figure 4 a The root of this vtree is x Yet when we right rotate x the new root of this vtree becomes w More generally when applying rotation operations to a vtree fragment the root of that fragment may change One can in principle keep track of the various rotations applied and then compute the new root of the vtree fragment based on which rotations were applied The SDD library facilitates this process by providing a primitive that recovers the new root of a vtree fragment This primitive returns the memory location that stores the pointer to the vtree root By recovering the content of this location the user will then have access to the current root which may have changed due to rotations This primitive is discussed in Section 5 It is also illustrated in one of the code samples in Section 7 4 5 Search and Minimization The SDD library provides a primitive for reducing
8. description of its file format is printed as a header void sdd_vtree_save const char fname Vtree vtree Saves a vtree to file Vtree sdd_vtree_read const char filename Reads a vtree from file void sdd_vtree_save_as_dot const char fname Vtree vtree Saves a vtree to file formatted for use with Graphviz dot to produce graphs like the one in Figure 1 a 5 3 4 Navigation int sdd_vtree_is_leaf const Vtree vtree Returns 1 if vtree is a leaf node and 0 otherwise Vtree sdd_vtree_left const Vtree vtree Returns the left child of a vtree node returns NULL if the vtree is a leaf node Vtree sdd_vtree_right const Vtree vtree Returns the right child of a vtree node returns NULL if the vtree is a leaf node Vtree sdd_vtree_parent const Vtree vtree Returns the parent of a vtree node return NULL if the vtree is a root node 15 5 3 5 Edit Operations int sdd_vtree_rotate_left Vtree vtree SddManager manager SddSize time_limit float size_limit Rotates a vtree node left given time and size limits A limit of 0 deactivates the limit Returns 1 if the operation succeeds and 0 otherwise i e limits exceeded This operation assumes no dead SDD nodes inside or above vtree and does not introduce any new dead SDD nodes int sdd_vtree_rotate_right Vtree vtree SddManager manager SddSize time_limit float size_limit int max_cartesian_product Rotates a vtree node right given
9. in the manager that satisfies the SDD The weighted model count of a literal is the sum of weights attained by its models that are also models of the given SDD The probability of a literal is the ratio of its weighted model count over the one for the given SDD To facilitate the computation of weighted model counts with respect to changing literal weights a WMC manager is created for the given SDD This manager stores the weights of literals allowing one to change them and to recompute the corresponding weighted model count each time the weights change WmcManager wmc_manager_new SddNode node int log_mode SddManager manager Creates a WMC manager for the SDD rooted at node and initializes literal weights When log mode 0 all computations done by the manager will be in natural log space Literal weights are initialized to 0 in log mode and to 1 otherwise A number of functions are given below for passing values to or recovering values from a WMC manager In log mode all these values are in natural logs Finally a WMC manager may become invalid if garbage collection or SDD minimization takes place void wmc_manager_free WmcManager wmc_manager Frees the memory of the WMC manager 5To avoid invalidating a WMC manager the user should refrain from performing the SDD operations of Section 5 2 1 when auto garbage collection and SDD minimization is active 18 void wmc_set_literal_weight const SddLiteral literal const
10. m elements the array will be of size 2m with primes appearing at locations 0 2 2m 2 and their corresponding subs appearing at locations 1 3 2m 1 Assumes that sdd_node_is_decision node returns 1 Moreover the returned array should not be freed void sdd_node_set_bit int bit SddNode node Sets the bit flag for an SDD node Bit flags are initialized to 0 and as a general rule they should be reset to O when flags are not being used int sdd_node_bit SddNode node Returns the bit flag of an SDD node 13 5 2 5 Misc Functions Vtree sdd_vtree_of SddNode node Returns the vtree that an SDD node is normalized for Every SDD node has an ID When an SDD node is garbage collected its structure is not freed but inserted into a gc list Moreover this structure may be reused later by another newly created SDD node which will have its own new ID SddSize sdd_id SddNode node Returns the ID of SDD node This function may be helpful for debugging int sdd_garbage_collected SddNode node SddSize id Returns 1 if the SDD node with the given ID has been garbage collected returns 0 otherwise This function may be helpful for debugging SddNode sdd_copy SddNode node SddManager dest_manager Returns a copy of an SDD with respect to a new manager dest_manager The destination manager and the manager associated with the SDD to be copied must have copies of the same vtree SddNode sdd_rename_variables SddN
11. manager manager alpha sdd_conjoin alpha sdd_manager_literal 3 manager manager alpha sdd_conjoin alpha sdd_manager_literal 4 manager manager to perform a rotate we need the manager s vtree Vtree manager_vtree sdd_manager_vtree manager Vtree manager_vtree_right sdd_vtree_right manager_vtree obtain the manager s pointer to the root Vtree root_location sdd_vtree_location manager_vtree manager printf saving vtree amp sdd n sdd_vtree_save_as_dot output before rotate vtree dot manager_vtree sdd_save_as_dot output before rotate sdd dot alpha ref alpha no dead nodes when rotating sdd_ref alpha manager printf left rotating int succeeded sdd_vtree_rotate_left manager_vtree_right manager 0 0 0 printf s n succeeded succeeded did not succeed deref alpha since ref s are no longer needed sdd_deref alpha manager the root changed after rotation so get the manager s vtree again this time using root_location manager_vtree root_location printf saving vtree sdd n sdd_vtree_save_as_dot output after rotate vtree dot manager_vtree sdd_save_as_dot output after rotate sdd dot alpha sdd_vtree_free vtree sdd_manager_free manager return 0 7 6 Example 5 Swapping a Vtree Node with Limits include lt stdio h gt include lt stdlib h gt include sddapi h int main int argc char a
12. s SDD This function calls sdd_vtree_search on the manager s vtree The following functions can be used to change the settings that control the vtree search algorithm applies for both manual and automatic SDD minimization In order the default settings are 25000000 25000000 25000000 1 2 1 2 1 2 1024 1024 and 1 0 void sdd_manager_set_lr_time_limit SddSize time_limit SddManager manager void sdd_manager_set_rr_time_limit SddSize time_limit SddManager manager void sdd_manager_set_sw_time_limit SddSize time_limit SddManager manager void sdd_manager_set_lr_size_limit float size_limit SddManager manager void sdd_manager_set_rr_size_limit float size_limit SddManager manager void sdd_manager_set_sw_size_limit float size_limit SddManager manager void sdd_manager_set_rr_cartesian_product_limit int cartesian_product_limit SddManager manager void sdd_manager_set_sw_cartesian_product_limit int cartesian_product_limit SddManager manager void sdd_manager_set_convergence_threshold float threshold SddManager manager 5 6 Weighted Model Counting Weighted model counting WMC is performed with respect to a given SDD and literal weights and is based on the following definitions The weight of a variable instantiation is the product of weights assigned to its literals The weighted model count of the SDD is the sum of weights attained by its models Here a model is an instantiation of all variables
13. starts by going over some of the basic concepts underlying Sentential Decision Diagrams These concepts are essential for getting started with the SDD library which is discussed in Section 5 The source code distributed with the SDD package is then discussed in Section 6 Smaller code samples are also provided in Section 7 to illustrate some of the SDD library features 1 1 Compressed Partitions SDDs are based on a new type of Boolean function decomposition which we start with Consider a Boolean function f and suppose that we split its variables into two disjoint sets X and Y We can always decompose function f as follows MAIN vv pn X A 5n while satisfying the following two conditions Partition The functions p X are mutually exclusive exhaustive and non false Compression The functions s Y are distinct This kind of a decomposition always exists and is unique for a particular split of the function variables This decomposition is called a compressed X Y partition of the function f where the functions p X are called primes and the functions s Y are called subs 2 For an example consider the Boolean function f AAB V BAC V CAD 1 By splitting the function variables into X A B and Y C D we get the following decomposition ANB A true V GAABA C Vv AB ACAD 2 Sas NY SS A prime sub prime sub prime sub The primes are mutually exclusive exhaustive and non false Moreover
14. the node The number of dereferences to a node cannot be larger than the number of its references except for terminal SDD nodes for which referencing and dereferencing has no effect void sdd_manager_garbage_collect SddManager manager Performs a global garbage collection Claims all dead SDD nodes in the manager int sdd_manager_garbage_collect_if float dead_node_threshold SddManager manager Performs a global garbage collection if the number of dead SDD nodes over the number of all SDD nodes in the manager exceeds dead_node_threshold Returns 1 if garbage collection is performed 0 otherwise void sdd_vtree_garbage_collect Vtree vtree SddManager manager Performs local garbage collection Claims all dead SDD nodes inside or above vtree int sdd_vtree_garbage_collect_if float dead_node_threshold Vtree vtree SddManager manager Performs local garbage collection if the number of dead SDD nodes over the number of all SDD nodes in the vtree exceeds dead_node_threshold Returns 1 if garbage collection is performed 0 otherwise 17 5 5 Manual SDD Minimization Vtree sdd_vtree_minimize Vtree vtree SddManager manager Performs local garbage collection on vtree and then tries to minimize the size of SDD of vtree by searching for a different vtree Returns the root of found vtree void sdd_manager_minimize SddManager manager Performs global garbage collection and then tries to minimize the size of manager
15. the size of existing SDDs which works by searching for a better vtree i e one that tries to minimize the SDD size Similar to garbage collection SDD minimization can be invoked manually by the user or automatically by the SDD library Automatic garbage collection and automatic SDD minimization are activated or deactivated simultane ously Manual SDD minimization will also invoked the garbage collector so the SDD node referencing rules of manual garbage collection apply when invoking SDD minimization manually The SDD package is distributed with the source code for the vtree search algorithm used in SDD min imization This algorithm searches the space of vtrees locally using the rotation and swap operations as described in 1 The SDD package is also distributed with source code for compiling CNFs and DNFs into SDDs This compiler makes use of the vtree search algorithm and is discussed in Section 6 5 SDD API This section discusses the API of the SDD library Section 7 provides a number of code samples which provide concrete illustrations of using the API 5 1 Managers The creation and manipulation of SDDs are maintained by an SDD manager The use of an SDD manager is analogous to the use of managers in OBDD packages such as CUDD 4 For a discussion on the design and implementation of such systems see 3 To declare an SDD manager one provides an initial vtree By declaring an initial vtree we also declare an initial number of
16. v 2 The SDD library provides primitives for both types of garbage collection which are discussed in Section 5 3 4 When to Reference Nodes During automatic garbage collection or before invoking the garbage collector manually the user must make sure that all SDD nodes of interest are referenced If automatic garbage collection is not being used and the user does not intend to invoke the garbage collector a rare situation then no referencing is ever needed If automatic garbage collection is not being used a more realistic situation however is for the user to call the garbage collector at specific places in their application allowing them to selectively decide what SDD nodes to reference and when Typically one invokes the garbage collector manually when the number of dead nodes grows too large The SDD library facilitates this process by providing primitives for conditional garbage collection allowing the user to invoke garbage collection when the percentage of dead SDD nodes exceeds a certain threshold During automatic garbage collection the SDD library makes its own decisions on when to invoke the garbage collector again based on the number of dead nodes 4 More on Vtrees We now provide further details on the support provided by the SDD library for vtrees 4 1 Orders Each vtree induces a total order on its variables which is obtained by a left to right traversal of the vtree nodes For example all vtrees in Figure 2 induce th
17. variables See the section on creating vtrees for a few ways to specify an initial vtree Note that variables are referred to by an index If there are n variables in an SDD manager then the variables are referred to as 1 n Literals are referred to by signed indices For example given the i th variable we refer to its positive literal by 7 and its negative literal by 1 5 1 1 Creating Managers SddManager sdd_manager_new Vtree vtree Creates a new SDD manager given a vtree The manager copies the input vtree Any manipulations performed by the manager are done on its own copy and does not affect the input vtree SddManager sdd_manager_create SddLiteral var_count int auto_gc_and_minimize Creates a new SDD manager using a balanced vtree over the given number of variables Automatic garbage collection and automatic SDD minimization are activated in the created manager when auto_gc_and_minimize is not 0 void sdd_manager_free SddManager manager Frees the memory of an SDD manager created by new_sdd_manager including all SDD nodes created using that manager The following four functions add a new variable with index n 1 to the manager where n is the current number of variables in the manager void sdd_manager_add_var_before_first SddManager manager void sdd_manager_add_var_after_last SddManager manager Let v be the leftmost rightmost leaf node in the vtree A new leaf node labeled with variable n 1 is crea
18. 1 3 printf modifying vtree swap node 5 limit growth by 1fx limit succeeded sdd_vtree_swap left_vtree manager 0 limit 0 printf s n succeeded succeeded did not succeed printf sdd size zu n sdd_size alpha deref alpha since ref s are no longer needed sdd_deref alpha manager sdd_vtree_free vtree sdd_manager_free manager return 0 25 7 7 Example 6 Minimizing an SDD From Source The code sample in Section 7 4 invokes the vtree search function from the SDD library This code sample invokes the source version of this function as provided in the SDD package for users who may be interested in modifying the search algorithm This code sample can be compiled using gcc 02 std c99 test c Iinclude Llib lsdd lm o test loc search c loc state c where loc is the directory containing the source files search c and state c of the search algorithm The main difference between this code sample and the one in Section 7 4 is the need to explicitly initialize and free the search state associated with a manager include lt stdio h gt include lt stdlib h gt include sddapi h include compiler h void initialize_manager_search_state SddManager manager void free_manager_search_state SddManager manager void minimize_sdd SddManager manager vtree_search sdd_manager_vtree manager manager int main int argc char argv set up vtree and manager Vtree
19. 6 5 3 7 Misc Functions int sdd_vtree_is_sub const Vtree vtreel const Vtree vtree2 Returns 1 if vtreel is a sub vtree of vtree2 and 0 otherwise Vtree sdd_vtree_lca Vtree vtreel Vtree vtree2 Vtree root Returns the lowest common ancestor lca of vtree nodes vtreel and vtree2 assuming that root is a common ancestor of these two nodes SddLiteral sdd_vtree_var_count const Vtree vtree Returns the number of variables contained in the vtree SddLiteral sdd_vtree_var const Vtree vtree Returns the variable associated with a vtree node if the vtree node is a leaf and returns 0 otherwise SddLiteral sdd_vtree_position const Vtree vtree Returns the position of a given vtree node in the vtree inorder Position indices start at 0 Vtree sdd_vtree_location Vtree vtree SddManager manager Returns the location of the pointer to the vtree root This location can be used to access the new root of the vtree which may have changed due to rotating some of the vtree nodes 5 4 Manual Garbage Collection SddRefCount sdd_ref_count SddNode node Returns the reference count of an SDD node The reference count of a terminal SDD is 0 terminal SDDs are always live SddNode sdd_ref SddNode node SddManager manager References an SDD node if it is not a terminal node Returns the node SddNode sdd_deref SddNode node SddManager manager Dereferences an SDD node if it is not a terminal node Returns
20. SDD Advanced 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 allows users to construct manipulate and optimize SDDs This manual describes the SDD package which is distributed as a C library called libsdd together with source code for compiling CNFs and DNFs into SDDs and for minimizing the SDD size The license terms for the SDD package are given at the end of this manual Contents 1 Introduction Tl Compr ess d Partitions 2 4 20 e AR A A A ad BA Bae a LEDO MELON Jo ndo ec Bey Se e a Gee a A A a A a Sy i R S eee ds 2 Sentential Decision Diagrams SDDs 2 1 Graphical Depiction 10 p o oe ado e e Boa ene kh Be yatta See ghee ee ee 22 Size and COM e a A 4 aoe tee a e 2 3 shared SDDS ke ane o a See ee oo eS Bae dea Bee we to a be ke ak ee 2 4 Normalization sy lt lt 10 a ES a A A E A A A A 2 5 SDD and Vtree Nod s omo a a a a a a 2 6 Bottom up Construction of SDDs 0 0 0 0002 ee ee SA yrs 6 5 Bet ah one Ae E EN 3 Garbage Collection 3 1 Live and Dead Nodes cri i a aoier a rare t aa Ai a a antai g a a a aa a aa a a oE a e 3 2 Ref r nc Counts eis Lrs g so Te ed bE OE tAn alaa he A Vas e ar a 4 3 3 Automatic a
21. SddWmc weight WmcManager wmc_manager Sets the weight of a literal in the given WMC manager should pass the natural log of the weight in log mode SddWmc wmc_propagate WmcManager wmc_manager Returns the weighted model count of the SDD underlying the WMC manager using the current literal weights This function should be called each time the weights of literals are changed SddWmc wmc_zero_weight WmcManager wmc_manager Returns oo for log mode and 0 otherwise SddWmc wmc_one_weight WmcManager wmc_manager Returns 0 for log mode and 1 otherwise SddWmc wmc_literal_weight const SddLiteral literal const WmcManager wmc_manager Returns the weight of a literal SddWmc wmc_literal_derivative const SddLiteral literal const WmcManager wmc_manager Returns the partial derivative of the weighted model count with respect to the weight of literal The result returned by this function is meaningful only after having called wmc_propagate SddWmc wmc_literal_pr const SddLiteral literal const WmcManager wmc_manager Returns the probability of literal The result returned by this function is meaningful only after having called wmc_propagate 6 CNF DNF to SDD Compiler The SDD Package includes the SDD library libsdd a as well as two source codes for e A vtree search algorithm which corresponds to the one described in 1 with some refinements that tend to yield faster results but perhaps larger compilati
22. const SddWmc weight WmcManager wmc_manager SddWmc wmc_propagate WmcManager wmc_manager SddWmc wmc_zero_weight WmcManager wmc_manager SddWmc wmc_one_weight WmcManager wmc_manager SddWmc wmc_literal_weight const SddLiteral literal const WmcManager wmc_manager SddWmc wmc_literal_derivative const SddLiteral literal const WmcManager wmc_manager SddWmc wmc_literal_pr const SddLiteral literal const WmcManager wmc_manager 32
23. const Vtree vtree Vtree sdd_vtree_left const Vtree vtree Vtree sdd_vtree_right const Vtree vtree Vtree sdd_vtree_parent const Vtree vtree Edit Operations int sdd_vtree_rotate_left Vtree vtree SddManager manager SddSize time_limit float size_limit int sdd_vtree_rotate_right Vtree vtree SddManager manager SddSize time_limit float size_limit int max_cartesian_product int sdd_vtree_swap Vtree vtree SddManager manager SddSize time_limit float size_limit int max_cartesian_product void sdd_manager_set_size_limit_context Vtree vtree SddManager manager void sdd_manager_update_size_limit_context SddManager manager State int sdd_vtree_bit const Vtree vtree void sdd_vtree_set_bit int bit Vtree vtree void sdd_vtree_data Vtree vtree void sdd_vtree_set_data void data Vtree vtree void sdd_vtree_search_state Vtree vtree void sdd_vtree_set_search_state void search_state Vtree vtree Misc Functions int sdd_vtree_is_sub const Vtree vtreel const Vtree vtree2 Vtree sdd_vtree_lca Vtree vtreel Vtree vtree2 Vtree root SddLiteral sdd_vtree_var_count const Vtree vtree SddLiteral sdd_vtree_var const Vtree vtree 31 SddLiteral sdd_vtree_position const Vtree vtree Vtree x sdd_vtree_location Vtree vtree SddManager manager Manual Garbage Collection SddRefCount sdd_ref_count SddNode node SddNode sdd_ref SddNode node SddManager mana
24. ctor is based on reference counts In particular every decision SDD node n has a reference count whose value is the sum of two quantities a the number of uncanceled references made by the user to node n and b the number of live SDD nodes referencing node n as a prime or sub Hence a decision SDD node is live if and only if its reference count is greater than 0 The SDD library provides a primitive for accessing this reference count of an SDD node RRS KKM KL A A L 9 BRL gt B cC D PCL CID ha CID FAL a User referenced left root b User referenced left middle roots c User referenced all roots Figure 3 Double circles are live nodes and single circles are dead nodes 3 3 Automatic and Manual Garbage Collection The SDD library provides primitives for activating and deactivating automatic garbage collection The user can also invoke garbage collection manually at two levels globally and locally Global garbage collection will claim any dead SDD node Local garbage collection is applied to a vtree v and it will claim dead SDD nodes in vtree v and above vtree
25. d_minimum_cardinality SddNode node Returns the minimum cardinality of an SDD the smallest cardinality attained by any of its models SddNode sdd_minimize_cardinality SddNode node SddManager manager Returns the SDD whose models are the minimum cardinality models of the given SDD SddNode sdd_apply SddNode node1 SddNode node2 BoolOp op SddManager manager Returns the result of combining two SDDs where op can be CONJOIN 0 or DISJOIN 1 SddNode sdd_apply_in_vtree SddNode node1 SddNode node2 BoolOp op Vtreex vtree SddManager manager Same as sdd_apply but accepts a vtree The two SDD nodes passed as arguments must be inside vtree This operation can be more efficient than sdd_apply 12 5 2 2 Size and Count SddSize sdd_size SddNode node SddSize sdd_count SddNode node Returns the size or node count of an SDD rooted at node SddSize sdd_shared_size SddNode nodes SddSize count Returns the size of a shared SDD nodes contains the SDD roots and count is the number of roots 5 2 3 File I O SDDs can be read from and written to file When an SDD is saved to file a description of its file format is printed as a header void sdd_save const char fname SddNode node Saves an SDD to file Typically one also saves the corresponding vtree to file This allows one to read the SDD back using the same vtree SddNode sdd_read const char filename SddManager manager Reads an SDD from file T
26. e saves time it may eventually lead to exhausting memory To address this issue the SDD library provides a garbage collector that can invoked either by the user or automatically by the SDD library This is described next 3 1 Live and Dead Nodes A decision SDD node is either live or dead When the garbage collector is invoked dead SDD nodes are claimed their memory is freed The SDD library provides a primitive for referencing SDD nodes When a node is referenced it is guaranteed to be live More generally a decision SDD node is live if and only if a it has been referenced by the user or b it is referenced by a live SDD node as a prime or sub A reference to a decision SDD node can be canceled by dereferencing the node The SDD library provides a primitive for dereferencing SDD nodes Terminal SDDs are always live never garbage collected Terminal SDDs can be referenced and dereferenced but these operations have no effect in this case Consider Figure 3 a in which the left root has been referenced by the user This SDD has three live nodes The one that has been referenced by the user left root and two other nodes that are referenced by live SDD nodes A further reference by the user to the middle root leads to Figure 3 b A final user reference to the right root leads to Figure 3 c in which all nodes are now live If we dereference the right root in Figure 3 c we go back to Figure 3 b 3 2 Reference Counts The garbage colle
27. e same total variable order A B C D On the other hand the vtree in Figure 1 a induces the total variable order B A D C The SDD library provides prim itives for retrieving the total variable order induced by a vtree It also provides primitives for constructing 3If we view v as a vtree node garbage collected SDD nodes will be those normalized for v its descendants and its ancestors vtrees according to a given variable order A code sample is provided in Section 7 which illustrates some construction methods of vtrees More generally a vtree induces a total order on all of its nodes which is obtained by an inorder traversal of the vtree nodes i e left subtree node right subtree In Figure 2 we have labeled each vtree node with its position in the corresponding vtree inorder first position is 0 The SDD library provides primitives for retrieving the position of each vtree node The library also provides primitives for saving vtrees into the dot format while labeling each vtree node with its position in the corresponding inorder All example vtrees used in this manual have been produced using this primitive 4 2 Operations The SDD library provides primitives for changing the structure of a vtree and adjusting the structure of corresponding SDDs Three primitives are provided for this purpose which are explained in Figure 4 right rotating a vtree node left rotating a vtree node and swapping a vtree node O swap_vnode
28. f live SDD nodes in vtree v 5 3 6 State void sdd_vtree_set_bit int bit Vtree vtree Sets the bit flag for a vtree node Bit flags are initialized to 0 and as a general rule they should be reset to 0 when flags are not being used int sdd_vtree_bit const Vtree vtree Returns the bit flag of a vtree node void sdd_vtree_set_data void data Vtree vtree Sets the data field for a vtree node This is a void pointer which is provided for user convenience This field can be used to allocate auxiliary data to individual vtree nodes The SDD library does not access this field directly except to initialize it to NULL The source code for the CNF DNF to SDD compiler see Section 6 provides an example of how this field could be used void sdd_vtree_data Vtree vtree Returns the data field for a vtree node void sdd_vtree_set_search_state void search_state Vtree vtree Sets the search state field for a vtree node This is a void pointer which is provided for user convenience This field can be used to allocate additional auxiliary data to individual vtree nodes which is dedicated to vtree search algorithms developed by the user The SDD library does not access this field directly except to initialize it to NULL The source code for the vtree search algorithm see Section 6 provides an example of how this field could be used void sdd_vtree_search_state Vtree vtree Returns the search state field for a vtree node 1
29. ference on Artificial Intelligence AAAI pages 187 194 2013 Adnan Darwiche SDD A new canonical representation of propositional knowledge bases In Proceedings of the 22nd International Joint Conference on Artificial Intelligence IJCAI pages 819 826 2011 C Meinel and T Theobald Algorithms and Data Structures in VLSI Design OBDD Foundations and Applications Springer 1998 Fabio Somenzi CUDD CU Decision Diagram package University of Colorado at Boulder http v1si colorado edu fabio CUDD 2012 Yexiang Xue Arthur Choi and Adnan Darwiche Basing decisions on sentences in decision diagrams In Proceedings of the 26th Conference on Artificial Intelligence AAAI pages 842 849 2012 27 A 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 Redistributions 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 w
30. ger SddNode sdd_deref SddNode node SddManager manager void sdd_manager_garbage_collect SddManager manager int sdd_manager_garbage_collect_if float dead_node_threshold SddManager manager void sdd_vtree_garbage_collect Vtree vtree SddManager manager int sdd_vtree_garbage_collect_if float dead_node_threshold Vtree vtree SddManager manager Manual SDD Minimization Vtree sdd_vtree_minimize Vtree vtree SddManager manager void sdd_manager_minimize SddManager manager void sdd_manager_set_lr_time_limit SddSize time_limit SddManager manager void sdd_manager_set_rr_time_limit SddSize time_limit SddManager manager void sdd_manager_set_sw_time_limit SddSize time_limit SddManager manager void sdd_manager_set_lr_size_limit float size_limit SddManager manager void sdd_manager_set_rr_size_limit float size_limit SddManager manager void sdd_manager_set_sw_size_limit float size_limit SddManager manager void sdd_manager_set_rr_cartesian_product_limit int cartesian_product_limit SddManager manager void sdd_manager_set_sw_cartesian_product_limit int cartesian_product_limit SddManager manager void sdd_manager_set_convergence_threshold float threshold SddManager manager Weighted Model Counting WmcManager wmc_manager_new SddNode node int log_mode SddManager manager void wmc_manager_free WmcManager wmc_manager void wmc_set_literal_weight const SddLiteral literal
31. he read SDD is guaranteed to be equivalent to the one in the file but may have a different structure depending on the current vtree of the manager SDD minimization will not be performed when reading an SDD from file even if auto SDD minimization is active void sdd_save_as_dot const char fname SddNode node Saves an SDD to file formatted for use with Graphviz dot to produce graphs like the one in Figure 1 b void sdd_shared_save_as_dot const char fname SddManager manager Saves the SDD of the manager s vtree a shared SDD formatted for use with Graphviz dot to produce graphs like the one in Figure 1 b 5 2 4 Navigation The following functions are useful for navigating the structure of an SDD i e visiting all its nodes int sdd_node_is_true SddNode node int sdd_node_is_false SddNode node int sdd_node_is_literal SddNodex node int sdd_node_is_decision SddNode node Returns 1 if node is of the mentioned type 0 otherwise SddLiteral sdd_node_literal SddNode node Returns the signed integer i e variable index or the negation of a variable index of an SDD node repre senting a literal Assumes that sdd_node_is literal node returns 1 SddNodeSize sdd_node_size SddNode node Returns the size of an SDD node Recall that the size is zero for terminal nodes i e non decision nodes SddNode sdd_node_elements SddNode node Returns an array containing the elements of an SDD node If the node has
32. lized for node v 5 in Figure 2 b and for node v 3 in Figure 2 c If a Boolean function f is normalized for an internal vtree node v its variables can be uniquely split into X Variables of f appearing in the left subtree of v Y Variables of f appearing in the right subtree of v We next show how this variable splitting strategy leads to a canonical SDD once a vtree is fixed 2 Sentential Decision Diagrams SDDs Consider the Boolean function and vtree in Figure 1 This Boolean function is normalized for node v 3 leading to the variable split X A B Y C D and the following decomposition AA B V BAC V CAD AAB A true V SAMBA C V aB ACAD 3 _ o prime sub prime sub prime sub This decomposition has three primes AA B AA B and B The last prime is a literal and is therefore a terminal SDD The first two primes however will need to be decomposed further They are both normalized for node v 1 leading to the variable split X B Y A and the decompositions AnB B N ADVISE RAM AAB B NA V BA L o o o prime sub prime sub prime sub prime sub Note that all resulting primes and subs are terminal SDDs The decomposition in 3 also has three subs true C and CAD The first two are terminal SDDs The last sub is not terminal It is normalized for node v 5 leading to the variable split X D Y C and the corresponding decom
33. manager_options SddManager manager 29 SDDs Queries and Transformations SddNode sdd_conjoin SddNode nodel SddNode node2 SddManager manager SddNode sdd_disjoin SddNode nodel 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 SddNode sdd_apply SddNode node1 SddNode node2 BoolOp op SddManager manager SddNode sdd_apply_in_vtree SddNode node1 SddNode node2 BoolOp op Vtreex vtree SddManager manager Size and Count SddSize sdd_size SddNode node SddSize sdd_count SddNode node SddSize sdd_shared_size SddNode nodes SddSize count File I O void sdd_save const char fname SddNode node SddNode sdd_read const char filename SddManager manager void sdd_save_as_dot const char fname SddNode node void sdd_shared_save_as_dot const char fname SddManager manager Navigation int sdd_node_is_true SddNode node int sdd_node_is_false SddNode node int sdd_node_is_literal SddNodex node int sdd_node_is_decision SddNode node SddLi
34. mma sdd_manager_literal 3 manager manager sdd_conjoin gamma sdd_manager_literal 2 manager manager gamma sdd_conjoin gamma sdd_manager_literal 4 manager manager printf before referencing n printf live sdd size zu n sdd_manager_live_size manager printf dead sdd size zu n sdd_manager_dead_size manager ref SDDs so that they are not garbage collected sdd_ref alpha manager sdd_ref beta manager sdd_ref gamma manager printf after referencing n printf live sdd size zu n sdd_manager_live_size manager printf dead sdd size zu n sdd_manager_dead_size manager garbage collect sdd_manager_garbage_collect manager printf after garbage collection n printf live sdd size zu n sdd_manager_live_size manager printf dead sdd size zu n sdd_manager_dead_size manager sdd_deref alpha manager sdd_deref beta manager sdd_deref gamma manager printf saving vtree amp shared sdd n sdd_vtree_save_as_dot output shared vtree dot vtree sdd_shared_save_as_dot output shared dot manager sdd_vtree_free vtree sdd_manager_free manager return 0 7 4 Example 3 Minimizing an SDD include lt stdio h gt include lt stdlib h gt include sddapi h include compiler h 22 int main int argc char argv set up vtree and manager Vtree vtree sdd_vtree_read in
35. n Figure 3 a depicts a shared SDD that represents three distinct Boolean functions one for each root The size of this shared SDD is 12 Its node count is 6 2 4 Normalization A literal or decision SDD node n is associated with the lowest vtree node v that contains the variables of n We say in this case that n is normalized for v A constant SDD node is not normalized for associated with any vtree node The SDD library provides primitives for saving SDDs into the dot format These primitives label each decision SDD node with the vtree node it is normalized for All example SDDs used in this manual have been produced using these primitives 2 5 SDD and Vtree Nodes When an SDD node n is normalized for some node in vtree v we will say that node n is in vtree v The term SDD of vtree v will also refer to the collection of SDD nodes in vtree v The SDD library provides primitives for accessing the size and count of SDD nodes in some vtree v lif f is the Boolean function represented by a literal or decision node n then function f and node n are guaranteed to be normalized for the same vtree node see Section 1 2 2The dot format for describing graphs can be visualized by the GraphViz system available at http www graphviz org 2 6 Bottom up Construction of SDDs Section 2 started by describing a top down procedure for constructing SDDs which decomposes a Boolean function and then recursively decomposes its primes and subs Using the
36. nager SddNode sdd_manager_false const SddManager manager SddNode sdd_manager_literal const SddLiteral literal SddManager manager Automatic Garbage Collection and SDD Minimization void sdd_manager_auto_gc_and_minimize_on SddManager manager void sdd_manager_auto_gc_and_minimize_off SddManager manager void sdd_manager_set_minimize_function SddVtreeSearchFunc func SddManager manager void sdd_manager_unset_minimize_function SddManager manager Size and Count SddSize sdd_manager_size const SddManager manager SddSize sdd_manager_live_size const SddManager manager SddSize sdd_manager_dead_size const SddManager manager SddSize sdd_manager_count const SddManager manager SddSize sdd_manager_live_count const SddManager manager SddSize sdd_manager_dead_count const SddManager manager Misc Functions void sdd_manager_print SddManager manager SddLiteral sdd_manager_var_count SddManager manager Vtree sdd_manager_vtree const SddManager manager Vtree sdd_manager_vtree_copy const SddManager manager Vtree sdd_manager_vtree_of_var const SddLiteral var const SddManager manager Vtreex sdd_manager_lca_of_literals int count SddLiteral literals SddManager manager int sdd_manager_is_var_used SddLiteral var SddManager manager void sdd_manager_var_order SddLiteral var_order SddManager manager void sdd_manager_set_options void options SddManager manager void sdd_
37. nd Manual Garbage Collection o o 3 4 When to Reference Nodes te tei ir ee 4 More on Vtrees AD OIE 2 nie Ade bad hoe gle hh dado tes ace Dake el alga a e 42 Operations a rr bs BAIS A B eee a ek we ee eee le Ade tS da PA A A A ak EO Et Re AROS AA AA AE te Re ae Be E A ee ak A 45 Search and Minimization a rese dad a a pie Aupa ga me a ee 5 SDD API Oil Managers O ek ee be bd Bk oe ee eh ee A e a we A 51 1 Creating Managers ico est ae Ge a ok Wa Ba Gl ea Bae eS 5 12 Terminal SDDS sche dsd Bb da tra Bo 5 1 3 Automatic Garbage Collection and SDD Minimization OA piz rand Counts wisk fede an we etd eee ne be eee ee a Dro Mis Functions e oo ayaa a A VAD Sede oo Ge a te Ee a 52 MOD DS la e ad en Se e e GB 5 2 1 Queries and Transformations 2 2 0 52 2 Size and Counti a ER A A NE 02 3 Ple Os a da La a A Ae e o Ak A S24 Navigation i soe a a a dd A e yeh o e a 5 2 9 Misc Functions e ade 4 26 a e A A aa A A aah ad le aes ae ae Sa au Belk Be wea ad ke ee ee 5 3 1 Creating Vireesiu menre A A E ie a a a B 3 2 ize and Count g aa cients ee fh ARE Baek aye ce nie Aha BE A eee Dao MEMO 2 seh detect tortie wae ar ahs Mech haat a Pe Seba aes tasty ae gA NAVIGACION ata toe tty wy aa de dad A le ee ee a ea a 53 5 Edit Operations 24d PA GOP EAN es ESAS EBD A EEE SS D30 UAL ts het hoe ye eG ee Oe Pe Bagh ht ne eee BE be ea A en eh e A ddr MASCHRUNCTIONS e hades A A as te a ts
38. ns 1 a subdirectory include containing the header file sddapi h and 2 a subdirectory lib including the library file libsdd a Compile the code using gcc 02 std c99 test c Iinclude Llib lsdd lm o test Executing the command test will then run the program The example in Section 7 7 requires linking two additional files as explained in that section Note that each sample program may output different dot files in the directory they are run in These files can be converted to graphs using the GraphViz dot program Each sample program is also included with the SDD package along with a Makefile for compiling them 7 2 Example 1 Constructing a Simple SDD include lt stdio h gt include lt stdlib h gt include sddapi h int main int argc char argv set up vtree and manager SddLiteral var_count 4 SddLiteral var_order 4 2 1 4 3 20 const char type balanced Vtree vtree sdd_vtree_new_with_var_order var_count var_order type SddManager manager sdd_manager_new vtree construct a formula A B v B C v C7D printf constructing SDD SddNode f_a sdd_manager_literal 1 manager SddNodex f_b sdd_manager_literal 2 manager SddNode f_c sdd_manager_literal 3 manager SddNode f_d sdd_manager_literal 4 manager SddNode alpha sdd_manager_false manager SddNode beta beta sdd_conjoin f_a f_b manager alpha sdd_disjoin alpha beta manager beta sdd_c
39. nst char filename These are functions from the libsdd a library The following functions are also given in the source SddNode fnf_to_sdd_auto Fnf fnf SddManager manager SddNode fnf_to_sdd_manual Fnf fnf SddManager manager for compiling an FNF into an SDD Flat Normal Form FNF includes both CNF and DNF as special cases Finally the file format supported for reading CNF DNF s is the widely used DIMACS format This format includes a header p cnf n m where n is the number of CNF variables and m is the number of CNF clauses Each subsequent line represents a clause consisting of literals 1 or where 7 is a variable from 1 to n each line terminated by a O Lines starting with c are treated as comments and are ignored For example the following CNF file p cnf 6 3 140 1250 1 2 3 6 0 represents the CNF X1 V X4 A 7X1 V X2 V X5 A 7X1 V 7X2 V X V X6 The same file format can be used to represent DNFs except that we interpret a set of literals as a DNF term a conjunction of literals The file above will then specify the DNF X1 A X4 V 7X1 A X2 A X5 V 7X1 A7X2 A X3 A Xe 7 Code Samples We provide here a few sample programs and instructions for compiling each program with the SDD library These code samples are also included with the SDD package 7 1 Compiling To compile the examples in Sections 7 2 7 6 under Linux save any of the code samples to a file test c in a directory which contai
40. ode node SddLiteral variable_map SddManager manager Returns an SDD which is obtained by renaming variables in the SDD node The array variable_map has size n 1 where n is the number of variables in the manager A variable i 1 lt i lt n that appears in the given SDD is renamed into variable variable_map i variable_map 0 is not used int sdd_variables SddNode node SddManager manager Returns an array whose size is n 1 where n is the number of variables in the manager For each variable i 1 lt i lt n array i is 1 if variable i appears in the SDD node otherwise array i is 0 The array can be freed when it is no longer needed array 0 is not used 5 3 Vtrees We now discuss the functions for constructing manipulating and navigating vtrees This includes functions for saving vtrees to files and loading vtrees from files 5 3 1 Creating Vtrees There are a few default vtree structures linear or balanced and vtrees can also be read from and written to file see next section Vtree sdd_vtree_new SddLiteral var_count const char type Returns a vtree over a given number of variables var_count The type of a vtree may be right right linear left left linear vertical or balanced Vtree sdd_vtree_new_with_var_order SddLiteral var_count SddLiteral var_order const char type Returns a vtree over a given number of variables var_count whose left to right variable ordering is given in
41. of SDD variables currently associated with the manager Vtree sdd_manager_vtree const SddManager manager Returns the root node of a manager s vtree Vtree sdd_manager_vtree_copy const SddManager manager Returns a copy of a manager s vtree Vtreex sdd_manager_vtree_of_var const SddLiteral var const SddManager manager Returns the leaf node of a manager s vtree which is associated with var Vtree sdd_manager_lca_of_literals int count SddLiteral literals SddManager manager Returns the smallest vtree which contains the variables of literals where count is the number of literals If we view the variable of each literal as a leaf vtree node the function will then return the lowest common ancestor lca of these leaf nodes 11 int sdd_manager_is_var_used SddLiteral var SddManager manager Returns 1 if var is referenced by a decision SDD node dead or alive returns 0 otherwise void sdd_manager_var_order SddLiteral var_order SddManager manager Fills the array var_order whose length must equal the number of variables in the manager with the left to right variable ordering of the manager s vtree void sdd_manager_set_options void options SddManager manager Sets the options field for an SDD manager This is a void pointer which is provided for user convenience This field can be used to allocate auxiliary data to an SDD manager The SDD library does not access this field directly except
42. onjoin f_b f_c manager alpha sdd_disjoin alpha beta manager beta sdd_conjoin f_c f_d manager alpha sdd_disjoin alpha beta manager printf done n printf saving sdd and vtree sdd_save_as_dot output sdd dot alpha sdd_vtree_save_as_dot output vtree dot vtree printf donen sdd_vtree_free vtree sdd_manager_free manager return 0 7 3 Example 2 Garbage Collecting an SDD include lt stdio h gt include lt stdlib h gt include sddapi h int main int argc char argv set up vtree and manager SddLiteral var_count 4 const char type right Vtree vtree sdd_vtree_new var_count type SddManager manager sdd_manager_new vtree construct the term X_1 X_2 X_3 X_4 SddNode alpha sdd_manager_literal 1 manager alpha sdd_conjoin alpha sdd_manager_literal 2 manager manager alpha sdd_conjoin alpha sdd_manager_literal 3 manager manager 21 alpha sdd_conjoin alpha sdd_manager_literal 4 manager manager construct the term X_1 X_2 X_3 X4 SddNode beta sdd_manager_literal 1 manager beta sdd_conjoin beta sdd_manager_literal 2 manager manager beta beta sdd_conjoin beta sdd_manager_literal 3 manager manager sdd_conjoin beta sdd_manager_literal 4 manager manager construct the term X_1 7X_2 X_3 X_4 SddNode gamma sdd_manager_literal 1 manager gamma gamma sdd_conjoin ga
43. ons This algorithm is also implemented by the library functions sdd_vtree_minimize and sdd_vtree_gc_then minimize discussed earlier e A CNF DNF to SDD compiler which employs the provided vtree search algorithm Two versions of the compiler are distributed based on automatic and manual garbage collection and SDD minimization The SDD Package also includes a pre compiled binary for each supported architecture along with some sample CNFs To compile one of the sample CNFs into an SDD using the pre compiled binary we execute the following on the command line bin sdd linux c cnf s208 1 scan cnf t balanced r2 The c flag specifies a CNF file the t balanced flag and option specifies that a balanced vtree is used as an initial one and the r2 flag specifies that dynamic vtree search should be performed These command line options correspond to the ones used in the experimental results reported in 1 To see a list of all command line options run the command bin sdd linux h There are a few particularly relevant functions for individuals who are looking to modify the CNF DNF to SDD compiler First the following functions are available for reading CNFs and DNFs from file 6The choice of initial vtree and the use of dynamic vtree search can have a significant impact on the efficiency of compilation or even whether a CNF DNF can be successfully compiled or not 19 Cnf sdd_cnf_read const char filename Dnf sdd_dnf_read co
44. ons or swaps that may significantly increase the size of an SDD or that may take too much time the SDD library allows users to specify time or size limits on these operations If an operation exceeds these limits as it is doing its work the operation fails and rolls back any changes it has made Time limits are specified in terms of the number of apply operations performed during an operation i e the number of conjoins and disjoins The number of apply operations is not strictly a measure of time but should produce consistent results across different architectures Size limits are accumulative and hence can be used to constrain the SDD growth due to a sequence of vtree operations In particular a size limit is interpreted relative to a particular vtree v and initial size s That is when a size limit of say 1 2 is specified for a vtree operation it means that after performing the 4The dot format for describing graphs can be visualized by the GraphViz system available at http www graphviz org 3 A a A B 5 Ble EAL NEE A Ley C D A B C D CID Eau AB FALL C D GGL 4158 EAT a Before rotation b After rotation Figure 5 Left rotating vtree node v 3 in Figure 5 a leads to the vtree and SDD in Figure 5 b operation the size of the SDD for vtree v must remain
45. position CAD D ACIV DA L prime sub prime sub Note again that all resulting primes and subs are terminal SDDs 2 1 Graphical Depiction We have now fully decomposed the Boolean function of Figure 1 leading to the canonical SDD depicted graphically in Figure 1 b This figure contains four decompositions each of which is depicted by a circle O which is called a decision SDD node The children of a decision SDD node are depicted by paired boxes pls called elements The left box of an element corresponds to a prime p while the right box corresponds to its sub s In the graphical depiction of SDDs a prime p sub s is either a constant literal or pointer to a decision SDD node Constants and literals are called terminal SDD nodes 2 2 Size and Count The size of a decision SDD node is the number of its elements The size of a terminal SDD node is 0 The size of an SDD is the sum of the sizes attained by its nodes The root decision node of Figure 1 b has size 3 The remaining decision nodes have size 2 each The size of this SDD is then 9 3 2 4 2 42 The node count of an SDD is the number of its decision nodes The node count of the SDD in Figure 1 b is 4 The SDD library provides primitives for retrieving the size of an SDD and the count of its decision nodes 2 3 Shared SDDs An SDD is typically identified by its root SDD node A shared SDD is a multi rooted SDD with each root representing its own Boolean functio
46. put opt swap vtree SddManager manager sdd_manager_new vtree printf reading sdd from file n SddNode alpha sdd_read input opt swap sdd manager printf sdd size zu n sdd_size alpha ref perform the minimization and then de ref sdd_ref alpha manager printf minimizing sdd size sdd_manager_minimize manager printf done n printf sdd size zu n sdd_size alpha sdd_deref alpha manager augment the SDD printf augmenting sdd n SddNodex beta sdd_disjoin sdd_manager_literal 4 manager sdd_manager_literal 5 manager manager beta sdd_conjoin alpha beta manager printf sdd size zu n sdd_size beta ref perform the minimization again on new SDD and then de ref sdd_ref beta manager printf minimizing sdd sdd_manager_minimize manager printf done n printf sdd size zu n sdd_size beta sdd_deref beta manager sdd_manager_free manager sdd_vtree_free vtree return 0 7 5 Example 4 Rotating a Vtree Node include lt stdio h gt include lt stdlib h gt include sddapi h int main int argc char argv set up vtree and manager Vtree vtree sdd_vtree_read input rl 4 vtree SddManager manager sdd_manager_new vtree 23 construct the term X_1 X_2 X_3 X_4 SddNode alpha sdd_manager_literal 1 manager alpha sdd_conjoin alpha sdd_manager_literal 2
47. rgv set up vtree and manager Vtree vtree sdd_vtree_read input big swap vtree SddManager manager sdd_manager_new vtree 24 printf reading sdd from file n SddNode alpha sdd_read input big swap sdd manager printf sdd size zu n sdd_size alpha to perform a swap we need the manager s vtree Vtree manager_vtree sdd_manager_vtree manager double limit ref alpha no dead nodes when swapping sdd_ref alpha manager limit 2 0 printf modifying vtree swap node 7 limit growth by 1fx limit int succeeded sdd_manager_set_size_limit_context manager_vtree manager succeeded sdd_vtree_swap manager_vtree manager 0 limit 0 printf s n succeeded succeeded did not succeed printf sdd size zu n sdd_size alpha printf modifying vtree swap node 7 no limit succeeded sdd_vtree_swap manager_vtree manager 0 0 0 0 printf s n succeeded succeeded did not succeed printf sdd size zu n sdd_size alpha printf updating context of size limit n sdd_manager_update_size_limit_context manager Vtree left_vtree sdd_vtree_left manager_vtree limit 1 2 printf modifying vtree swap node 5 limit growth by 1fx limit succeeded sdd_vtree_swap left_vtree manager 0 limit 0 printf s n succeeded succeeded did not succeed printf sdd size zu n sdd_size alpha limit
48. ritten 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 28 B SDD API The libsdd library provides the following functions which are described in Section 5 This section is intended more as a reference Managers Creating Managers SddManager sdd_manager_new Vtree vtree SddManager sdd_manager_create SddLiteral var_count int auto_gc_and_minimize void sdd_manager_free SddManager manager void sdd_manager_add_var_before_first SddManager manager void sdd_manager_add_var_after_last SddManager manager void sdd_manager_add_var_before SddLiteral target_var SddManager manager void sdd_manager_add_var_after SddLiteral target_var SddManager manager Terminal SDDs SddNode sdd_manager_true const SddManager ma
49. ted and made a left right sibling of leaf v void sdd_manager_add_var_before SddLiteral target_var SddManager manager void sdd_manager_add_var_after SddLiteral target_var SddManager manager Let v be the vtree leaf node labeled with variable target_var A new leaf node labeled with variable n 1 is created and made a left right sibling of leaf v 5 1 2 Terminal SDDs SddNode sdd_manager_true const SddManager manager Returns an SDD representing the function true SddNode sdd_manager_false const SddManager manager Returns an SDD representing the function false SddNode sdd_manager_literal const SddLiteral literal SddManager manager Returns an SDD representing a literal The variable literal is of the form i where 7 is an index of a variable which ranges from 1 to the number of variables in the manager If literal is positive then the SDD representing the positive literal of the i th variable is returned If literal is negative then the SDD representing the negative literal is returned 10 5 1 3 Automatic Garbage Collection and SDD Minimization Automatic garbage collection and SDD minimization will take place only when calling functions that con struct SDDs These functions are listed in Section 5 2 1 void sdd_manager_auto_gc_and_minimize_on SddManager manager Activates automatic garbage collection and automatic SDD minimization void sdd_manager_auto_gc_and_minimize_off SddManager manager
50. teral sdd_node_literal SddNodex node SddNodeSize sdd_node_size SddNode node SddNodex sdd_node_elements SddNode node void sdd_node_set_bit int bit SddNode node int sdd_node_bit SddNode node Misc Functions Vtree sdd_vtree_of SddNode node SddSize sdd_id SddNode node int sdd_garbage_collected SddNode node SddSize id SddNode sdd_copy SddNode node SddManager dest_manager SddNode sdd_rename_variables SddNode node SddLiteral variable_map SddManager manager int sdd_variables SddNode node SddManager manager Vtrees Creating Vtrees Vtree sdd_vtree_new SddLiteral var_count const char type 30 Vtree sdd_vtree_new_with_var_order SddLiteral var_count SddLiteral var_order const char type void sdd_vtree_free Vtree vtree Size and Count SddSize sdd_vtree_size const Vtree vtree SddSize sdd_vtree_live_size const Vtree vtree SddSize sdd_vtree_dead_size const Vtree vtree SddSize sdd_vtree_count const Vtree vtree SddSize sdd_vtree_live_count const Vtree vtree SddSize sdd_vtree_dead_count const Vtree vtree SddSize sdd_vtree_size_at const Vtree vtree SddSize sdd_vtree_live_size_at const Vtree vtree SddSize sdd_vtree_dead_size_at const Vtree vtree File I O void sdd_vtree_save const char fname Vtree vtree Vtree sdd_vtree_read const char filename void sdd_vtree_save_as_dot const char fname Vtree vtree Navigation int sdd_vtree_is_leaf
51. time size and cartesian product limits A limit of 0 deactivates the limit Returns 1 if the operation succeeds and 0 otherwise i e limits exceeded This operation assumes no dead SDD nodes inside or above vtree and does not introduce any new dead SDD nodes int sdd_vtree_swap Vtree vtree SddManager manager SddSize time_limit float size_limit int max_cartesian_product Swaps the children of a vtree node given time size and cartesian product limits A limit of 0 deactivates the limit Returns 1 if the operation succeeds and 0 otherwise i e limits exceeded This operation assumes no dead SDD nodes inside or above vtree and does not introduce any new dead SDD nodes A size limit is interpreted using a context which consists of two elements First a vtree v which is used to define the live SDD nodes whose size is to be constrained by the limit Second an initial size s to be used as a reference point when measuring the amount of size increase That is a limit will constrain the size of live SDD nodes in vtree v to lt lxs void sdd_manager_set_size_limit_context Vtree vtree SddManager manager Declares a limit on the size of live SDD nodes in vtree v Sets the reference point s to the current size of live SDD nodes in vtree v Vtree operations constrained by this limit are assumed to be applied to vtree v void sdd_manager_update_size_limit_context SddManager manager Updates the reference point s to the current size o
52. to initialize it to NULL The source code for the CNF DNF to SDD compiler see Section 6 provides an example of how this field could be used void sdd_manager_options SddManager manager Returns the options field for an SDD manager 5 2 SDDs We now describe the functions for constructing and manipulating SDDs This includes functions for accessing SDD properties saving SDDs to files and loading SDDs from files 5 2 1 Queries and Transformations SddNode sdd_conjoin SddNode nodel SddNode node2 SddManager manager SddNode sdd_disjoin SddNode nodel SddNode node2 SddManager manager SddNode sdd_negate SddNode node SddManager manager Returns the result of applying the corresponding Boolean operation on the passed SDDs SddNode sdd_condition SddLiteral lit SddNode node SddManager manager Returns the result of conditioning an SDD on a literal where a literal is a positive or negative integer SddNode sdd_exists SddLiteral var SddNode node SddManager manager SddNode sdd_forall SddLiteral var SddNode node SddManager manager Returns the result of existentially universally quantifying out a variable from an SDD A model of an SDD is a truth assignment of the SDD variables which also satisfies the SDD The cardinality of a model is the number of variables assigned the value true by the model SddModelCount sdd_model_count SddNode node Returns the model count of an SDD SddLiteral sd
53. x 0 3 swap_vnode x a a Rotating a vtree node Ta the children of a vtree node lr_vnode x Figure 4 Rotating and swapping vtree nodes For an example of these operations consider the vtree and corresponding SDD in Figure 5 a If we left rotate vtree node v 3 we get the vtree and corresponding SDD in Figure 5 b Note how the rotation operation has adjusted the SDD structure in addition to changing the vtree structure for details see 1 Consider Figure 4 Before swapping or right rotating x the user must ensure that there are no dead SDD nodes inside or above vtree x Moreover before left rotating x the user must ensure that are no dead SDD nodes inside or above vtree w Swapping and rotation operations will not introduce any dead SDD nodes These operations are typically used to search for an alternative of some vtree v which implies that all operations will be applied to nodes inside vtree v In this case one should start by calling local garbage collection on vtree v to ensure that there are no dead nodes inside or above vtree v This ensures the preconditions of these operations Moreover since these operations do not introduce dead SDD nodes the preconditions continue to hold after applying each operation 4 3 Limits Rotating or swapping a vtree node can have a significant impact on the size of the corresponding SDD These operations may also take a substantial amount of time in some cases To protect against rotati
Download Pdf Manuals
Related Search