Skip to content

Commit

Permalink
allow all cliques in output
Browse files Browse the repository at this point in the history
  • Loading branch information
timbeurskens committed Mar 13, 2022
1 parent b3581fd commit b845312
Show file tree
Hide file tree
Showing 3 changed files with 41 additions and 34 deletions.
2 changes: 1 addition & 1 deletion Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[package]
name = "rsbdd"
version = "0.5.0"
version = "0.5.1"
edition = "2021"

# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
Expand Down
71 changes: 39 additions & 32 deletions examples/max_clique_gen.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ fn main() -> io::Result<()> {
(@arg input: -i --input +takes_value "Input file (graph in csv edge-list format)")
(@arg output: -o --output +takes_value "The output file")
(@arg undirected: -u --undirected !takes_value "Use undirected edges (test for both directions in the set complement operation)")
(@arg all: -a --all !takes_value "Construct a BDD satisfying all cliques, not just the maximum clique(s)")
)
.get_matches();

Expand Down Expand Up @@ -50,6 +51,7 @@ fn main() -> io::Result<()> {
let mut edges_complement: Vec<(String, String)> = Vec::new();

let is_undirected: bool = args.is_present("undirected");
let show_all: bool = args.is_present("all");

for v1 in &vertices {
for v2 in &vertices {
Expand Down Expand Up @@ -102,39 +104,44 @@ fn main() -> io::Result<()> {
}

writeln!(writer)?;
writeln!(writer, "\"No larger clique exists (every other clique is at most as big as the clique defined above)\"")?;
writeln!(writer)?;

writeln!(
writer,
"forall {} # (",
vertices
.iter()
.map(|v| format!("v_{}", v))
.collect::<Vec<String>>()
.join(", ")
)?;

writeln!(
writer,
"{}",
edges_complement
.iter()
.map(|(from, to)| format!(" -(v_{} & v_{})", from, to))
.collect::<Vec<String>>()
.join(" &\n")
)?;

writeln!(
writer,
") => [{}] >= [{}]",
vertices.iter().cloned().collect::<Vec<String>>().join(", "),
vertices
.iter()
.map(|v| format!("v_{}", v))
.collect::<Vec<String>>()
.join(", ")
)?;
if show_all {
writeln!(writer, "true")?;
} else {
writeln!(writer, "\"No larger clique exists (every other clique is at most as big as the clique defined above)\"")?;
writeln!(writer)?;

writeln!(
writer,
"forall {} # (",
vertices
.iter()
.map(|v| format!("v_{}", v))
.collect::<Vec<String>>()
.join(", ")
)?;

writeln!(
writer,
"{}",
edges_complement
.iter()
.map(|(from, to)| format!(" -(v_{} & v_{})", from, to))
.collect::<Vec<String>>()
.join(" &\n")
)?;

writeln!(
writer,
") => [{}] >= [{}]",
vertices.iter().cloned().collect::<Vec<String>>().join(", "),
vertices
.iter()
.map(|v| format!("v_{}", v))
.collect::<Vec<String>>()
.join(", ")
)?;
}

// flush the writer before dropping it
writer.flush().expect("Could not flush write buffer");
Expand Down

0 comments on commit b845312

Please sign in to comment.