Just a memo about ZDD

[shnarazk]

fn solve(cnf: &CNF) -> Certificate {
    match solve_(cnf) {
         Ok(c)|Err(c) => c,
    }
}
fn solve_(cnf: &CNF) -> Result<Certificate, Certificate> {
    let mut a_graph: ZDD;
    while let partial_assignment = a_graph.is_equivalent_to(cnf, oracle)? {
        a_graph.add(!partial_assignment);
    }
    Ok(Certificate::UNSAT)
}

• the given cnf is a shared reference because we will not add learnt clauses.

• ZDD is a mutable reference but we can merge its variations by thread join.

• we need to store some extra properties, such as activity or phase, on vars.

• we could get some nice properties from ZDD itself.

• I'm not trying to represent CNF as ZDD which is over 1M cascaded decisions. This is an alternative representation for learnt clauses. It's nice that both of knowledge acquired by conflict learning and the problem itself have the same representation. But this does not mean we have to choose it.