WmcManager

class pysdd.sdd.WmcManager(SddNode node, bool log_mode=1)

Creates a WMC manager for the SDD rooted at node and initializes literal weights.

When log mode =6 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.

Note: To avoid invalidating a WMC manager, the user should refrain from performing the SDD operations like queries and transformations when auto garbage collection and SDD minimization is active. For this reason, the WMCManager will set the prevent_transformation flag on the SDDManager. This prevents transformations on the SDDManager when auto_gc_and_minize is on. When the WMCManager is not used anymore, Sddmanager.set_prevent_transformations(prevent=False) can be executed to re-allow transformations.

Background:

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 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.

literal_derivative

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.

literal_pr

Returns the probability of literal.

The result returned by this function is meaningful only after having called wmc propagate.

literal_weight

Returns the weight of a literal.

node

node: pysdd.sdd.SddNode

one_weight

Returns 0 for log-mode and 1 otherwise.

propagate

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.

set_literal_weight

Set weight of literal.

Sets the weight of a literal in the given WMC manager (should pass the natural log of the weight in log-mode).

This is a slow function, to set one or more literal weights fast use set_literal_weights_from_array.

set_literal_weights_from_array

Set all literal weights.

Expects an array of size <nb_literals>*2 which represents literals [-3, -2, -1, 1, 2, 3]

zero_weight

Returns -inf for log-mode and 0 otherwise.