From e6d621fac0b07e733049556a5a3bf0a0df8a51ca Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Thu, 8 Feb 2024 14:05:02 +0100 Subject: [PATCH] Make the most relevant algorithms cancellable. --- .../_feedback_vertex_set.rs | 115 +++++++++++++++--- .../_independent_cycles.rs | 42 ++++++- .../_strongly_connected_components.rs | 53 ++++++-- .../_weakly_connected_components.rs | 30 ++++- src/fixed_points/mod.rs | 8 ++ src/symbolic_async_graph/reachability.rs | 35 +++++- src/trap_spaces/_impl_trap_spaces.rs | 8 ++ 7 files changed, 251 insertions(+), 40 deletions(-) diff --git a/src/_impl_regulatory_graph/signed_directed_graph/_feedback_vertex_set.rs b/src/_impl_regulatory_graph/signed_directed_graph/_feedback_vertex_set.rs index f7860db..9575bc7 100644 --- a/src/_impl_regulatory_graph/signed_directed_graph/_feedback_vertex_set.rs +++ b/src/_impl_regulatory_graph/signed_directed_graph/_feedback_vertex_set.rs @@ -1,5 +1,5 @@ -use crate::VariableId; use crate::_impl_regulatory_graph::signed_directed_graph::{SdGraph, Sign}; +use crate::{never_stop, should_log, VariableId, LOG_NOTHING}; use std::collections::{HashMap, HashSet}; impl SdGraph { @@ -8,18 +8,25 @@ impl SdGraph { /// /// This is not the complete FVS approximation algorithm, but it is used multiple times, /// so we abstract it into this helper method. - fn _fvs_helper, VariableId) -> Option>>( + fn _fvs_helper( &self, subgraph: &mut HashSet, mut candidates: HashSet, compute_cycle: F, - ) -> HashSet { + log_level: usize, + interrupt: &I, + ) -> Result, E> + where + F: Fn(&HashSet, VariableId) -> Option>, + I: Fn() -> Result<(), E>, + { let mut result = HashSet::new(); // The shortest known cycle in the current `subgraph` for the given `pivot`. let mut shortest_cycle_for_pivot: HashMap> = HashMap::new(); while !candidates.is_empty() { + interrupt()?; // Ensure determinism. let mut iterable = Vec::from_iter(candidates.clone()); iterable.sort(); @@ -29,6 +36,7 @@ impl SdGraph { let cycle = if let Some(known_cycle) = shortest_cycle_for_pivot.get(&vertex) { known_cycle } else if let Some(computed_cycle) = compute_cycle(subgraph, vertex) { + interrupt()?; shortest_cycle_for_pivot .entry(vertex) .or_insert(computed_cycle) @@ -50,7 +58,14 @@ impl SdGraph { if best.1 == usize::MAX { // The remaining graph is acyclic! - return result; + return Ok(result); + } + + if should_log(log_level) { + println!( + "Selected {:?} as candidate with cycle length {}.", + best.0, best.1 + ); } result.insert(best.0); @@ -60,7 +75,7 @@ impl SdGraph { shortest_cycle_for_pivot.retain(|_k, v| !v.contains(&best.0)); } - result + Ok(result) } /// Compute a feedback vertex set of the subgraph induced by the vertices in the @@ -79,19 +94,59 @@ impl SdGraph { &self, restriction: &HashSet, ) -> HashSet { + self._restricted_feedback_vertex_set(restriction, LOG_NOTHING, &never_stop) + .unwrap() + } + + /// A version of [SdGraph::restricted_feedback_vertex_set] with cancellation + /// and logging. + pub fn _restricted_feedback_vertex_set Result<(), E>>( + &self, + restriction: &HashSet, + log_level: usize, + interrupt: &F, + ) -> Result, E> { let candidates = restriction.clone(); // We then prune the candidates twice: First time, most of the uninteresting nodes are // removed, second time then optimizes the result such that it is (usually) at least // subset minimal. The minimality is still not guaranteed though. - let candidates = self._fvs_helper(&mut restriction.clone(), candidates, |g, x| { - self.shortest_cycle(g, x, usize::MAX) - }); + if should_log(log_level) { + println!( + "Starting FVS computation with {} candidates.", + candidates.len() + ); + } + + let candidates = self._fvs_helper( + &mut restriction.clone(), + candidates, + |g, x| self.shortest_cycle(g, x, usize::MAX), + log_level, + interrupt, + )?; + + if should_log(log_level) { + println!( + "Finished initial FVS pruning with {} candidates.", + candidates.len() + ); + } + + let result = self._fvs_helper( + &mut restriction.clone(), + candidates, + |g, x| self.shortest_cycle(g, x, usize::MAX), + log_level, + interrupt, + )?; - self._fvs_helper(&mut restriction.clone(), candidates, |g, x| { - self.shortest_cycle(g, x, usize::MAX) - }) + if should_log(log_level) { + println!("Finished FVS computation: {} nodes.", result.len()); + } + + Ok(result) } /// Compute a feedback vertex set of the desired parity, considered within the subgraph induced @@ -105,15 +160,45 @@ impl SdGraph { restriction: &HashSet, parity: Sign, ) -> HashSet { + self._restricted_parity_feedback_vertex_set(restriction, parity, LOG_NOTHING, &never_stop) + .unwrap() + } + + /// A version of [SdGraph::restricted_parity_feedback_vertex_set] with cancellation + /// and logging. + pub fn _restricted_parity_feedback_vertex_set Result<(), E>>( + &self, + restriction: &HashSet, + parity: Sign, + log_level: usize, + interrupt: &F, + ) -> Result, E> { // We will be searching in a subset of a known FVS. This is because FVS detection is // a bit faster and usually gives us a reasonable starting point. - let candidates = self.restricted_feedback_vertex_set(restriction); + let candidates = self._restricted_feedback_vertex_set(restriction, log_level, interrupt)?; + + if should_log(log_level) { + println!( + "Starting parity FVS computation with {} candidates.", + candidates.len() + ); + } // The same as normal FVS method, but uses different cycle detection. Here, we don't // repeat it again, because in most cases it is not needed. - self._fvs_helper(&mut restriction.clone(), candidates, |g, x| { - self.shortest_parity_cycle(g, x, parity, usize::MAX) - }) + let result = self._fvs_helper( + &mut restriction.clone(), + candidates, + |g, x| self.shortest_parity_cycle(g, x, parity, usize::MAX), + log_level, + interrupt, + )?; + + if should_log(log_level) { + println!("Finished parity FVS computation: {} nodes.", result.len()); + } + + Ok(result) } /// **(internal)** Compute the degree of a vertex within the given set. diff --git a/src/_impl_regulatory_graph/signed_directed_graph/_independent_cycles.rs b/src/_impl_regulatory_graph/signed_directed_graph/_independent_cycles.rs index a971aa5..04b6019 100644 --- a/src/_impl_regulatory_graph/signed_directed_graph/_independent_cycles.rs +++ b/src/_impl_regulatory_graph/signed_directed_graph/_independent_cycles.rs @@ -1,5 +1,5 @@ -use crate::VariableId; use crate::_impl_regulatory_graph::signed_directed_graph::{SdGraph, Sign}; +use crate::{never_stop, should_log, VariableId, LOG_NOTHING}; use std::collections::HashSet; impl SdGraph { @@ -16,10 +16,24 @@ impl SdGraph { &self, restriction: &HashSet, ) -> Vec> { + self._restricted_independent_cycles(restriction, LOG_NOTHING, &never_stop) + .unwrap() + } + + /// A version of [SdGraph::restricted_independent_cycles] with cancellation + /// and logging. + pub fn _restricted_independent_cycles Result<(), E>>( + &self, + restriction: &HashSet, + log_level: usize, + interrupt: &F, + ) -> Result>, E> { let mut cycles = Vec::new(); let mut components = self.restricted_strongly_connected_components(restriction); while let Some(mut scc) = components.pop() { + interrupt()?; + let mut best_cycle = None; let mut best_cycle_len = usize::MAX; // Not particularly efficient, but keeps this whole thing deterministic. @@ -27,6 +41,7 @@ impl SdGraph { scc_iter.sort(); for x in &scc_iter { if let Some(cycle) = self.shortest_cycle(&scc, *x, best_cycle_len) { + interrupt()?; if cycle.len() == 1 { // Cycle of length one will always win, no need to check further. best_cycle = Some(cycle); @@ -42,6 +57,9 @@ impl SdGraph { } if let Some(best_cycle) = best_cycle { + if should_log(log_level) { + println!("Selected {:?} as the shortest candidate.", best_cycle); + } for x in &best_cycle { scc.remove(x); } @@ -51,7 +69,7 @@ impl SdGraph { } cycles.sort_by_key(|it| it.len()); - cycles + Ok(cycles) } /// Compute a collection of independent cycles of the given `parity` within the desired @@ -68,10 +86,24 @@ impl SdGraph { restriction: &HashSet, parity: Sign, ) -> Vec> { + self._restricted_independent_parity_cycles(restriction, parity, LOG_NOTHING, &never_stop) + .unwrap() + } + + /// A version of [SdGraph::restricted_independent_parity_cycles] with cancellation + /// and logging. + pub fn _restricted_independent_parity_cycles Result<(), E>>( + &self, + restriction: &HashSet, + parity: Sign, + log_level: usize, + interrupt: &F, + ) -> Result>, E> { let mut cycles = Vec::new(); let mut components = self.restricted_strongly_connected_components(restriction); while let Some(mut scc) = components.pop() { + interrupt()?; let mut best_cycle = None; let mut best_cycle_len = usize::MAX; // Not particularly efficient, but keeps this whole thing deterministic. @@ -79,6 +111,7 @@ impl SdGraph { scc_iter.sort(); for x in &scc_iter { if let Some(cycle) = self.shortest_parity_cycle(&scc, *x, parity, best_cycle_len) { + interrupt()?; if cycle.len() == 1 { // Cycle of length one will always win, no need to check further. best_cycle = Some(cycle); @@ -91,6 +124,9 @@ impl SdGraph { } if let Some(best_cycle) = best_cycle { + if should_log(log_level) { + println!("Selected {:?} as the shortest candidate.", best_cycle); + } for x in &best_cycle { scc.remove(x); } @@ -100,7 +136,7 @@ impl SdGraph { } cycles.sort_by_key(|it| it.len()); - cycles + Ok(cycles) } } diff --git a/src/_impl_regulatory_graph/signed_directed_graph/_strongly_connected_components.rs b/src/_impl_regulatory_graph/signed_directed_graph/_strongly_connected_components.rs index bfd8c8e..a657881 100644 --- a/src/_impl_regulatory_graph/signed_directed_graph/_strongly_connected_components.rs +++ b/src/_impl_regulatory_graph/signed_directed_graph/_strongly_connected_components.rs @@ -1,5 +1,5 @@ -use crate::VariableId; use crate::_impl_regulatory_graph::signed_directed_graph::{SdGraph, Sign}; +use crate::{never_stop, should_log, VariableId, LOG_NOTHING}; use std::collections::HashSet; impl SdGraph { @@ -7,10 +7,7 @@ impl SdGraph { /// /// The result is sorted by component size. pub fn strongly_connected_components(&self) -> Vec> { - let mut results = Vec::new(); - scc_recursive(self, self.mk_all_vertices(), &mut results); - results.sort_by_key(|it| it.len()); - results + self.restricted_strongly_connected_components(&self.mk_all_vertices()) } /// Find all non-trivial strongly connected components in the given `restriction` of this `SdGraph`. @@ -20,10 +17,28 @@ impl SdGraph { &self, restriction: &HashSet, ) -> Vec> { + self._restricted_strongly_connected_components(restriction, LOG_NOTHING, &never_stop) + .unwrap() + } + + /// A version of [SdGraph::restricted_strongly_connected_components] with cancellation + /// and logging. + pub fn _restricted_strongly_connected_components Result<(), E>>( + &self, + restriction: &HashSet, + log_level: usize, + interrupt: &F, + ) -> Result>, E> { let mut results = Vec::new(); - scc_recursive(self, restriction.clone(), &mut results); + scc_recursive( + self, + restriction.clone(), + &mut results, + log_level, + interrupt, + )?; results.sort_by_key(|it| it.len()); - results + Ok(results) } } @@ -32,27 +47,37 @@ impl SdGraph { /// The complexity of the procedure is $n^2$. It can be (in theory) improved to $n \cdot log(n)$, /// but at the moment I don't really see a benefit to it as it is still sufficiently fast for /// most reasonable cases. -fn scc_recursive( +fn scc_recursive Result<(), E>>( graph: &SdGraph, mut universe: HashSet, results: &mut Vec>, -) { + log_level: usize, + interrupt: &F, +) -> Result<(), E> { trim_trivial(&graph.successors, &mut universe); + interrupt()?; trim_trivial(&graph.predecessors, &mut universe); + interrupt()?; if universe.is_empty() { - return; + return Ok(()); } let pivot = universe.iter().next().cloned().unwrap(); let fwd = graph.restricted_forward_reachable(&universe, HashSet::from([pivot])); + interrupt()?; + let bwd = graph.restricted_backward_reachable(&universe, HashSet::from([pivot])); + interrupt()?; let fwd_or_bwd: HashSet = fwd.union(&bwd).cloned().collect(); let fwd_and_bwd: HashSet = fwd.intersection(&bwd).cloned().collect(); if is_non_trivial(graph, &fwd_and_bwd) { + if should_log(log_level) { + println!("Found SCC with {} nodes.", fwd_or_bwd.len()); + } results.push(fwd_and_bwd); } @@ -61,16 +86,18 @@ fn scc_recursive( let bwd_rest: HashSet = bwd.difference(&fwd).cloned().collect(); if !universe_rest.is_empty() { - scc_recursive(graph, universe_rest, results); + scc_recursive(graph, universe_rest, results, log_level, interrupt)?; } if !fwd_rest.is_empty() { - scc_recursive(graph, fwd_rest, results); + scc_recursive(graph, fwd_rest, results, log_level, interrupt)?; } if !bwd_rest.is_empty() { - scc_recursive(graph, bwd_rest, results); + scc_recursive(graph, bwd_rest, results, log_level, interrupt)?; } + + Ok(()) } /// **(internal)** Check if an SCC is trivial. diff --git a/src/_impl_regulatory_graph/signed_directed_graph/_weakly_connected_components.rs b/src/_impl_regulatory_graph/signed_directed_graph/_weakly_connected_components.rs index 66f546b..5bf93a1 100644 --- a/src/_impl_regulatory_graph/signed_directed_graph/_weakly_connected_components.rs +++ b/src/_impl_regulatory_graph/signed_directed_graph/_weakly_connected_components.rs @@ -1,4 +1,4 @@ -use crate::{SdGraph, VariableId}; +use crate::{never_stop, should_log, SdGraph, VariableId, LOG_NOTHING}; use std::collections::HashSet; impl SdGraph { @@ -12,8 +12,20 @@ impl SdGraph { &self, restriction: &HashSet, ) -> Vec> { + self._restricted_weakly_connected_components(restriction, LOG_NOTHING, &never_stop) + .unwrap() + } + + /// A version of [SdGraph::restricted_weakly_connected_components] with cancellation + /// and logging. + pub fn _restricted_weakly_connected_components Result<(), E>>( + &self, + restriction: &HashSet, + log_level: usize, + interrupt: &F, + ) -> Result>, E> { if restriction.is_empty() { - return Vec::new(); + return Ok(Vec::new()); } let pivot = *restriction.iter().min().unwrap(); @@ -21,7 +33,9 @@ impl SdGraph { let mut component = HashSet::from([pivot]); loop { let fwd = self.restricted_forward_reachable(restriction, component.clone()); + interrupt()?; let bwd = self.restricted_backward_reachable(restriction, component.clone()); + interrupt()?; if fwd.is_subset(&component) && bwd.is_subset(&component) { break; } @@ -33,10 +47,18 @@ impl SdGraph { let new_restriction: HashSet = restriction.difference(&component).cloned().collect(); + if should_log(log_level) { + println!("Found weak component with {} vertices.", component.len()); + } + result.push(component); - result.append(&mut self.restricted_weakly_connected_components(&new_restriction)); + result.append(&mut self._restricted_weakly_connected_components( + &new_restriction, + log_level, + interrupt, + )?); - result + Ok(result) } } diff --git a/src/fixed_points/mod.rs b/src/fixed_points/mod.rs index 2001bb3..1df1d40 100644 --- a/src/fixed_points/mod.rs +++ b/src/fixed_points/mod.rs @@ -150,6 +150,8 @@ impl FixedPoints { Self::_symbolic(stg, restriction, global_log_level(), &never_stop).unwrap() } + /// A version of [FixedPoints::symbolic] with cancellation + /// and logging. pub fn _symbolic Result<(), E>>( stg: &SymbolicAsyncGraph, restriction: &GraphColoredVertices, @@ -302,6 +304,8 @@ impl FixedPoints { Self::_symbolic_merge(universe, to_merge, project, global_log_level(), &never_stop).unwrap() } + /// A version of [FixedPoints::symbolic_merge] with cancellation + /// and logging. pub fn _symbolic_merge Result<(), E>>( universe: &BddVariableSet, to_merge: Vec, @@ -448,6 +452,8 @@ impl FixedPoints { Self::_symbolic_vertices(stg, restriction, global_log_level(), &never_stop).unwrap() } + /// A version of [FixedPoints::symbolic_vertices] with cancellation + /// and logging. pub fn _symbolic_vertices Result<(), E>>( stg: &SymbolicAsyncGraph, restriction: &GraphColoredVertices, @@ -505,6 +511,8 @@ impl FixedPoints { Self::_symbolic_colors(stg, restriction, global_log_level(), &never_stop).unwrap() } + /// A version of [FixedPoints::symbolic_colors] with cancellation + /// and logging. pub fn _symbolic_colors Result<(), E>>( stg: &SymbolicAsyncGraph, restriction: &GraphColoredVertices, diff --git a/src/symbolic_async_graph/reachability.rs b/src/symbolic_async_graph/reachability.rs index 0be6a90..a957a95 100644 --- a/src/symbolic_async_graph/reachability.rs +++ b/src/symbolic_async_graph/reachability.rs @@ -1,6 +1,6 @@ use crate::biodivine_std::traits::Set; use crate::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph}; -use crate::VariableId; +use crate::{log_essential, never_stop, should_log, VariableId, LOG_ESSENTIAL, LOG_NOTHING}; use std::cmp::max; use std::collections::{HashMap, HashSet}; @@ -108,7 +108,28 @@ impl Reachability { initial: &GraphColoredVertices, step: F, ) -> GraphColoredVertices { - if cfg!(feature = "print-progress") { + let log_level = if cfg!(feature = "print-progress") { + LOG_ESSENTIAL + } else { + LOG_NOTHING + }; + Reachability::_reach(graph, initial, step, log_level, &never_stop).unwrap() + } + + /// A version of [Reachability::reach] with cancellation + /// and logging. + pub fn _reach( + graph: &SymbolicAsyncGraph, + initial: &GraphColoredVertices, + step: F, + log_level: usize, + interrupt: &I, + ) -> Result + where + F: Fn(&SymbolicAsyncGraph, &GraphColoredVertices, VariableId) -> GraphColoredVertices, + I: Fn() -> Result<(), E>, + { + if should_log(log_level) { println!( "Start symbolic reachability with {}[nodes:{}] candidates.", initial.approx_cardinality(), @@ -133,6 +154,8 @@ impl Reachability { }) .collect::>(); + interrupt()?; + let mut result = initial.clone(); let mut max_size = 0; @@ -141,13 +164,15 @@ impl Reachability { 'reach: loop { for var in graph.variables().rev() { let next_step = step(graph, &result, var); + interrupt()?; + if next_step.is_empty() { saturated.insert(var); } else { result = result.union(&next_step); max_size = max(max_size, result.symbolic_size()); - if cfg!(feature = "print-progress") { + if log_essential(log_level, result.symbolic_size()) { let current = result.approx_cardinality(); let max = graph.unit_colored_vertices().approx_cardinality(); println!( @@ -169,7 +194,7 @@ impl Reachability { } } - if cfg!(feature = "print-progress") { + if should_log(log_level) { println!( "Structural reachability done: {}[nodes:{}] candidates. Max intermediate size: {}.", result.approx_cardinality(), @@ -178,7 +203,7 @@ impl Reachability { ); } - return result; + return Ok(result); } } } diff --git a/src/trap_spaces/_impl_trap_spaces.rs b/src/trap_spaces/_impl_trap_spaces.rs index c969556..c5e86bb 100644 --- a/src/trap_spaces/_impl_trap_spaces.rs +++ b/src/trap_spaces/_impl_trap_spaces.rs @@ -18,6 +18,8 @@ impl TrapSpaces { .unwrap() } + /// A version of [TrapSpaces::essential_symbolic] with cancellation + /// and logging. pub fn _essential_symbolic Result<(), E>>( network: &BooleanNetwork, ctx: &SymbolicSpaceContext, @@ -120,6 +122,8 @@ impl TrapSpaces { Self::_minimal_symbolic(network, ctx, restriction, global_log_level(), &never_stop).unwrap() } + /// A version of [TrapSpaces::minimal_symbolic] with cancellation + /// and logging. pub fn _minimal_symbolic Result<(), E>>( network: &BooleanNetwork, ctx: &SymbolicSpaceContext, @@ -139,6 +143,8 @@ impl TrapSpaces { Self::_minimize(ctx, spaces, global_log_level(), &never_stop).unwrap() } + /// A version of [TrapSpaces::minimize] with cancellation + /// and logging. pub fn _minimize Result<(), E>>( ctx: &SymbolicSpaceContext, spaces: &NetworkColoredSpaces, @@ -225,6 +231,8 @@ impl TrapSpaces { Self::_maximize(ctx, spaces, global_log_level(), &never_stop).unwrap() } + /// A version of [TrapSpaces::maximize] with cancellation + /// and logging. pub fn _maximize Result<(), E>>( ctx: &SymbolicSpaceContext, spaces: &NetworkColoredSpaces,