Creation of Boolean Variables as ZBDDs

[sirandreww]

I'm working with ZDDs using this library and I'm noticing the following issue:

    let inner_node_capacity = 1 << 20;
    let apply_cache_capacity = 1 << 20;
    let threads = 1;

    let manager_ref: oxidd::zbdd::ZBDDManagerRef =
        oxidd::zbdd::new_manager(inner_node_capacity, apply_cache_capacity, threads);

    let a =
        manager_ref.with_manager_exclusive(|manager| ZBDDFunction::new_singleton(manager).unwrap());
    let b =
        manager_ref.with_manager_exclusive(|manager| ZBDDFunction::new_singleton(manager).unwrap());
    let x =
        manager_ref.with_manager_exclusive(|manager| ZBDDFunction::new_singleton(manager).unwrap());

    let def = a.and(&b).unwrap().equiv(&x).unwrap();

    let r = def.and(&x).unwrap().and(&a).unwrap();

    debug_assert!(r.satisfiable());

I'm defining 3 variables a, b, x and I'm defining x to be the result of a ^ b (x = a && b). Then I'm checking the result of the SAT query x && a and it is not SAT? (The assert fails). Am I somehow using the library incorrectly?

Version

oxidd = "0.7.0"

[nhusung]

You seem to be confusing singleton sets and Boolean variable functions. The variable a in your code snippet corresponds to the singleton set {a}, i.e., the Boolean function a ∧ ¬b ∧ ¬x. r is def ∧ (¬a ∧ ¬b ∧ x) ∧ (a ∧ ¬b ∧ ¬x) = ⊥.

For your use case, you first need to create the singleton sets (to make the decision diagram have three levels), and then construct the Boolean functions representing the variables. I just noticed that I did not really expose the functionality on ZBDDFunction, I’ll leave this issue open until that is fixed. Until then, you may want to use the following helper function

/// Returns a pair `(singletons, boolean_vars)`. Each of the returned `Vec`s contains `n` elements.
fn zbdd_singletons_vars(mref: &ZBDDManagerRef, n: usize) -> (Vec<ZBDDFunction>, Vec<ZBDDFunction>) {
    let singletons: Vec<ZBDDFunction> = mref.with_manager_exclusive(|manager| {
        (0..n)
            .map(|_| ZBDDFunction::new_singleton(manager).unwrap())
            .collect()
    });
    let vars = mref.with_manager_shared(|manager| {
        singletons
            .iter()
            .map(|s| {
                ZBDDFunction::from_edge(
                    manager,
                    oxidd::zbdd::var_boolean_function(manager, s.as_edge(manager)).unwrap(),
                )
            })
            .collect()
    });
    (singletons, vars)
}

You can use this as follows:

let (_, vars) = zbdd_singletons_vars(manager_ref);
let a = &vars[0];
let b = &vars[1];
let x = &vars[2];

Directly calling ZBDDFunction::new_var() three times after another would mean that all the functions have different domains, which is not what you want. This is currently somewhat inconvenient and will probably be improved in one of the next releases.

[sirandreww]

Can you provide me with a resource that explains this set representation with ZDDs? What does the function var_boolean_function

I'm working in an environment where I am building a circuit incrementally depending on some unknown heuristic, so the number of variables that I will be using is not known to me at all. I need to be able to add variables to the ZDDs according to my needs "on the fly". Do you think this function would work? Is there a reason that I need to keep the singleton sets?

   fn get_new_variable(mref: &ZBDDManagerRef) -> ZBDDFunction {
        mref.with_manager_exclusive(|manager| {
            let s = ZBDDFunction::new_singleton(manager).unwrap();
            ZBDDFunction::from_edge(
                manager,
                oxidd::zbdd::var_boolean_function(manager, s.as_edge(manager)).unwrap(),
            )
        })
    }