diff --git a/Cargo.toml b/Cargo.toml index f0384c8..e30e0ca 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,5 +1,5 @@ [workspace] -members = ["bin", "benchmarks", "sdd-rs-lib"] +members = ["bin", "benchmarks", "sddrs"] resolver = "2" [workspace.lints.rust] diff --git a/bin/Cargo.toml b/bin/Cargo.toml index 2ba09d1..8c604b5 100644 --- a/bin/Cargo.toml +++ b/bin/Cargo.toml @@ -1,6 +1,21 @@ [package] name = "sddrsc" edition = "2021" +license = "BSD-3-Clause" +authors = ["Josef Podany"] +repository = "https://github.com/jsfpdn/sdd-rs" +description = "Bottom-up Sentential Decision Diagram compiler." +keywords = [ + "knowledge-compilation", + "boolean-functions", + "sentential-decision-diagrams", +] +categories = [ + "compilers", + "data-structures", + "mathematics", + "command-line-utilities", +] [[bin]] name = "sddrsc" @@ -10,7 +25,7 @@ path = "main.rs" tracing-subscriber = "0.3" tracing = "0.1" clap = { version = "4.5.4", features = ["derive"] } -sddrs = { path = "../sdd-rs-lib" } +sddrs = { path = "../sddrs" } anyhow = "1.0" [lints] diff --git a/sdd-rs-lib/Cargo.toml b/sddrs/Cargo.toml similarity index 62% rename from sdd-rs-lib/Cargo.toml rename to sddrs/Cargo.toml index 7d80553..0d87792 100644 --- a/sdd-rs-lib/Cargo.toml +++ b/sddrs/Cargo.toml @@ -2,9 +2,18 @@ name = "sddrs" version = "0.1.0" edition = "2021" -authors = ["josef podany"] +authors = ["Josef Podany"] repository = "https://github.com/jsfpdn/sdd-rs" -description = "Bottom-up sentential decision diagram compiler library." +description = "Bottom-up Sentential Decision Diagram compiler library." +keywords = [ + "knowledge-compilation", + "boolean-functions", + "sentential-decision-diagrams", + "model-counting", + "satisfiability", +] +categories = ["compilers", "data-structures", "mathematics"] +license = "BSD-3-Clause" [lib] name = "sddrs" diff --git a/sddrs/README.md b/sddrs/README.md new file mode 100644 index 0000000..b61976f --- /dev/null +++ b/sddrs/README.md @@ -0,0 +1,82 @@ +# :books: sddrs: Bottom-Up Sentential Decision Diagram Compiler + +**Incrementally build, manipualate, and optimize +[Sentential Decision Diagrams (SDD)](https://en.wikipedia.org/wiki/Sentential_decision_diagram): +a succinct representation of Boolean functions.** + +## :tada: Features + +The compiler currently supports: + +* incremental compilation of Boolean functions (knowledge bases) to *compressed* and *trimmed* SDDs, +* efficient querying of model count, model enumeration, and equivalence of SDDs, +* dynamic minimization of SDDs via *vtree fragments*, +* garbage collection of dead nodes, +* SDD compilation from CNF in + [DIMACS](https://www21.in.tum.de/~lammich/2015_SS_Seminar_SAT/resources/dimacs-cnf.pdf) format. + +## :package: Usage + +Then import the crate, initialize an `SddManager` and compile Boolean functions! +The following snippet compiles the function $(A \land B) \lor C$ to an SDD, +computes number of its models, enumerates and prints them to the stdout, +and renders the compiled SDD and its vtree to the DOT format. + +```rust +use sddrs::manager::{options, GCStatistics, SddManager}; +use sddrs::literal::literal::Polarity; +use bon::arr; + +fn main() { + let options = options::SddOptions::builder() + // Create right-linear vtree. + .vtree_strategy(options::VTreeStragey::RightLinear) + // Initialize the manager with variables A, B, and C. + .variables(["A".to_string(), "B".to_string(), "C"]) + .build(); + let manager = SddManager::new(options); + + // Retrieve SDDs for literals A, B, and C. + let a = manager.literal("A", Polarity::Positive).unwrap(); + let b = manager.literal("B", Polarity::Positive).unwrap(); + let c = manager.literal("C", Polarity::Positive).unwrap(); + + // Compute "A ∧ B" + let a_and_b = manager.conjoin(&a, &b); + // Compute "(A ∧ B) ∨ C" + let a_and_b_or_c = manager.disjoin(&a_and_b, &c); + + let model_count = manager.model_count(&a_and_b_or_c); + let models = manager.model_enumeration(&a_and_b_or_c); + + println!("'(A ∧ B) ∨ C' has {model_count} models."); + println!("They are:\n{models}"); + + let sdd_path = "my_formula.dot" + let f = File::create(sdd_path).unwrap(); + let mut b = BufWriter::new(f); + manager + .draw_sdd(&mut b as &mut dyn std::io::Write, &sdd) + .unwrap(); + + let vtree_path = "my_vtree.dot" + let f = File::create(vtree_path).unwrap(); + let mut b = BufWriter::new(f); + manager + .draw_vtree(&mut b as &mut dyn std::io::Write) + .unwrap(); + + println!("Rendered SDD to '{sdd_path}' and vtree to '{vtree_path}'"); +} +``` + +## :page_with_curl: Related Links + +* [SDD: A New Canonical Representation of Propositional Knowledge Bases - Adnad Darwiche](http://reasoning.cs.ucla.edu/fetch.php?id=121&type=pdf): + paper introducing SDDs +* [Dynamic Minimization of Sentential Decision Diagrams - Arthur Choi and Adnan Darwiche](http://reasoning.cs.ucla.edu/fetch.php?id=128&type=pdf): + paper describing dynamic minimization of SDDs +* [SDD: A New Canonical Representation of Propositional Knowledge Bases – Adnan Darwiche (YouTube tutorial)](https://www.youtube.com/watch?v=_5Estmve91o) +* [Bottom-Up Knowledge Compilers – Adnan Darwiche (YouTube tutorial)](https://www.youtube.com/watch?v=8yZapazT9Ls) +* [The SDD Package homepage](http://reasoning.cs.ucla.edu/sdd/): homepage of the original C SDD compiler +* [RSDD](https://github.com/neuppl/rsdd): alternative implementation of SDD in Rust diff --git a/sdd-rs-lib/dot_writer/dot_writer.rs b/sddrs/dot_writer/dot_writer.rs similarity index 100% rename from sdd-rs-lib/dot_writer/dot_writer.rs rename to sddrs/dot_writer/dot_writer.rs diff --git a/sdd-rs-lib/dot_writer/mod.rs b/sddrs/dot_writer/mod.rs similarity index 100% rename from sdd-rs-lib/dot_writer/mod.rs rename to sddrs/dot_writer/mod.rs diff --git a/sdd-rs-lib/lib.rs b/sddrs/lib.rs similarity index 100% rename from sdd-rs-lib/lib.rs rename to sddrs/lib.rs diff --git a/sdd-rs-lib/literal/literal.rs b/sddrs/literal/literal.rs similarity index 100% rename from sdd-rs-lib/literal/literal.rs rename to sddrs/literal/literal.rs diff --git a/sdd-rs-lib/literal/manager.rs b/sddrs/literal/manager.rs similarity index 100% rename from sdd-rs-lib/literal/manager.rs rename to sddrs/literal/manager.rs diff --git a/sdd-rs-lib/literal/mod.rs b/sddrs/literal/mod.rs similarity index 100% rename from sdd-rs-lib/literal/mod.rs rename to sddrs/literal/mod.rs diff --git a/sdd-rs-lib/manager/dimacs.rs b/sddrs/manager/dimacs.rs similarity index 100% rename from sdd-rs-lib/manager/dimacs.rs rename to sddrs/manager/dimacs.rs diff --git a/sdd-rs-lib/manager/manager.rs b/sddrs/manager/manager.rs similarity index 100% rename from sdd-rs-lib/manager/manager.rs rename to sddrs/manager/manager.rs diff --git a/sdd-rs-lib/manager/mod.rs b/sddrs/manager/mod.rs similarity index 100% rename from sdd-rs-lib/manager/mod.rs rename to sddrs/manager/mod.rs diff --git a/sdd-rs-lib/manager/model.rs b/sddrs/manager/model.rs similarity index 97% rename from sdd-rs-lib/manager/model.rs rename to sddrs/manager/model.rs index 7a93227..799a8e7 100644 --- a/sdd-rs-lib/manager/model.rs +++ b/sddrs/manager/model.rs @@ -32,7 +32,7 @@ impl Models { impl Display for Models { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let mut builder = Builder::default(); - builder.push_record(self.variables.iter().map(|v| v.label())); + builder.push_record(self.variables.iter().map(Variable::label)); for model in &self.models { builder.push_record( diff --git a/sdd-rs-lib/manager/options.rs b/sddrs/manager/options.rs similarity index 100% rename from sdd-rs-lib/manager/options.rs rename to sddrs/manager/options.rs diff --git a/sdd-rs-lib/sdd/decision.rs b/sddrs/sdd/decision.rs similarity index 100% rename from sdd-rs-lib/sdd/decision.rs rename to sddrs/sdd/decision.rs diff --git a/sdd-rs-lib/sdd/element.rs b/sddrs/sdd/element.rs similarity index 100% rename from sdd-rs-lib/sdd/element.rs rename to sddrs/sdd/element.rs diff --git a/sdd-rs-lib/sdd/mod.rs b/sddrs/sdd/mod.rs similarity index 100% rename from sdd-rs-lib/sdd/mod.rs rename to sddrs/sdd/mod.rs diff --git a/sdd-rs-lib/sdd/sdd.rs b/sddrs/sdd/sdd.rs similarity index 100% rename from sdd-rs-lib/sdd/sdd.rs rename to sddrs/sdd/sdd.rs diff --git a/sdd-rs-lib/sdd/sdd_ref.rs b/sddrs/sdd/sdd_ref.rs similarity index 100% rename from sdd-rs-lib/sdd/sdd_ref.rs rename to sddrs/sdd/sdd_ref.rs diff --git a/sdd-rs-lib/util.rs b/sddrs/util.rs similarity index 100% rename from sdd-rs-lib/util.rs rename to sddrs/util.rs diff --git a/sdd-rs-lib/vtree/fragment.rs b/sddrs/vtree/fragment.rs similarity index 100% rename from sdd-rs-lib/vtree/fragment.rs rename to sddrs/vtree/fragment.rs diff --git a/sdd-rs-lib/vtree/mod.rs b/sddrs/vtree/mod.rs similarity index 100% rename from sdd-rs-lib/vtree/mod.rs rename to sddrs/vtree/mod.rs diff --git a/sdd-rs-lib/vtree/vtree.rs b/sddrs/vtree/vtree.rs similarity index 100% rename from sdd-rs-lib/vtree/vtree.rs rename to sddrs/vtree/vtree.rs