Knowledge compilation is a well-researched field focused on translating propositional logic formulas into eficient data structures that allow polynomial-time online queries related to the SAT problem. Knowledge compilation techniques can be used to partition product configuration tasks into two distinct phases: fast online processing and slow ofline preprocessing. Binary Decision Diagrams (BDDs) are widely studied in this area and provide a graph representation of Boolean formulas. However, BDD construction can be time-consuming, particularly for large instances, as their size grows exponentially with the number of variables. This paper explores methods to improve BDD construction time, including optimizing variable ordering. The evaluation involves applying these techniques to formulas in Rich Conjunctive Normal Form, comparing the results with Sentential Decision Diagrams. The experiments use CAS Software AG benchmarks.
life logical relations and rules in a way that can easily be used in computer. The following example demonstrates how Boolean formulas are used in the area of product configuration: Example 1.1. Suppose a company selling bikes ofers various configurations, where selecting one component (i.e., bike frame) can limit choices for other components (i.e., wheels) due to compatibility constraints. These constraints can be represented as Boolean formulas. 1 = ¬ F1 ∨ ((W ∨ B) ∧ ¬BL ∧ ¬G) (1)
Each variable in Equation 1 is assigned a value of true if the option is chosen. F1 is the variable representing the frame option, and W, B, G, BL are the variables representing the frame colors white, blue, green, and black respectively. The formula represents the rule that if a frame 1 is chosen, only the colors white and blue can be selected.
Configuration of complex products with many options may be a computationally hard problem that also can be (T. Ostertag) large amount of states [1].
Given the OBDD representation of a Boolean formula, satisfiability can be checked in constant time, solutions can be found in linear time, and models can be counted in polynomial time [2]. However, the size of the BDD as well as its construction time can be exponential in the number of variables.
uration rules can be eficiently verified in the runtime, but we have to consider potentially long preprocessing time. Therefore, the reduction of BDD is essential for improving performance and can be achieved by optimizing variable ordering.
In this paper, we overview existing approaches for minimizing BDD size, apply them to RCNF formulas and introduce modifications of existing approaches: variable frequency and M-FORCE constraint ordering heuristics and construction strategies. We evaluate existing as well as our heuristics using real-world configurations and present our modification of ordering heuristics for Sentential Decision Diagrams (SDDs) construction, which is if either the satisfying assignment of the formula is found a recently developed type of decision diagram that is a or it is determined that the formula is not satisfiable. superset of OBDDs.
Chapter 2 presents some basic definitions that will 2.3. Binary Decision Diagram be used throughout the work. Chapter 3 provides some insights into related works. Chapter 4 presents our or- This section is based on the Handbook of Model Checkdering heuristics. Chapter 5 presents the libraries used ing [3]. to implement our approach and which also serve to measure baseline performance. Finally, Chapter 6 provides evaluation results for the described methods.
Definition 2.5. A Binary Decision Diagram (BDD) represents a Boolean function as an acyclic directed graph, with the nonterminal vertices labeled by Boolean variables and the leaf vertices labeled with the values 1 and 0.
Each nonterminal vertex has two outgoing edges: ℎ( ) , corresponding to the case where its variable has value 1, and ( ) , corresponding to the case where its variable has value 0.
Definition 2.6. An Ordered Binary Decision Diagram (OBDD) is a BDD for which an additional ordering rule applies: for each nonterminal vertex associated with variable and a vertex ∈ {( ), ℎ( )} associated with variable , we must have <
This chapter contains definitions and examples of main concepts used in this work.
This section contains definitions and notions including canonical normal forms of Boolean formulas.
Definition 2.1. Conjunctive Normal Form (CNF) is a conjunction of clauses ⋀ , where each clause is a disjunction of literals ⋁ . A CNF clause is satisfied if at least one of its literals is satisfied. A CNF formula is satisfied if all of its clauses are satisfied.
An OBDD can be reduced by eliminating redundant nodes and merging terminal and duplicate nodes. The result of such reduction is the Reduced Ordered BDD (ROBDD) [3]. This reduction can be performed in the time linear in the size of the original graph [4].
Definition 2.2. Disjunctive Normal Form (DNF) is a ROBDDs serve as a canonical form for Boolean funcdisjunction of terms ⋀ , where each term is a con- tions, meaning that, for a given variable ordering, evjunction of literals ⋁ . A DNF term is satisfied if all of ery Boolean function has a unique representation as a its literals are satisfied. A DNF formula is satisfied if at ROBDD. The construction of a ROBDD is essential to least one of its terms is satisfied. keep the BDD as small as possible, as the complexity of most algorithms that utilize BDD is dependent on the Definition 2.3. An At-Most-One (AMO) constraint is a number of nodes/length of paths in the tree. In this paper, Boolean formula that takes a set of literals as an input and every mention of BDD refers to ROBDD. outputs true (is satisfied ) if and only if maximal one of Given a BDD of a function, we can answer these and the input literals is satisfied. For a set of literals { 1, ..., }, other questions related to a SAT problem for a given we use the following notation for the AMO constraint: instance. The function is satisfiable, if it does have a ( 1, ..., ) terminal node labeled with value 1. We can find a ranDefinition 2.4. A Rich Conjunctive Normal Form dom solution for the formula by traversing the diagram (RCNF) formula is a conjunction of constraints, where from root toward the ”1” leaf. The complexity of such a constraint can be a DNF formula, a disjunction of lit- algorithm is (ℎ) , where h is the height of the BDD. We erals (equal to the CNF clause) or an AMO constraint. can count the number of solutions by traversing the BDD A RCNF formula is satisfied if all of its constraints are and counting the paths. The complexity is () , where satisfied. Basically, RCNF is an extension of a CNF that is the number of nodes. [2, 3] allows more types of constraints, and thus allows smaller The common strategy for BDD frameworks is to divide representation of a complex configuration rules . an overall function into smaller functions and creating BDDs bottom-up. We start by creating BDDs for single 2.2. The Boolean Satisfiability Problem literals, and then subsequently use the BDDs from previous steps to create new ones by applying operations like Let { 1, ..., } be a set of Boolean variables and be a AND, OR, XOR. The generalization of these operations propositional logic formula in CNF that contains only is called Apply algorithm. The algorithm creates a BDD literals of { 1, ..., }. Formula is satisfiable if and only that represents the given result of applying the operation if there exists a set of variable assignments, so that is between the formulas of input BDDs. The overall time true. The Boolean Satisfiability Problem (SAT) is solved complexity of an Apply operation is ( × ), where
This section is based on the work of Darwiche (2011) [6].
Sentential Decision Diagram (SDD) is a more recent technique of representing of propositional knowledge bases. SDDs are a strict superset of OBDDs and are inspired by two discoveries: structured decomposability and strongly deterministic decompositions.
To explain SDDs, we first define the decomposition that is used to construct this type of decision diagram and the we define the important notion of vtrees. Definition 2.7. Consider a Boolean function ( , ) with non-overlapping variables and . If = ( 1( ) ∧ 1( )) ∨ ... ∨ ( ( ) ∧ ( )) then {( 1, 1), ..., ( , )} is called a ( , ) -decomposition of function . We call each pair ( , )an element of the decomposition, a prime and a sub. If ∧ = false for ≠ the decomposition is called strongly deterministic on .
Definition 2.8. A vtree for variables is a full binary tree whose leaves are in one-to-one correspondence with the variables in .
This section provides some insights into existing researches of BDDs and SDDs.
The work of Hadzic et al. [8] presents BDDs as an eficient solution to the configuration problem. The authors also describe how they applied this method practically in the commercial software product Configit . They highlight that BDDs can be eficiently applied in industry use cases, since they have several advantages over commonly used search-based configurators, including faster response times, better scalability, and improved rule quality [8]. However, the research just mentions variable ordering methods to optimize BDDs, but does not provide any examples of eficient heuristics.
and are the number of vertices in BDDs where An SDD that consists of a constant or a literal is called vertices and respectively are the root nodes of input terminal. Otherwise, it is called decomposition. SDDs trees. are canonical, which means that for a given vtree, every
A BDD requires a defined variable ordering that will be Boolean function has a unique representation of an SDD followed along all paths of a diagram. The size of a BDD [6]. SDDs are a strict superset over BDDs. The variable depends heavily on the ordering of input variables. Some ordering of a BDD will then correspond to the total order functions can rise in size from linear to exponential in the of the vtree, which is defined as a sequence of variables number of variables due to a bad ordering. However, the obtained from the left-right traversal of the vtree [ 6]. problem of finding an optimal variable ordering to con- BDD-trees are twofold exponential in treewidth, struct a minimum-size BDD is proven to be NP-complete whereas SDDs are just exponential. The SDDs are also as and some functions don’t have an optimal ordering [5]. tractable as BDDs, but are more succinct both in theory Thus, instead of computing an optimal variable ordering, and in practice [7]. There exist some Boolean functions is a common approach to use heuristics to generate a that can be represented with at least exponential BDD good ordering and use it during BDD construction. size and only polynomial SDD size [7]. Definition 2.9. Notation: ⟨.⟩ denotes a mapping from SDDs into Boolean functions. is an SDD that respects vtree if:
The vtree is used to recursively decompose a given Boolean function starting at the root of the tree. The left subtree of each node corresponds to the X variables, and the right subtree to Y variables of the ( , ) decomposition. The SDD representation is then based on a recursive application of the presented decomposition technique. The formal definition of this operation is as follows:
In contrast to static variable ordering techniques, the dynamic ordering techniques attempt to adjust the ordering online during the construction of the decision diagram [9]. The idea was presented by Rudell (1993) [11] based on the observation that swapping two adjacent variables of a BDD can be implemented without major changes to the Boolean function library API [3]. One of such techniques is sifting . Variables are moved up and down in the ordering, until the algorithm finds a location that leads to an acceptable number of total vertices. Evaluation results show that sifting improves the memory performance, but it is also a time-consuming process [3].
This chapter describes diferent methods of ruleset preprocessing, variable ordering and BDD construction strategies. We will discuss the usage of existing state-ofthe-art methods like FORCE as well as suggest some new algorithms.
This section explores various variable reordering heuristics and their algorithms aimed at improving BDD construction speed. The algorithms prioritize low ordering time, manageable implementation complexity, and efective variable ordering specifically for RCNF formulas.
We implemented and experimented with the following two diferent variable ordering heuristics: Variable Frequency (VF) and FORCE (F).
Most SDD constructing algorithms work analog to the BDD construction that we presented earlier in this chapter: create a decision diagram from smaller decision dia- 4.1.1. Variable Frequency grams. This process is usually referred to as bottom-up compilation. We propose the variable frequency (VF) as an easy to
The work of Oztok and Darwiche (2015) [12] describes implement and eficient heuristic that produces reasona top-down compiler constructing SDDs from CNF formu- able orderings. The VF heuristic evaluates the variable’s las. The top-down compiler produces a subset of SDDs influence on the function output using the frequency called Decision-SDDs. The compiler utilizes techniques metric. This metric counts either overall appearances of from SAT solvers and model counting algorithms to de- each variable or the number of constraints containing compose a formula. Results presented in [12] show that this variable. Subsequently, the algorithm sorts the list the top-down compiler is consistently more performant of variables using these values in descending order. The than the bottom-up compiler. heuristic can be seen as a modification of the Depen
The miniC2D software package created by the Uni- dent Count heuristic described in [9], but used mainly versity of California includes code for SDD compilation for a more general type of decision diagram called Multibased on the idea of a top-down compiler from [12]. The Valued Decision Diagrams (MDDs). program doesn’t produce the SDDs itself, but its output The intuition behind this heuristic is that more concan be transformed to the SDD in linear time. strained variables are placed on a level closer to the root of the tree, which allows them to shorten the paths to 3.5. Multivalued Decision Diagram the terminal nodes. However, the frequency metric does not consider the semantics of the formula and can lead Multivalued Decision Diagram (MDD) is another struc- to a false conclusion about variable influence. ture that is also proved to be eficient in product config- The frequency counting takes linear time in the numuration area. MDDs can be seen as a generalization of ber of constraints in a formula Θ(||) , considering that BDDs, where a function can work with more than binary we have information about each constraint’s contained (true/false) values. Research by Andersen et al. [13] pro- variables. Sorting takes Θ(| || |) . Overall, the algovides an analysis of MDD usage in an interactive cost rithm takes loglinear time in the number of variables calculation task. The research also highlights the impor- Θ(| || |) tance of variable ordering for both MDDs and BDDs. The evaluations even show that MDDs can perform better 4.1.2. FORCE Heuristic than BDDs for presented tasks. Nevertheless, most variable ordering heuristics are generally considered to be appliable to both BDDs and MDDs [9], so we could also apply the heuristics that we overview in our research to MDDs.
The FORCE heuristic which is described in the paper by Aloul et al. (2003) [14]. FORCE is introduced as an alternative to MINCE, as described in Section 3.2, and comes with a simpler implementation and orders-of-magnitude increased speed, while providing competitive results with MINCE.
The algorithm is based on the same observation as the MINCE heuristic: Related variables in satisfiability () = (∑ ) /||
∈ with denoting the index of a vertex in a current placement.
The new position ′ is calculated with the following formula in which is the set of all hyper-edges connected to the vertex . typically participate in the same CNF clauses [14], so the We implemented the following two diferent constraint heuristic reorders Boolean variables to place ”connected” ordering heuristics: Variable Frequency (VF-C) and Modvariables close to each other. FORCE transforms the vari- ified FORCE (M-FORCE). able ordering problem into the linear placement problem.
The vertices of a hypergraph correspond to variables and 4.2.1. Variable Frequency edges correspond to clauses. Since in our case, the RCNF is used, the clauses are replaced with constraints for all the definitions.
The FORCE algorithm uses the force-directed placement instead of a min-cut placement. The idea behind it is that interconnected objects (vertices of a hypergraph or variables in our case) experience forces analog to springs according to the Hooke’s law. The algorithm computes these forces and displaces the vertices in the direction of the forces iteratively.
After an initial ordering is given, the center of gravity of each hyperedge is defined the following way: We propose a concept of variable frequency ordering for constraints. The idea is to sort constraints according to the variables that they contain (similar to the VF ordering for variables). Specifically, it evaluates which variables are most influential in the ruleset and places the constraints that contain such variables at the beginning of a ruleset. Analog to the variable ordering with the same name, it evaluates the influence of the variables using frequency metric.
The proposed algorithm works the following way: we use the results of variable frequency ordering (Section 4.1.1). Then we analyze which variable in each constraint is the most frequent in the whole formula. If there are several variables with the same frequency, the one with the lowest index is taken. The constraint is then associated with this variable, and we sort the constraints according to the frequency of their associated variables.
It should be noted that the method induces a partition over the set of constraints based on the associated variables. The partition is specified in Equation 4. Let be the set of all constraints, and () the associated variable of constraint , i.e., the most frequent one. (2) (3) = (∑ () ∈
) /| |
Thereafter, the vertices are sorted according to the newly calculated positions. These iterations continue until a given metric of ordering stops improving. As proposed in the paper, the total variable span metric is used and the iterations stop after the metric doesn’t decrease after given number of iterations. Additionally, the iterations number is bounded by ⋅ | | , where is a constant.
The worst-case time of the algorithm is ((|| + | || |) ⋅ | |) [14], where C is the set of constraints, and we assume that the average degree of hyperedges and the average degree of vertices are limited by a constant.
We present the heuristic that utilizes the idea of the FORCE variable ordering heuristic by applying it to the constraint ordering. It uses the concept of interconnected objects and placement by measuring their forces, but uses constraints as objects and redefines the interconnected 4.2. Constraint Reordering objects as constraints having the same variables. Another approach to reduce BDD construction time is Basically, the algorithm is a modification of the FORCE by manipulating the ordering of constraints in an RCNF variable ordering, the diference is in the types of objects formula. By strategically grouping certain constraints that it takes as input. We build the hypergraph by using together, the time required for combining smaller BDDs constraints as nodes and edges as sets of constraints that during construction can be decreased. This not only obtain the same variable. For a set of variables | | , a set results in a smaller BDD but also reduces the time for of constraints and hypergraph edges definition looks subsequent operations. Constraint reordering, particu- like this: larly when combined with dynamic reordering, can be highly eficient as it minimizes the number of nodes in = { ⊆ | ∈ , ∀ ∈ ∶ ∈ } (5) intermediate results, thereby accelerating the sifting operation.
We then use Formulas 2 and 3 and run the same algorithm to find a constraint placement that minimizes = { [] ⊆ | ′ ∈ [] ⟺ () = (
′)} (4)
So, in addition to the most frequent variables being added to the overall BDD in the first iterations, this approach also groups the constraints with the same variables. 4.2.2. Modified FORCE the total span of the hypergraph (, ) . The number of iterations is bounded by ⋅ log || BDD of two constraints. We subsequently continue merging the BDDs containing the same amounts of constraints, As we can assume that every variable is used at least until the overall BDD is built. The construction order once, it applies || = | | . So, the worst-case time of each iteration is | | + ||
(analog to FORCE, we assume that average degrees of vertices and hyperedges are bound by a constant). The sorting takes Θ(||||) the worst-case performance of the algorithm is ((| | +
, so ||||)||)
.
The hypergraph construction is not as trivial as in the case of the origial FORCE heuristic. With the usage of mapping from variables to their parent constraints and a mapping of constraints to the edges attached to them, the overall time complexity of the hypergraph construction is (|| + | |)
, assuming that the number of variables in a constraint and the number of constraints containing a certain variable are bound by a constant.
weights to each constraint based on their influence on the output. These weights can be used in equations, such as the center of gravity and position formulas, to prioritize the faster movement of more influential constraints.
Given a constraint ordering, there can be several construction strategies on how to use that ordering to construct a BDD. The Apply algorithm is used to recursively create BDD from smaller BDDs starting with just variables. The order in which the algorithm is applied afects can be represented as a binary tree (Figure 1).
Example 4.1. Construction tree for a formula ( 1 ∨
This way, constraint BDDs do not get appended in the exact order provided by this ordering, but global ordering is not influenced too much. For example, if we swap every two constraints (for instance, swap A and B, C and D in the example 4.1) the construction of their resulting tree will stay the same.
An AMO constraint is not a binary operation, and its the construction time of a BDD and can be changed ei- construction is not directly possible using frameworks ther by constraint reordering, which we discussed in the previous section, or by construction strategies. like CUDD or libsdd that we will discuss later. Therefore, we have evaluated two ways on how to transform it into
In this section, we will present two construction strate- a form that uses Boolean operators. gies for RCNF formulas. We mention the commonly used Depth-First strategy and present the Merge Strategy.
The first way is to create a DNF representation of the AMO constraint, which is shown by Equation 6 and with each iteration, which slows down the appending of the AMO formula. 4.3.1. Depth-First Strategy A common straightforward approach: we append a smaller BDD to the overall diagram as soon as it gets constructed. For a RCNF formula, the strategy creates a constraint, appends it to the overall BDD tree and moves on with construction of the next constraint.
Constraint construction time stays bound by constraint size, whereby the overall tree increases its size the next BDDs. 4.3.2. Merge Strategy We present the Merge Strategy as an alternative to the Depth-First. This strategy tries to solve the problem by dividing this problem into smaller ones.
First, we merge the first two constraints of them together, then we merge the resulting BDD with another Equation 7 shows the whole formula .
= ( ⋀ ¬ ) ∧ ∧ ( ⋀ ¬ ),
∈ {1, ..., } −1 =1 =1
=+1 =1 = (⋁ ) ∨ ( ⋀ ¬ )
In this case, the number of operations needed to build a BDD grows quadratically in the number of literals in
Another way of presenting the AMO constraints is to use the XOR operation, which is also supported by the Apply algorithm. The formula constructed with XOR is shown by Equation 8: = ( 1 ⊕ 2 ⊕ ... ⊕ ∧ ) ∨ =0 = ⋁ ¬ ,
= ⋀ ¬ =0 (6) (7) (8)
The number of operations grows linear in the number of literals, which is makes it a more eficient method of building decision diagrams for AMO constraints. 4.4.1. SDD Vtrees and Variable Orders As we discussed earlier, the SDDs variable ordering is more complex and is defined by vtrees instead of total variable ordering that is used in OBDDs.
Darwiche and Choi presented the following definition in [15]: Definition 4.1. A vtree dissects a total variable order if a left-right traversal of the vtree visits leaves (variables) in the same order as .
In order to evaluate performance of the previously described BDD heuristics in the context of SDDs, we propose generating a total variable ordering, and then creating a vtree that dissects that ordering.
For one total variable ordering, there are many trees that can dissect it. Right-linear trees were discussed preciously in section 2. SDDs that respect right-linear vtrees correspond precisely to the OBDDs, and therefore they cannot lead to any enhanced performance. Another choice are left-linear trees and balanced trees. The balanced trees were used for evaluation in [15] and are also supported by the framework presented in this paper.
In this chapter, we describe the frameworks that allow constructing BDDs and SDDs using methods described in Chapters 2 and 4. 5.1. CUDD CUDD1 (Colorado University Decision Diagram) is an open-source state-of-the-art package for BDD manipulation written in C [16]. Practically, the package allows presents an implementation of the Apply algorithm and all needed data structures like unique table and cache.
The package also contains implementations of dynamic ordering algorithms. Available algorithms include sifting, window permutations, group sifting and others. The chosen algorithm will be used every time the number of nodes has increased up to a given threshold, which is set automatically after each reordering.
libsdd is an open-source library for SDD construction and performing queries on them [17]. The interface and functionality of this package are very similar to the CUDD, but with respect to the SDD specifics.
We can create a vtree with a given total order and pass a parameter that specifies the type of the tree (right-linear, left-linear, balanced, vertical or random) that dissects a given total variable ordering. The library also allows automatic SDD minimization, which is similar to BDD dynamic ordering.
This chapter focuses on the evaluation of the algorithms described in the previous sections. We will take a look at the evaluated benchmarks and compare the results of diferent program configurations on these benchmarks.
For the evaluation, we use a GPU computer with 64GB RAM, Intel Core i9-9900K 3.60Ghz CPU and Nvidia GeForce RTX 2080 Ti GPU.
We used CUDD framework to implement the BDD construction and ordering and libsdd for SDD construction and ordering.
One of the CAS Software applications is the Merlin CPQ configuration tool. It allows creating configuration rules using diferent complex relations between products and product parts. Fundamentally, the program has to solve the SAT problem for product configurations.
The evaluated benchmarks consist of real product conifguration rules of diferent companies that use Merlin CPQ. Each benchmark corresponds to a company and contains rulesets that describe company products. Their rules were converted from the Merlin CPQ format into boolean formulas. Each ruleset is an independent RCNF formula saved as a DIMACS file. Table 1 shows the benchmarks and the number of variables and constraints in each of them.
We evaluate the construction times as well as diagram sizes for the baseline approaches and diferent configurations of our approach. This includes several combinations of variants of variable ordering, constraint ordering, construction strategies, and an optional prior conversion of RCNF to CNF. We compare these configurations to the total construction time of SDDs using vtrees generated by the miniC2D top-down SDD compiler.
Configurations in the experiments are named using abbreviations. The construction strategy is specified only if it difers from the default depth-first strategy. All configurations utilize sifting dynamic ordering and XOR operations for AMO constraints, as shown in the Section 4.4.
When constructing a decision diagram, choosing a suboptimal ordering and dealing with numerous constraints in a ruleset can result in construction times lasting several days. To manage this, we impose a time limit during the construction process and evaluate the algorithm’s We can observe that the only configurations managing coverage. If the total construction time exceeds the limit, to order all instances under the limit are either VF or VFthe process is stopped, and the ruleset is considered un- C heuristics. The FORCE variable heuristic comes close constructed. We assess the algorithms by comparing the to ordering all instances. M-FORCE constraint heuristic number of constructed rulesets and analyzing various is even less performant, which can be explained with statistics for each algorithm. For example, we compare the fact that the number of constraints has more influthe ordering time for cases where ordering was com- ence here and this number is bigger than the number of pleted within the time limit. variables in the given benchmarks. The combination of
First, we evaluate diferent configurations with a 5- M-FORCE and FORCE heuristics applied to the rulesets minute limit and then use the most performant ones for converted to CNF is the least performant of all, since construction with a 1-hour limit. the number of clauses in CNF rulesets is normally bigger than the number of constraints in original RCNF rulesets.
Figure 2 shows how many instances of the whole set of ruleset can be ordered in a time given by the y-axis. Here, In this section, we will evaluate the decision diagram we evaluate only individual heuristics (with an excep- construction with a time limit. tion to M-FORCE/FORCE/MERGE/cnf), since the present variable and constraint ordering heuristics are indepen- 6.5.1. 5-Minute Limit dent, and configurations with both methods being used will just have an ordering time that equals the sum of In Table 3 we can see the results for BDD construcvariable and constraint orderings. In contrast, the CNF tion with variable ordering, constraint ordering, and benchmark changes the ordering time, since the number diferent construction strategies. t r u c k s , h e a t i n g and of variables and clauses is higher (as can be seen from f o r k l i f t s benchmarks did not result in successfully conTable 1). structed rulesets and are therefore not present. Merge
Bench 24 27 2 2 144 162 33 36 0 3 8 8 211 238 strategy consistently outperforms depth-first in every configuration. The best performance was achieved by the M-FORCE/FORCE/MERGE configuration, which also showed better results when the formula was given in RCNF rather than CNF.
Bench vms campers printers boards plants circuits Total
SDD mC2D cnf 8 0 7 0 27 33 170 2 247
We can see that even the best configuration shows only 56,1% done rulesets. F o r k l i f t s did not yield any constructed rulesets and is not present in the table and h e a t i n g and t r u c k s yielded just a few. From Table 1 we can see that these benchmarks are the biggest in terms of both variable number and constraint number, which leads to long ordering time. Still, big rulesets from h e a t i n g and t r u c k s are only constructed by MF/F, which manages to create the most optimal ordering.
We also evaluated the numbers of nodes for the diagrams constructed with the 1-hour limit. Here, we take only the subset of rulesets that are covered by each evaluated configuration.
SDD BDD SDD BDD BDD SDD BDD Bench MFF VVFF-C MFF VVFF-C MFF mcCn2fD MFF
M M M plants 63464 570814 5559 78494 1112080 4745 390098 printers 2155 7573 1908 6935 4668 3238 4559 vms 3937 4759 2091 5302 3280 3050 6170 circuits 3050 8141 3130 9946 12993 4975 29231 boards 5552 11306 2879 12200 6024 4611 6599 campers 3202 15079 1899 16447 2177 2015 7472
In Table 4 we can see that the heuristics do not work as well for SDDs as for BDDs. Configurations using variable and constraint heuristics do not improve coverage, Table 6 suggesting unsuitability for constructing eficient vtrees Median values of node counts for each configuration for SDDs. The best result is shown by the construction using vtrees created by miniC2D tool. We can see that M-FORCE/FORCE/MERGE BDD construction (Table 3) almost reaches the performance of best SDD configuration. t r u c k s , h e a t i n g and f o r k l i f t s benchmarks again did not yield constructed rulesets.
In Table 6 we can see that SDD M-FORCE/FORCE configuration has the lowest median node count on 4 benchmarks out of 6. SDD configurations generally have better scores than BDD. The best performance BDD conifguration is M-FORCE/FORCE. 6.5.2. 1-Hour Limit In Table 5 we can see coverage results for the 1-hour limit.
The table contains both results for SDDs and BDDs
The M-FORCE/FORCE/MERGE configuration manages to outperform SDDs constructed with vtrees from miniC2d. M-FORCE/FORCE also shows comparable results.
M-FORCE/FORCE/MERGE configuration delivers the best results for overall BDD construction time and outperforms all SDD configurations in 1-hour limit. However, it provides results that have one of the highest nodes counts. The presented configurations also improve construction time for SDDs in 1 hour limit, but still are inferior to some BDD configurations. In opposition to BDD, MFORCE/FORCE results in the smallest number of nodes for SDD.
Some benchmarks (t r u c k s , h e a t i n g , f o r k l i f t s ) could not be constructed within the limit due to complexity that can be observed from number of variables and constraints. Such big instances need more time to be compiled or more complex ordering heuristics to be applied.
Overall, with presented ordering heuristics, BDDs are much more eficient in modelling the rulesets and show promising results for use cases of knowledge compilation.
In this paper, we examined methods to enhance the construction time and size of BDDs for RCNF formulas.
We presented variable ordering and constraint ordering methods that utilize the ideas of commonly used variable ordering methods. Furthermore, we considered diferent tree construction strategies. Additionally, we discussed the application of all described methods for SDD construction using vtrees.
We evaluated heuristics on RCNF benchmarks, assessing coverage in diferent time limits and determining the best results for each configuration, and found that Modified-FORCE and FORCE can greatly improve the BDD construction time. Furthermore, we applied the variable ordering heuristics to construct balanced vtrees for SDD construction, and results showed that FORCE and Modified-FORCE result in the best decision diagram size among all configurations. [7] S. Bova, Sdds are exponentially more succinct than obdds, CoRR abs/1601.00501 (2016). URL: http:// arxiv.org/abs/1601.00501. a r X i v : 1 6 0 1 . 0 0 5 0 1 . [8] T. Hadzic, S. Subbarayan, R. M. Jensen, H. R. Andersen, J. Møller, H. Hulgaard, Fast backtrack-free product configuration using a precompiled solution space representation, in: Proceedings from the International Conference on Economic, Technical and Organisational aspects of Product Configuration Systems, Technical University of Denmark (DTU), 2004, pp. 133–140. [9] M. Rice, S. Kulhari, A survey of static variable ordering heuristics for eficient bdd/mdd construction (2008) 13. [10] F. Aloul, I. Markov, K. Sakallah, Mince: A static global variable-ordering heuristic for sat search and bdd manipulation, JOURNAL OF UNIVERSAL
COMPUTER SCIENCE 10 (2004) 1562–1596. [11] R. L. Rudell, Dynamic variable ordering for ordered binary decision diagrams, Proceedings of 1993 International Conference on Computer Aided Design (ICCAD) (1993) 42–47. [12] U. Oztok, A. Darwiche, A top-down compiler for sentential decision diagrams, in: Proceedings of the 24th International Conference on Artificial Intelligence, IJCAI’15, AAAI Press, 2015, p. 3141–3148. [13] H. R. Andersen, T. Hadzic, D. Pisinger, Interactive cost configuration over decision diagrams, Journal of Artificial Intelligence Research 37 (2010) 99–139. [14] F. A. Aloul, I. L. Markov, K. A. Sakallah, Force:
A fast and easy-to-implement variable-ordering heuristic, in: Proceedings of the 13th ACM Great Lakes Symposium on VLSI, GLSVLSI ’03, Association for Computing Machinery, New York, NY, USA, 2003, p. 116–119. URL: https://doi.org/10.1145/ 764808.764839. doi:1 0 . 1 1 4 5 / 7 6 4 8 0 8 . 7 6 4 8 3 9 . [1] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, [15] A. Choi, A. Darwiche, Dynamic minimization of L.-J. Hwang, Symbolic model checking: 1020 states sentential decision diagrams, Proceedings of the and beyond, Information and computation 98 (1992) AAAI Conference on Artificial Intelligence 27 (2013) 142–170. 187–194. URL: https://ojs.aaai.org/index.php/AAAI/ [2] D. E. Knuth, The Art of Computer Programming, article/view/8690. doi:1 0 . 1 6 0 9 / a a a i . v 2 7 i 1 . 8 6 9 0 .
Volume 4, Fascicle 1B: Binary Decision Diagrams, [16] F. Somenzi, CUDD User’s Manual, 2005. URL: Addison-Wesley Professional, 2009. http://web.mit.edu/sage/export/tmp/y/usr/share/ [3] R. E. Bryant, Binary Decision Diagrams, Springer doc/polybori/cudd/node3.html.
International Publishing, Cham, 2018, pp. 191–217. [17] A. Choi, A. Darwiche, SDD Advanced-User ManURL: https://doi.org/10.1007/978-3-319-10575-8_7. ual Version 2.0, Automated Reasoning Group Comdoi:1 0 . 1 0 0 7 / 9 7 8 - 3 - 3 1 9 - 1 0 5 7 5 - 8 _ 7 . puter Science Department University of Califor[4] D. Sieling, I. Wegener, Reduction of obdds in linear nia, 2018. URL: http://reasoning.cs.ucla.edu/sdd/ time, Inf. Process. Lett. 48 (1993) 139–144. doc/sdd-advanced-manual.pdf. [5] Bryant, Graph-based algorithms for boolean function manipulation, IEEE Transactions on Computers C-35 (1986) 677–691. doi:1 0 . 1 1 0 9 / T C . 1 9 8 6 .
1 6 7 6 8 1 9 . [6] A. Darwiche, Sdd: A new canonical representation of propositional knowledge bases, in: IJCAI, 2011.