neuppl / rsdd Goto Github PK

Add a swap method to the BddBuilder trait:

pub trait BddBuilder<'a>: BottomUpBuilder<'a, BddPtr<'a>> {
   /// swaps variables `a` and `b` in the variable order.
   /// all pointers into the manager are invalidated. 
   /// returns a new manager and root list, where the order of roots in the returned list 
   /// matches the order provided by `roots.`
   fn swap(manager: BddManger<'a>, roots: Vec<BddPtr<'a>, a: VarLabel, b: VarLabel) -> (Manager<'b>, Vec<BddPtr<'b>>;

   /// reorders all BDDs to have the order `order`.
   /// all pointers into the manager are invalidated. 
   /// returns a new manager and root list, where the order of roots in the returned list 
   /// matches the order provided by `roots.`
   fn reorder(manager: BddManger<'a>, roots: Vec<BddPtr<'a>, order: VarOrder) -> (Manager<'b>, Vec<BddPtr<'b>>;
}

• Swapping adjacent variables in a BDD is efficient. Swapping two arbitrary variables can be accomplished by repeated swapping of adjacent variables.
• Here is a document visualizing swapping and describing how to efficiently implement it:
  variable-swap.pdf
• reorder should be implemented in terms of swap.
• This is blocked by #154.

Add a /bin/ directory that organizes the following main binaries for interacting with the library.

• bottomup_cnf_to_bdd: takes as input a CNF and outputs a BDD.
  • Input argument: CNF file
    • DIMACS format
    • JSON format
  • Input argument: order, specifies a variable order:
    • default: auto_minfill: use a min-fill heuristic to find the variable ordering
    • auto_force: use the FORCE heuristic to find a variable ordering
    • manual: provide a manual variable order as a JSON file
  • Input argument: strategy, specifies a compilation order (i.e., a tree describing the sequence in which clauses are conjoined together)
    • default: dtree, uses the dtree decomposition of the CNF according to the variable order
  • Input argument: verbose, show verbose output (timing information, hash table information, etc.)
  • Input argument: progress, show a progress bar that gives an estimate of compilation progress (fraction of compiled clauses)
• bottomup_formula_to_bdd: takes as input an arbitrary logical formula and outputs a BDD.
  • Input argument: formula file (in SEXPR JSON format)
  • Input argument: ordering
    • Default: manual, must provide a manual variable order.
    • interaction_minfill: user provides an interaction graph between variables and minfill is run to extract a good variable order
• bottomup_cnf_to_sdd: same as for BDD
• bottomup_formula_to_sdd: same as for BDD
• cnf_to_ddnnf: compiles a d-DNNF from a CNF
  • Input: a CNF file
  • Input: order, specifies a variable ordering strategy
    • Default: static_minfill, follows a static variable ordering based on the minfill heuristic on the graph
    • static_manual, user provides a manual static variable ordering
• weighted_model_count: takes as input a compiled circuit and weight file and outputs the resulting weighted model count
  • Input: circuit, either a dDNNF, SDD, or BDD
  • Input: semiring, choice of semiring under which to perform the computation
    • Either f64 or rational for now; more to come later
  • Input: weights A JSON file describing the weights (a dictionary mapping literals to weights)

Bug:

When doing a ternary And with the RSDD CLI, RSDD only considers the first two arguments in the conjunction, and ignores the third. This is the case for all n-ary operations with n>2.

Repro Steps:

Command:

cargo run --release --bin weighted_model_count --features="cli" -- -f minimal_example.sexp -w minimal_example_weights.json

‌

minimal_example.sexp:

(And (Not (Var T0)) (Not (Var T1)) (Not (Var T2)))

‌

minimal_example_weights.json:

{"T0": { "low": 0.9, "high": 0.1}, "T1": { "low": 0.9, "high": 0.1}, "T2": { "low": 0.9, "high": 0.1}}

‌

Outputs:

Expected Output:

unweighted model count: 1
weighted model count: 0.729

Actual Output:

unweighted model count: 2
weighted model count: 0.81

‌

Notes:

There is a workaround to this issue that you can just do nesting of binary conjunctions. For example using the following formula file.

minimal_example_workaround.sexp:

(And (Not (Var T0)) (And (Not (Var T1)) (Not (Var T2))))

This is fine, but RSDD should at least error on invalid input instead of giving an incorrect output.

Jotting this down so I don't forget - we should try to cache our cargo dependencies so that our CI build times are shorter.

Coupe thoughts:

• might be a good idea to commit Cargo.lock
• seems like there's no first-party GitHub Action for this - https://github.com/Swatinem/rust-cache seems like a good start
• this blog post seems to indicate that there are some other microoptimizations we could look at, most notably https://github.com/nextest-rs/nextest - but I think we can table that until later

Updating this to be a tracking issue for the standardized import/export of all the main datastructures within the library.

All these import/export tools can be found in src/serialize/

• Serialize/Deserialize BDD
• Serialize/Deserialize SDD
• Serialize/Deserialize d-DNNF
• Serialize/Deserialize VTRee
• Serialize/Deserialize DTree
• Serialize/Deserialize Interaction Graph
• Serialize/Deserialize weighted model counting parameters

In addition to serializing/deserializing these data structures, it's necessary to be able to load them into the relevant builder/manager. Here we track these workflows:

• Import/Export BDD from builder
• Import/Export SDD from builder
• import/Export d-DNNF from builder

Bug:

RSDD CLI is generating a non-reduced BDD with duplicate leaves/redundant nodes. We suspect this is leading to a noticeable performance loss in runtime of programs using larger BDDs. It is unclear if this issue is in the CLI only, or if it is in the core RSDD code.

Repro Steps:

(1) Add print statement to weighted_model_count.rs code to get printed BDD output

Here is the change as a git diff to main branch at commit sha `39aadfb`:

diff --git a/bin/weighted_model_count.rs b/bin/weighted_model_count.rs
index e2359d4..a482696 100644
--- a/bin/weighted_model_count.rs
+++ b/bin/weighted_model_count.rs
@@ -155,6 +155,7 @@ fn single_wmc(
     let bdd = builder.smooth(bdd, num_vars);

     let res = bdd.unsmoothed_wmc(&params);
+ println!("{}", bdd.to_string_debug());

     let elapsed = start.elapsed();

(2) Run RSDD CLI

Command:

cargo run --release --bin weighted_model_count --features="cli" -- -f minimal_example.sexp -w minimal_example_weights.json

‌

minimal_example.sexp:

(And (Var T0) (Var T1))

‌

minimal_example_weights.json:

{"T0": { "low": 0.9, "high": 0.1}, "T1": { "low": 0.9, "high": 0.1}}

‌

Outputs:

Expected Output:

(0, (1, T, F))
unweighted model count: 1
weighted model count: 0.01

Actual Output:

(0, (1, T, F), (1, F, F))
unweighted model count: 1
weighted model count: 0.010000000000000002

Currently all nodes that are allocated by the bottom-up managers are never deallocated. This issue establishes a garbage collection interface for collecting unused nodes. It adds the following method to the BottomUpBuilder trait:

pub trait BottomUpBuilder<'a, Ptr> {
    ...
    /// garbage collects all nodes in the builder.
    /// only the roots provided in the `roots` argument are guaranteed to be preserved. 
    /// Roots may be moved during garbage collection; these new roots are returned in the 
    /// same order in which they were provided.
    fn collect(&'a self, roots: Vec<Ptr>) -> Vec<Ptr>
}

This issue involves scoping and implementing the garbage collecting strategy. Design considerations:

• Ideally, we should not simply garbage collect all nodes that are not referenced. It's often the case that nodes that are used once are often used again.
• Ideally, we should try to preserve as much of the apply cache as possible. We should study what cudd does and see how they manage to do it.
• This API needs to be able to handle lifetimes. All references to pointers should become invalidated after collection (since they can all be moved). Ideally this is maintained at the type signature level. The above API does not do this; we will need to experiment and think about this. Hopefully it does not require adding a trait-level lifetime to the Ptr trait, but it might.

Motivated from a conversation with Lisa: on top of model counting with .wmc(), it would be moderately useful to list out all valid models that satisfy a logical formula, and (optionally) the associated weights with each model.

Since this is computationally hard, we should do this on-demand only from the user. We can probably use the existing PartialModel struct; we could then return a tuple for each model, which contains both the assignments for each variable, and the associated weight.

I'm thinking something that looks like this:

let weights = WmcParams::new(/* ... */);
let formula: DDNNFPtr = builder.compile_cnf(); // can be whatever approach we'd prefer
let valid_models: ValidModels = formula.enumerate_models(&order, &weights);
for model in valid_models {
  println!("weight: {}, assignments: {}", model.weight(), model.assignments())
}