SddManager¶
-
class
pysdd.sdd.
SddManager
(long var_count=1, bool auto_gc_and_minimize=False, Vtree vtree=None)¶ Creates a new SDD manager, either given a vtree or using a balanced vtree over the given number of variables.
Parameters: - var_count – Number of variables
- auto_gc_and_minimize – Automatic garbage collection Automatic garbage collection and automatic SDD minimization are activated in the created manager when auto gc and minimize is not 0.
- 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.
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 [10]. For a discussion on the design and implementation of such systems, see [7].
To declare an SDD manager, one provides an initial vtree. By declaring an initial vtree, we also declare an initial number of 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 i and its negative literal by −i.
-
add_var_after
¶ 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 right sibling of leaf v.
-
add_var_after_last
¶ Let v be the rightmost leaf node in the vtree. A new leaf node labeled with variable n + 1 is created and made a right sibling of leaf v.
-
add_var_after_lca
¶ Let v be the smallest vtree which contains the variables of literals, where count is the number of literals. A new leaf node labeled with variable n + 1 is created and made a right sibling of v.
-
add_var_before
¶ 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 sibling of leaf v.
-
add_var_before_first
¶ Let v be the leftmost leaf node in the vtree. A new leaf node labeled with variable n + 1 is created and made a left sibling of leaf v.
-
add_var_before_lca
¶ Let v be the smallest vtree which contains the variables of literals, where count is the number of literals. A new leaf node labeled with variable n + 1 is created and made a left sibling of v.
-
apply
¶ Returns the result of combining two SDDs, where op can be CONJOIN (0) or DISJOIN (1).
-
auto_gc_and_minimize_off
¶ Deactivates automatic garbage collection and automatic SDD minimization.
-
auto_gc_and_minimize_on
¶ Activates automatic garbage collection and automatic SDD minimization.
-
condition
¶ Returns the result of conditioning an SDD on a literal, where a literal is a positive or negative integer.
-
conjoin
¶ Returns the result of applying the corresponding Boolean operation on the given SDDs.
-
copy
¶ Returns a new SDDManager, while copying the vtree and the SDD nodes of this manager. After this operation, the given list of nodes will contain the corresponding nodes in the new manager. :param nodes: A list of SddNodes to copy. :return: The new SDDManager
-
count
¶ Returns the node count of all SDD nodes in the manager.
-
dead_count
¶ Returns the node count of all dead SDD nodes in the manager.
-
dead_size
¶ Returns the size of all dead SDD nodes in the manager.
-
disjoin
¶ Returns the result of applying the corresponding Boolean operation on the given SDDs.
-
dot
¶ SDD for the given node, formatted for use with Graphviz dot.
Shared SDD, formatted for use with Graphviz dot.
-
exists
¶ Returns the result of existentially (universally) quantifying out a variable from an SDD.
-
exists_multiple
¶ Returns the result of existentially quantifying out a set of variables from an SDD.
This function is expected to be more efficient than existentially quantifying out variables one at a time. The array exists map specifies the variables to be existentially quantified out. The length of exists map is expected to be n + 1, where n is the number of variables in the manager. exists map[i] should be 1 if variable i is to be quantified out; otherwise, exists map[i] should be 0. exists map[0] is unused.
-
exists_multiple_static
¶ This is the same as sdd exists multiple, except that SDD minimization is never performed when quantifying out variables.
This can be more efficient than deactivating automatic SDD minimization and calling sdd exists multiple.
A model of an SDD is a truth assignment of the SDD variables which also satisfies the SDD. The cardinality of a truth assignment is the number of variables assigned the value true. An SDD may not mention all variables in the SDD manager. An SDD model can be converted into a global model by including the missing variables, while setting their values arbitrarily.
-
false
¶ Returns an SDD representing the function false.
-
fnf_to_sdd
¶
-
forall
¶ Returns the result of existentially (universally) quantifying out a variable from an SDD.
-
from_cnf_file
¶ Create an SDD from the given CNF file.
-
from_cnf_string
¶ Create an SDD from the given CNF string.
-
from_dnf_file
¶ Create an SDD from the given DNF file.
-
from_dnf_string
¶ Create an SDD from the given DNF string.
-
from_fnf
¶ Create an SDD from the given DNF file.
-
from_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.
-
garbage_collect
¶ Performs a global garbage collection: Claims all dead SDD nodes in the manager.
-
get_vars
¶
-
global_minimize_cardinality
¶ Returns the SDD whose models are the minimum-cardinality global models of the given SDD (i.e., with respect to the manager variables).
-
global_model_count
¶ Returns the global model count of an SDD (i.e., with respect to the manager variables).
-
init_vtree_size_limit
¶ Declares the size s of current SDD for vtree as the reference size for the relative size limit l.
That is, a rotation or swap operation will fail if the SDD size grows to larger than s × l.
-
is_auto_gc_and_minimize_on
¶ Is automatic garbage collection and automatic SDD minimization activated?
-
is_prevent_transformation_on
¶ Are transformations prevented when self.is_auto_gc_and_minimize_on()=True?
-
is_var_used
¶ Returns 1 if var is referenced by a decision SDD node (dead or alive); returns 0 otherwise.
Parameters: var – Literal (number)
-
l
¶ Short for literal(lit)
-
lca_of_literals
¶ 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.
-
literal
¶ Returns an SDD representing a literal.
Returns an SDD representing a literal. The variable literal is of the form ±i, where i 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.
Parameters: lit – Literal (integer number)
-
live_count
¶ Returns the node count of all live SDD nodes in the manager.
-
live_size
¶ Returns the size of all live SDD nodes in the manager.
-
minimize
¶ Performs global garbage collection and then tries to minimize the size of a manager’s SDD.
This function calls sdd vtree search on the manager’s vtree.
To allow for a timeout, this function can be interrupted by the keyboard interrupt (SIGINT).
-
minimize_cardinality
¶ Returns the SDD whose models are the minimum-cardinality models of the given SDD (i.e. with respect to the SDD variables).
-
minimize_limited
¶
-
minimum_cardinality
¶ Returns the minimum-cardinality of an SDD.
The smallest cardinality attained by any of its models. The minimum-cardinality of an SDD is the same whether or not we consider the global models of the SDD.
-
model_count
¶ Returns the model count of an SDD (i.e., with respect to the SDD variables).
-
move_var_after
¶ Let v be the vtree leaf node labeled with variable target var. The leaf node labeled with variable var is moved to become a right sibling of leaf v.
-
move_var_after_last
¶ Let v be the rightmost leaf node in the vtree. The leaf node labeled with variable var is moved to become a right sibling of leaf v.
-
move_var_before
¶ Let v be the vtree leaf node labeled with variable target var. The leaf node labeled with variable var is moved to become a left sibling of leaf v.
-
move_var_before_first
¶ Let v be the leftmost leaf node in the vtree. The leaf node labeled with variable var is moved to become a left sibling of leaf v.
-
negate
¶ Returns the result of applying the corresponding Boolean operation on the given SDDs.
-
print_stdout
¶
-
read_cnf_file
¶ Replace the SDD by an SDD representing the theory in the given CNF file.
-
read_dnf_file
¶ Replace the SDD by an SDD representing the theory in the given DNF file.
-
read_sdd_file
¶ Reads an SDD from file.
The 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.
-
remove_var_added_last
¶ Let v be the vtree leaf node with the variable that was added last to the vtree. This leaf is removed from the vtree.
-
rename_variables
¶ 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 <= i <= n, that appears in the given SDD is renamed into variable variable_map[i] (variable_map[0] is not used).
-
root
¶ root: object
-
save
¶ 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.
-
save_as_dot
¶ Saves an SDD to file, formatted for use with Graphviz dot.
-
set_options
¶
-
set_prevent_transformation
¶ Prevent transformations when prevent=True and self.is_auto_gc_and_minimize_on()=True
-
set_vtree_apply_time_limit
¶ Set the time limits for the vtree search algorithm.
A vtree operation is either a rotation or a swap. Times are in seconds and correspond to CPU time. Default values, in order, are 180, 60, 30, and 10 seconds.
-
set_vtree_cartesian_product_limit
¶ Sets the absolute size limit on the size of a cartesian product for right rotation and swap operations.
Default value is 8, 192.
-
set_vtree_fragment_time_limit
¶ Set the time limits for the vtree search algorithm.
A vtree operation is either a rotation or a swap. Times are in seconds and correspond to CPU time. Default values, in order, are 180, 60, 30, and 10 seconds.
-
set_vtree_operation_memory_limit
¶ Sets the relative memory limit for rotation and swap operations. Default value is 3.0.
-
set_vtree_operation_size_limit
¶ Sets the relative size limit for rotation and swap operations.
Default value is 1.2. A size limit l is relative to the size s of an SDD for a given vtree (s is called the reference size). Hence, using this size limit requires calling the following functions to set and update the reference size s, otherwise the behavior is not defined.
-
set_vtree_operation_time_limit
¶ Set the time limits for the vtree search algorithm.
A vtree operation is either a rotation or a swap. Times are in seconds and correspond to CPU time. Default values, in order, are 180, 60, 30, and 10 seconds.
-
set_vtree_search_convergence_threshold
¶
-
set_vtree_search_time_limit
¶ Set the time limits for the vtree search algorithm.
A vtree operation is either a rotation or a swap. Times are in seconds and correspond to CPU time. Default values, in order, are 180, 60, 30, and 10 seconds.
Saves the SDD of the manager’s vtree (a shared SDD), formatted for use with Graphviz dot.
-
size
¶ Returns the size of all SDD nodes in the manager.
-
true
¶ Returns an SDD representing the function true.
-
update_vtree_size_limit
¶ Updates the reference size for relative size limits.
It is preferrable to invoke this function, as it is more efficent than the function sdd manager init vtree size limit as it does not directly recompute the size of vtree.
-
var_count
¶ Returns the number of SDD variables currently associated with the manager.
-
var_order
¶ Return an array var order (whose length will be equal the number of variables in the manager) with the left-to-right variable ordering of the manager’s vtree.
-
vtree
¶
-
vtree_copy
¶
-
vtree_minimize
¶ Performs local garbage collection on vtree and then tries to minimize the size of the SDD of vtree by searching for a different vtree. Returns the root of the resulting vtree.
-
vtree_of_var
¶ Returns the leaf node of a manager’s vtree, which is associated with var.