From 2033e43128d5a172e20228115df1afe5508812de Mon Sep 17 00:00:00 2001 From: Josef Podany Date: Mon, 16 Dec 2024 17:45:33 +0100 Subject: [PATCH] add: docs: examples --- README.md | 2 + sddrs/README.md | 9 ++-- sddrs/examples/fragment_minimization.rs | 40 ++++++++++++++++++ sddrs/examples/input_output.rs | 33 +++++++++++++++ sddrs/examples/manual_minimization.rs | 56 +++++++++++++++++++++++++ sddrs/examples/simple.rs | 43 +++++++++++++++++++ sddrs/lib.rs | 2 + 7 files changed, 181 insertions(+), 4 deletions(-) create mode 100644 sddrs/examples/fragment_minimization.rs create mode 100644 sddrs/examples/input_output.rs create mode 100644 sddrs/examples/manual_minimization.rs create mode 100644 sddrs/examples/simple.rs diff --git a/README.md b/README.md index fa52c67..d3acf88 100644 --- a/README.md +++ b/README.md @@ -83,6 +83,8 @@ fn main() { } ``` +**See [examples](https://github.com/jsfpdn/sdd-rs/tree/main/sddrs/examples) for more examples.** + ### Binary The compiler can be also compiled and invoked as a command-line utility. diff --git a/sddrs/README.md b/sddrs/README.md index 5830bea..1218ea2 100644 --- a/sddrs/README.md +++ b/sddrs/README.md @@ -17,6 +17,8 @@ The compiler currently supports: ## Usage +**See [examples](https://github.com/jsfpdn/sdd-rs/tree/main/sddrs/examples) for more examples.** + The following snippet compiles the function `(A & B) | 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. @@ -24,14 +26,13 @@ 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"]) + .variables(&["A".to_string(), "B".to_string(), "C".to_string()]) .build(); let manager = SddManager::new(options); @@ -51,14 +52,14 @@ fn main() { println!("'(A ∧ B) ∨ C' has {model_count} models."); println!("They are:\n{models}"); - let sdd_path = "my_formula.dot" + 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 vtree_path = "my_vtree.dot"; let f = File::create(vtree_path).unwrap(); let mut b = BufWriter::new(f); manager diff --git a/sddrs/examples/fragment_minimization.rs b/sddrs/examples/fragment_minimization.rs new file mode 100644 index 0000000..01d2b0e --- /dev/null +++ b/sddrs/examples/fragment_minimization.rs @@ -0,0 +1,40 @@ +//! Example minimization of compiled knowledge via vtree fragments. + +use sddrs::{ + literal::literal::Polarity, + manager::{ + options::{self, FragmentHeuristic, GarbageCollection, MinimizationCutoff, VTreeStrategy}, + SddManager, + }, +}; + +fn main() { + let opts = options::SddOptions::builder() + .vtree_strategy(VTreeStrategy::LeftLinear) + .garbage_collection(GarbageCollection::Automatic) + .variables(&["A".to_string(), "B".to_string(), "C".to_string()]) + .build(); + let manager = SddManager::new(&opts); + + let a = manager.literal("A", Polarity::Positive).unwrap(); + let b = manager.literal("B", Polarity::Positive).unwrap(); + let c = manager.literal("C", Polarity::Positive).unwrap(); + + let conjunction = manager.conjoin(&a, &manager.conjoin(&b, &c)); + let size_before = conjunction.size(); + println!("size for right-linear: {}", size_before); + + manager + .minimize( + MinimizationCutoff::BreakAfterFirstImprovement, + &FragmentHeuristic::Root, + &conjunction, + ) + .unwrap(); + + let size_after = conjunction.size(); + println!("size after minimizing via fragments: {}", size_after); + + // Ideally, this should hold: + assert!(size_after <= size_before); +} diff --git a/sddrs/examples/input_output.rs b/sddrs/examples/input_output.rs new file mode 100644 index 0000000..7bfc405 --- /dev/null +++ b/sddrs/examples/input_output.rs @@ -0,0 +1,33 @@ +use sddrs::manager::{ + options::{self, GarbageCollection, VTreeStrategy}, + SddManager, +}; + +fn main() { + let opts = options::SddOptions::builder() + .vtree_strategy(VTreeStrategy::LeftLinear) + .garbage_collection(GarbageCollection::Automatic) + .variables(&[ + "A".to_string(), + "B".to_string(), + "C".to_string(), + "D".to_string(), + ]) + .build(); + let manager = SddManager::new(&opts); + + let dimacs = "c +p cnf 4 3 +1 3 -4 0 +4 0 +2 -3 0 +"; + let sdd = manager.from_dimacs(&mut dimacs.as_bytes()).unwrap(); + + println!("Compiled SDD in DOT Graphviz format:"); + manager.draw_sdd(&mut std::io::stdout(), &sdd).unwrap(); + + println!("\n---\nVtree in DOT Graphviz format:"); + manager.draw_vtree(&mut std::io::stdout()).unwrap(); + println!(); +} diff --git a/sddrs/examples/manual_minimization.rs b/sddrs/examples/manual_minimization.rs new file mode 100644 index 0000000..844a7b3 --- /dev/null +++ b/sddrs/examples/manual_minimization.rs @@ -0,0 +1,56 @@ +//! Example of manual minimization of compiled knowledge. +use sddrs::{ + literal::literal::Polarity, + manager::{ + options::{self, GarbageCollection, VTreeStrategy}, + SddManager, + }, +}; + +fn main() { + let opts = options::SddOptions::builder() + // x + // / \ + // A y + // / \ + // B C + .vtree_strategy(VTreeStrategy::RightLinear) + .garbage_collection(GarbageCollection::Automatic) + .variables(&["A".to_string(), "B".to_string(), "C".to_string()]) + .build(); + let manager = SddManager::new(&opts); + + let a = manager.literal("A", Polarity::Positive).unwrap(); + let b = manager.literal("B", Polarity::Positive).unwrap(); + let c = manager.literal("C", Polarity::Positive).unwrap(); + + // A && B && C + let conjunction = manager.conjoin(&a, &manager.conjoin(&b, &c)); + println!("size for right-linear: {}", conjunction.size()); + + // Rotate 'x' to obtain this vtree: + // x + // / \ + // y C + // / \ + // A B + manager + .rotate_left(&manager.root().right_child().unwrap()) + .unwrap(); + println!( + "size after rotating 'x' to the left: {}", + conjunction.size() + ); + + // Swap children of 'y' to obtain this vtree: + // x + // / \ + // y C + // / \ + // B A + manager.swap(&manager.root().left_child().unwrap()).unwrap(); + println!( + "size after swapping children of 'y': {}", + conjunction.size() + ); +} diff --git a/sddrs/examples/simple.rs b/sddrs/examples/simple.rs new file mode 100644 index 0000000..1e50fda --- /dev/null +++ b/sddrs/examples/simple.rs @@ -0,0 +1,43 @@ +//! Example of simple knowledge compilation. +use sddrs::{ + literal::literal::Polarity, + manager::{ + options::{self, GarbageCollection, VTreeStrategy}, + SddManager, + }, +}; + +fn main() { + let opts = options::SddOptions::builder() + .vtree_strategy(VTreeStrategy::RightLinear) + .garbage_collection(GarbageCollection::Automatic) + .variables(&["A".to_string(), "B".to_string(), "C".to_string()]) + .build(); + + let manager = SddManager::new(&opts); + + let a = manager.literal("A", Polarity::Positive).unwrap(); + let n_b = manager.literal("B", Polarity::Negative).unwrap(); + let c = manager.literal("C", Polarity::Positive).unwrap(); + + // A && !B + let fst = manager.conjoin(&a, &n_b); + assert_eq!(manager.model_count(&fst), 2); + println!("A && !B:\n{}\n", manager.model_enumeration(&fst)); + + // C => (A && !B) + let snd = manager.imply(&c, &fst); + assert_eq!(manager.model_count(&snd), 5); + println!("C => (A && !B):\n{}\n", manager.model_enumeration(&snd)); + + // !(C => (A && !B)) + let n_snd = manager.negate(&snd); + assert_eq!(manager.model_count(&n_snd), 3); + println!("!(C => A && !B):\n{}\n", manager.model_enumeration(&n_snd)); + + // (C => (A && !B)) <=> !(C => (A && !B)) == False + let ff = manager.equiv(&snd, &n_snd); + assert_eq!(manager.model_count(&ff), 0); + assert!(ff.is_false()); + println!("False:\n{}\n", manager.model_enumeration(&ff)); +} diff --git a/sddrs/lib.rs b/sddrs/lib.rs index 5a4f07f..3cd9c2d 100644 --- a/sddrs/lib.rs +++ b/sddrs/lib.rs @@ -11,6 +11,8 @@ //! * 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. //! +//! **See [examples](https://github.com/jsfpdn/sdd-rs/tree/main/sddrs/examples) for more examples.** +//! //! The following snippet compiles the function `(A ∧ B) ∨ C` to 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.