megamanmalte/aba2sat
0
0
Fork 0
Code Issues Pull requests Packages Projects Releases Wiki Activity

add iccma gen script and tarjan scc graph algorithm

Browse source
This commit is contained in:
Malte Tammena 2024-03-13 12:48:39 +01:00
parent b4b996b298
commit a1a779c404
3 changed files with 306 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

107
scripts/aba_generator.py Normal file
View file

@ -0,0 +1,107 @@
"""
Copyright <2023> <Tuomo Lehtonen, University of Helsinki>
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])

198
src/graph/mod.rs Normal file
View file

@ -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<Vec<usize>>,
}
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<Vec<usize>> {
struct TarjanState {
index: i32,
stack: Vec<usize>,
on_stack: Vec<bool>,
index_of: Vec<i32>,
lowlink_of: Vec<i32>,
components: Vec<Vec<usize>>,
}
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<usize> = 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],]
);
}
}

1
src/main.rs
View file

@ -33,6 +33,7 @@ mod aba;
mod args;
mod clauses;
mod error;
mod graph;
mod literal;
mod mapper;
mod parser;