From a1a779c4049f73a8ffeec577abd24df2b1e1df06 Mon Sep 17 00:00:00 2001 From: Malte Tammena Date: Wed, 13 Mar 2024 12:48:39 +0100 Subject: [PATCH] add iccma gen script and tarjan scc graph algorithm --- scripts/aba_generator.py | 107 +++++++++++++++++++++ src/graph/mod.rs | 198 +++++++++++++++++++++++++++++++++++++++ src/main.rs | 1 + 3 files changed, 306 insertions(+) create mode 100644 scripts/aba_generator.py create mode 100644 src/graph/mod.rs diff --git a/scripts/aba_generator.py b/scripts/aba_generator.py new file mode 100644 index 0000000..09f1f23 --- /dev/null +++ b/scripts/aba_generator.py @@ -0,0 +1,107 @@ +""" +Copyright <2023> + +Permission is hereby granted, free of charge, to any person obtaining a copy of this +software and associated documentation files (the "Software"), to deal in the Software +without restriction, including without limitation the rights to use, copy, modify, +merge, publish, distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to the following +conditions: + +The above copyright notice and this permission notice shall be included in all copies +or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, +INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR +PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT +OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR +OTHER DEALINGS IN THE SOFTWARE. +""" + +import sys, random +import argparse + +def create_framework(n_sentences, n_assumptions, n_rules_per_head, size_of_bodies): + """ + Create a random framework. + + sentences contains the non-assumption sentences. + n_rules_per_head should be a list exhausting the possible number of rules each head can have + size_of_bodies should be a list exhausting the possible number of sentences in any rule body + These should hold in order to get non-counterintuitive results: + - n_assumptions < n_sentences + - max(size_of_bodies) <= n_sentences+n_assumptions + """ + + assumptions = [str(i) for i in range(1,n_assumptions+1)] + sentences = [str(i) for i in range(n_assumptions+1,n_sentences+1)] + + contraries = {asmpt: random.choice(sentences+assumptions) for asmpt in assumptions} + + rules = [] + for head in sentences: + n_rules_in_this_head = random.choice(n_rules_per_head) + for _ in range(n_rules_in_this_head): + size_of_body = random.choice(size_of_bodies) + #pool = set(assumptions+sentences) + pool = assumptions+sentences + pool.remove(head) + #sorted(pool) + body = random.sample(pool, size_of_body) + rules.append((head, body)) + + return assumptions, sentences, contraries, rules + +def print_ICCMA_format(assumptions, contraries, rules, n_sentences, out_filename): + """ + Print the given framework in the ICCMA 2023 format. + """ + offset = len(assumptions) + with open(out_filename, 'w') as out: + out.write(f"p aba {n_sentences}\n") + for i, asm in enumerate(assumptions): + out.write(f"a {asm}\n") + #print(f"a {asm}") + for ctr in contraries: + out.write(f"c {ctr} {contraries.get(ctr)}\n") + #print(f"c {ctr} {contraries.get(ctr)}") + for rule in rules: + out.write(f"r {rule[0]} {' '.join(rule[1])}\n") + #print(f"r {rule[0]} {' '.join(rule[1])}") + +def print_ASP(assumptions, contraries, rules, query, out_filename): + """ + Print the given framework in ASP format. + """ + with open(out_filename, 'w') as out: + for asm in assumptions: + out.write(f"assumption(a{asm}).\n") + for ctr in contraries: + out.write(f"contrary(a{ctr},a{contraries.get(ctr)}).\n") + for i, rule in enumerate(rules): + out.write(f"head({str(i)},a{rule[0]}).\n") + if rule[1]: + for body in rule[1]: + out.write(f"body({str(i)},a{body}).\n") + out.write(f"query(a{query}).\n") + +def ICCMA23_benchmarks(sens, directory="iccma23_aba_benchmarks", identifier="aba"): + random.seed(811543731122527) + n_rules_max = [5,10] + rule_size_max = [5,10] + asmpt_ratio = [0.1,0.3] + for sen in sens: + for k in asmpt_ratio: + for rph_max in n_rules_max: + for spb_max in rule_size_max: + for i in range(10): + n_a = int(round(k*sen)) + n_rph = range(1,rph_max+1) + n_spb = range(1,spb_max+1) + filename = f"{directory}/{identifier}_{sen}_{k}_{rph_max}_{spb_max}_{i}.aba" + print(filename) + framework = create_framework(sen, n_a, n_rph, n_spb) + print_ICCMA_format(framework[0], framework[2], framework[3], sen, filename) + +ICCMA23_benchmarks(sens=[25,100,500,2000,5000]) diff --git a/src/graph/mod.rs b/src/graph/mod.rs new file mode 100644 index 0000000..42c73d8 --- /dev/null +++ b/src/graph/mod.rs @@ -0,0 +1,198 @@ +//! [SOURCE](https://github.com/TheAlgorithms/Rust) +//! +//! MIT License +//! +//! Copyright (c) 2019 The Algorithms +//! +//! Permission is hereby granted, free of charge, to any person obtaining a copy +//! of this software and associated documentation files (the "Software"), to deal +//! in the Software without restriction, including without limitation the rights +//! to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +//! copies of the Software, and to permit persons to whom the Software is +//! furnished to do so, subject to the following conditions: +//! +//! The above copyright notice and this permission notice shall be included in all +//! copies or substantial portions of the Software. +//! +//! THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +//! IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +//! FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +//! AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +//! LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +//! OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +//! SOFTWARE. +#![allow(dead_code)] + +pub struct Graph { + n: usize, + adj_list: Vec>, +} + +impl Graph { + pub fn new(n: usize) -> Self { + Self { + n, + adj_list: vec![vec![]; n], + } + } + + pub fn add_edge(&mut self, u: usize, v: usize) { + self.adj_list[u].push(v); + } +} +pub fn tarjan_scc(graph: &Graph) -> Vec> { + struct TarjanState { + index: i32, + stack: Vec, + on_stack: Vec, + index_of: Vec, + lowlink_of: Vec, + components: Vec>, + } + + let mut state = TarjanState { + index: 0, + stack: Vec::new(), + on_stack: vec![false; graph.n], + index_of: vec![-1; graph.n], + lowlink_of: vec![-1; graph.n], + components: Vec::new(), + }; + + fn strong_connect(v: usize, graph: &Graph, state: &mut TarjanState) { + state.index_of[v] = state.index; + state.lowlink_of[v] = state.index; + state.index += 1; + state.stack.push(v); + state.on_stack[v] = true; + + for &w in &graph.adj_list[v] { + if state.index_of[w] == -1 { + strong_connect(w, graph, state); + state.lowlink_of[v] = state.lowlink_of[v].min(state.lowlink_of[w]); + } else if state.on_stack[w] { + state.lowlink_of[v] = state.lowlink_of[v].min(state.index_of[w]); + } + } + + if state.lowlink_of[v] == state.index_of[v] { + let mut component: Vec = Vec::new(); + while let Some(w) = state.stack.pop() { + state.on_stack[w] = false; + component.push(w); + if w == v { + break; + } + } + state.components.push(component); + } + } + + for v in 0..graph.n { + if state.index_of[v] == -1 { + strong_connect(v, graph, &mut state); + } + } + + state.components +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn test_tarjan_scc() { + // Test 1: A graph with multiple strongly connected components + let n_vertices = 11; + let edges = vec![ + (0, 1), + (0, 3), + (1, 2), + (1, 4), + (2, 0), + (2, 6), + (3, 2), + (4, 5), + (4, 6), + (5, 6), + (5, 7), + (5, 8), + (5, 9), + (6, 4), + (7, 9), + (8, 9), + (9, 8), + ]; + let mut graph = Graph::new(n_vertices); + + for &(u, v) in &edges { + graph.add_edge(u, v); + } + + let components = tarjan_scc(&graph); + assert_eq!( + components, + vec![ + vec![8, 9], + vec![7], + vec![5, 4, 6], + vec![3, 2, 1, 0], + vec![10], + ] + ); + + // Test 2: A graph with no edges + let n_vertices = 5; + let edges: Vec<(usize, usize)> = vec![]; + let mut graph = Graph::new(n_vertices); + + for &(u, v) in &edges { + graph.add_edge(u, v); + } + + let components = tarjan_scc(&graph); + + // Each node is its own SCC + assert_eq!( + components, + vec![vec![0], vec![1], vec![2], vec![3], vec![4]] + ); + + // Test 3: A graph with single strongly connected component + let n_vertices = 5; + let edges = vec![(0, 1), (1, 2), (2, 3), (2, 4), (3, 0), (4, 2)]; + let mut graph = Graph::new(n_vertices); + + for &(u, v) in &edges { + graph.add_edge(u, v); + } + + let components = tarjan_scc(&graph); + assert_eq!(components, vec![vec![4, 3, 2, 1, 0]]); + + // Test 4: A graph with multiple strongly connected component + let n_vertices = 7; + let edges = vec![ + (0, 1), + (1, 2), + (2, 0), + (1, 3), + (1, 4), + (1, 6), + (3, 5), + (4, 5), + ]; + let mut graph = Graph::new(n_vertices); + + for &(u, v) in &edges { + graph.add_edge(u, v); + } + + let components = tarjan_scc(&graph); + assert_eq!( + components, + vec![vec![5], vec![3], vec![4], vec![6], vec![2, 1, 0],] + ); + } +} diff --git a/src/main.rs b/src/main.rs index cd04d6e..e159722 100644 --- a/src/main.rs +++ b/src/main.rs @@ -33,6 +33,7 @@ mod aba; mod args; mod clauses; mod error; +mod graph; mod literal; mod mapper; mod parser;