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

some bugs, some fixes, but no perfection yet

Browse source 
Loops forever ∞
This commit is contained in:
Malte Tammena 2024-03-15 23:37:23 +01:00
parent 1ab554fc8e
commit 8ab001405a
14 changed files with 447 additions and 264 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
Cargo.lock generated
View file

@ -8,6 +8,7 @@ version = "0.1.0"
dependencies = [
"cadical",
"clap",
"iter_tools",
"nom",
"thiserror",
]
@ -132,6 +133,12 @@ version = "1.0.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "acbf1af155f9b9ef647e42cdc158db4b64a1b61f743629225fde6f3e0be2a7c7"
[[package]]
name = "either"
version = "1.10.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "11157ac094ffbdde99aa67b23417ebdd801842852b500e395a45a9c0aac03e4a"
[[package]]
name = "errno"
version = "0.3.8"
@ -148,6 +155,24 @@ version = "0.4.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8"
[[package]]
name = "iter_tools"
version = "0.10.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "07a28265f753d634d09e32e5e38eb092fe003155ef6e32a0260906170a80eb48"
dependencies = [
"itertools",
]
[[package]]
name = "itertools"
version = "0.11.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b1c173a5686ce8bfa551b3563d0c2170bf24ca44da99c7ca4bfdab5418c3fe57"
dependencies = [
"either",
]
[[package]]
name = "jobserver"
version = "0.1.28"

1
Cargo.toml
View file

@ -10,5 +10,6 @@ license = "GPL3"
[dependencies]
cadical = "0.1.14"
clap = { version = "4.4.8", features = ["wrap_help", "derive"] }
iter_tools = "0.10.0"
nom = "7.1.3"
thiserror = "1.0.50"

8
scripts/validate.sh
View file

@ -34,12 +34,12 @@ run_dc_co() {
if [ "$our_result" != "$other_result" ]; then
printf "❌\n"
printf "%40s:%s\n" "arg" "$ADDITIONAL_ARG"
printf "%40s:%40s %s\n" "Ours" "$our_result" "$(jq /tmp/aba2sat-time --compact-output --color-output)"
printf "%40s:%40s %s\n" "Theirs" "$other_result" "$(jq /tmp/aspforaba-time --compact-output --color-output)"
printf "%40s:%40s %s\n" "Ours" "$our_result" "$(jq --compact-output --color-output </tmp/aba2sat-time)"
printf "%40s:%40s %s\n" "Theirs" "$other_result" "$(jq --compact-output --color-output </tmp/aspforaba-time)"
else
printf "✅\n"
printf "%40s:%40s %s\n" "Ours" "$our_result" "$(jq /tmp/aba2sat-time --compact-output --color-output)"
printf "%40s:%40s %s\n" "Theirs" "$other_result" "$(jq /tmp/aspforaba-time --compact-output --color-output)"
printf "%40s:%40s %s\n" "Ours" "$our_result" "$(jq --compact-output --color-output </tmp/aba2sat-time)"
printf "%40s:%40s %s\n" "Theirs" "$other_result" "$(jq --compact-output --color-output </tmp/aspforaba-time)"
fi
}

13
src/aba/debug.rs
View file

@ -4,7 +4,7 @@ use std::collections::{BTreeMap, HashMap, HashSet};
use super::{Aba, Num};
#[derive(Debug, Default, Clone)]
#[derive(Debug, Clone)]
pub struct DebugAba {
aba: Aba,
forward_map: HashMap<char, Num>,
@ -80,3 +80,14 @@ impl DebugAba {
}
}
}
impl Default for DebugAba {
fn default() -> Self {
Self {
aba: Default::default(),
forward_map: Default::default(),
backward_map: Default::default(),
next: 1,
}
}
}

161
src/aba/mod.rs
View file

@ -30,13 +30,14 @@ use std::{
marker::PhantomData,
};
use crate::{
clauses::{Atom, Clause, ClauseList},
literal::{IntoLiteral, Literal, TheoryAtom},
};
use crate::literal::TheoryAtom;
use self::prepared::PreparedAba;
pub mod debug;
mod prepared;
pub mod problems;
mod theory;
#[derive(Debug)]
pub struct Theory(Num);
@ -47,13 +48,13 @@ impl From<Num> for Theory {
}
}
pub type Rule<A> = (A, HashSet<A>);
pub type RuleList<A> = Vec<Rule<A>>;
pub type Rule = (Num, HashSet<Num>);
pub type RuleList = Vec<Rule>;
pub type Num = u32;
#[derive(Debug, Default, Clone, PartialEq)]
#[derive(Debug, Default, Clone, PartialEq, Eq)]
pub struct Aba {
rules: RuleList<Num>,
rules: RuleList,
inverses: HashMap<Num, Num>,
}
@ -89,11 +90,8 @@ impl Aba {
self.inverses.contains_key(a)
}
/// Translate the ABA into base rules / definitions for SAT solving
pub fn derive_clauses(&self) -> ClauseList {
let mut clauses = ClauseList::new();
self.derive_rule_clauses().collect_into(&mut clauses);
clauses
pub fn contains_atom(&self, elem: &Num) -> bool {
self.universe().any(|e| *e == *elem)
}
pub fn size(&self) -> usize {
@ -109,39 +107,9 @@ impl Aba {
.len()
}
/// Filtered list of rules
///
/// Iterates over all rules, marking reachable elements until
/// no additional rule can be applied. Then removes every
/// rule that contains any unreachable atom and returns the rest
pub fn trim(&mut self) {
// Begin with all assumptions marked as reachable
let mut reachable: HashSet<_> = self.assumptions().cloned().collect();
// Calculate all reachable elements
loop {
let mut marked_any = false;
for (head, body) in &self.rules {
if reachable.contains(head) {
continue;
}
if body.iter().all(|atom| reachable.contains(atom)) {
marked_any = true;
reachable.insert(*head);
}
}
if !marked_any {
break;
}
}
// Remove all rules that contain any unreachable atom
self.rules.retain(|(head, body)| {
// Both the head and all elements from the body must be reachable
reachable.contains(head) && body.iter().all(|atom| reachable.contains(atom))
});
}
fn derive_rule_clauses(&self) -> impl Iterator<Item = Clause> + '_ {
theory_helper::<Theory>(self)
/// Prepare this aba for translation to SAT
pub fn prepare(self) -> PreparedAba {
PreparedAba::from(self)
}
fn rule_heads(&self) -> impl Iterator<Item = &Num> + '_ {
@ -149,108 +117,15 @@ impl Aba {
}
}
fn body_to_clauses<I: TheoryAtom>(head: Literal, body: &HashSet<Num>) -> ClauseList {
let mut clauses = vec![];
let mut left_implication: Clause = body.iter().map(|elem| I::new(*elem).neg()).collect();
left_implication.push(head.clone().positive());
clauses.push(left_implication);
body.iter()
.map(|elem| vec![head.clone().negative(), I::new(*elem).pos()].into())
.collect_into(&mut clauses);
clauses
}
/// Generate the logic for theory derivation in the given [`Aba`]
///
/// This will need a valid [`TheoryAtom`] that will be used to construct the logic
///
/// # Explanation
///
/// We will mainly operate on heads of rules here. So consider head `p` and all bodies `b`
/// in the set of all bodies of `p`: `bodies(p)`.
/// Every body `b` in `bodies(p)` is a set of atoms. Any set of atoms (any body) can be
/// used to derive `p`. So the following relation must hold:
/// - if `p` is true, at least one body `b` must be true aswell.
/// this only holds, because `p` itself is not assumption (since we're
/// only talking flat ABA)
/// - if `b` in `bodies(p)` is true, `p` must be true aswell
///
/// The entire logic in this function is required to implement this equality in DNF.
///
/// # Extra steps
///
/// - We do some extra work here to prevent atoms that never occur in the head of rule and
/// are not an assumption from ever being true.
/// - heads with a single body are common enough in practice to benefit from special care.
/// A lot of the overhead is due to the fact that multiple bodies are an option, if that's
/// not given for a head `p` we use the simplified translation logic where `p` is true iff
/// `bodies(p)` is true.
pub fn theory_helper<I: TheoryAtom>(aba: &Aba) -> impl Iterator<Item = Clause> + '_ {
// The combined list of rules, such that every
// head is unique and possible contains a list of bodies
let mut rules_combined =
aba.rules
.iter()
.fold(HashMap::<_, Vec<_>>::new(), |mut rules, (head, body)| {
rules.entry(head).or_default().push(body);
rules
});
// All atoms that can be derived by rules
let rule_heads: HashSet<_> = aba.rule_heads().collect();
// For every non-assumption, that is not derivable add a rule without a body,
// such that it cannot be derived at all. This is to prevent the solver from
// guessing this atom on it's own
aba.universe()
.filter(|atom| !aba.contains_assumption(atom))
.filter(|atom| !rule_heads.contains(atom))
.map(|atom| (atom, vec![]))
.collect_into(&mut rules_combined);
// All combined rules
// These are heads with any number of bodies, possibly none
rules_combined
.into_iter()
.flat_map(|(head, bodies)| match &bodies[..] {
// No bodies, add a clause that prevents the head from accuring in the theory
[] => {
vec![Clause::from(vec![I::new(*head).neg()])]
}
// A single body only, this is equivalent to a head that can only be derived by a single rule
[body] => body_to_clauses::<I>(I::new(*head).pos(), body),
// n bodies, we'll need to take extra care to allow any number of bodies to derive this
// head without logic errors
bodies => {
let mut clauses = vec![];
bodies
.iter()
.enumerate()
.flat_map(|(idx, body)| {
body_to_clauses::<I>(TheoryHelper::<I, _>::new(idx, *head).pos(), body)
})
.collect_into(&mut clauses);
let helpers: Vec<_> = (0..bodies.len())
.map(|idx| TheoryHelper::<I, _>::new(idx, *head).pos())
.collect();
let mut right_implification: Clause = helpers.iter().cloned().collect();
right_implification.push(I::new(*head).neg());
clauses.push(right_implification);
helpers
.into_iter()
.map(|helper| Clause::from(vec![I::new(*head).pos(), helper.negative()]))
.collect_into(&mut clauses);
clauses
}
})
}
#[derive(Debug)]
struct TheoryHelper<T: TheoryAtom, A: Atom> {
struct TheoryHelper<T: TheoryAtom> {
_idx: usize,
_atom: A,
_atom: Num,
inner: PhantomData<T>,
}
impl<T: TheoryAtom, A: Atom> TheoryHelper<T, A> {
fn new(idx: usize, atom: A) -> Self {
impl<T: TheoryAtom> TheoryHelper<T> {
fn new(idx: usize, atom: Num) -> Self {
Self {
_idx: idx,
_atom: atom,

135
src/aba/prepared.rs Normal file
View file

@ -0,0 +1,135 @@
use std::collections::HashSet;
use iter_tools::Itertools;
use crate::{aba::Num, clauses::Clause, graph::Graph, literal::TheoryAtom};
use super::{theory::theory_helper, Aba, RuleList};
#[derive(Debug, Clone, PartialEq, Eq)]
struct r#Loop {
heads: HashSet<Num>,
support: RuleList,
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct PreparedAba {
aba: Aba,
loops: Vec<r#Loop>,
}
impl PreparedAba {
/// Translate the ABA into base rules / definitions for SAT solving
pub fn derive_clauses<I: TheoryAtom>(&self) -> impl Iterator<Item = Clause> + '_ {
theory_helper::<I>(self).chain(self.derive_loop_breaker::<I>())
}
fn derive_loop_breaker<I: TheoryAtom>(&self) -> impl Iterator<Item = Clause> + '_ {
self.loops.iter().flat_map(|r#loop| {
let mut head_list: Vec<_> = r#loop.heads.iter().collect();
head_list.push(head_list[0]);
let loop_enforcement_clauses =
head_list
.into_iter()
.tuple_windows()
.flat_map(|(first, second)| {
[
Clause::from(vec![I::new(*first).pos(), I::new(*second).pos()]),
Clause::from(vec![I::new(*first).neg(), I::new(*second).neg()]),
]
});
let head_sample = *r#loop.heads.iter().next().unwrap();
let body_rules = r#loop.support.iter().map(|(_head, body)| body);
let clauses = body_rules.multi_cartesian_product().map(move |product| {
product
.into_iter()
.map(|elem| I::new(*elem).pos())
.chain(std::iter::once(I::new(head_sample).neg()))
.collect()
});
loop_enforcement_clauses.chain(clauses)
})
}
}
/// Filtered list of rules
///
/// Iterates over all rules, marking reachable elements until
/// no additional rule can be applied. Then removes every
/// rule that contains any unreachable atom and returns the rest
fn trim_unreachable_rules(aba: &mut Aba) {
// Begin with all assumptions marked as reachable
let mut reachable: HashSet<_> = aba.assumptions().cloned().collect();
// Calculate all reachable elements
loop {
let mut marked_any = false;
for (head, body) in &aba.rules {
if reachable.contains(head) {
continue;
}
if body.iter().all(|atom| reachable.contains(atom)) {
marked_any = true;
reachable.insert(*head);
}
}
if !marked_any {
break;
}
}
// Remove all rules that contain any unreachable atom
aba.rules.retain(|(head, body)| {
// Both the head and all elements from the body must be reachable
reachable.contains(head) && body.iter().all(|atom| reachable.contains(atom))
});
}
fn calculate_loops_and_their_support(aba: &Aba) -> Vec<r#Loop> {
// Construct the graph containing all elements of the universe
// with edges based on the aba's rules
let graph = aba.rules.iter().fold(Graph::new(), |graph, (head, body)| {
body.iter().fold(graph, |mut graph, elem| {
graph.add_edge(*elem, *head);
graph
})
});
// Use a linear time algorithm to calculate the strongly connected
// components of the derived graph
let scc = graph.tarjan_scc();
// Loops are strongly connected components that have more than one element
// These are just the largest loops. There may be smaller loops inside loops
// but it should suffice to prevent these loops
let loops = scc.into_iter().filter(|component| component.len() > 1);
// Iterate over all loops and apply the fixing-logic
loops
.map(|heads| {
let heads: HashSet<_> = heads.into_iter().map(|head| head as Num).collect();
let loop_rules = aba
.rules
.iter()
.filter(|(head, _body)| heads.contains(head));
// Relevant rules are those that contain only elements from outside the loop
// All other rules cannot influence the value of the loop
let support = loop_rules
.filter(|(_head, body)| body.is_disjoint(&heads))
.cloned()
.collect();
r#Loop { heads, support }
})
.collect()
}
impl From<Aba> for PreparedAba {
fn from(mut aba: Aba) -> Self {
trim_unreachable_rules(&mut aba);
let loops = calculate_loops_and_their_support(&aba);
PreparedAba { aba, loops }
}
}
impl std::ops::Deref for PreparedAba {
type Target = Aba;
fn deref(&self) -> &Self::Target {
&self.aba
}
}

16
src/aba/problems/admissibility.rs
View file

@ -2,7 +2,7 @@
use std::collections::HashSet;
use crate::{
aba::{theory_helper, Aba, Num, Theory},
aba::{prepared::PreparedAba, Aba, Num, Theory},
clauses::{Clause, ClauseList},
error::Error,
literal::{IntoLiteral, TheoryAtom},
@ -33,11 +33,11 @@ pub struct DecideCredulousAdmissibility {
}
pub fn initial_admissibility_clauses<I: std::fmt::Debug + 'static + TheoryAtom>(
aba: &Aba,
aba: &PreparedAba,
) -> ClauseList {
let mut clauses = vec![];
// Create inference for the problem set
theory_helper::<I>(aba).collect_into(&mut clauses);
aba.derive_clauses::<I>().collect_into(&mut clauses);
// Attack the inference of the aba, if an attack exists
for (assumption, inverse) in &aba.inverses {
[
@ -90,7 +90,7 @@ fn construct_found_set(state: SolverState<'_>) -> HashSet<Num> {
impl Problem for SampleAdmissibleExtension {
type Output = HashSet<Num>;
fn additional_clauses(&self, aba: &Aba) -> ClauseList {
fn additional_clauses(&self, aba: &PreparedAba) -> ClauseList {
let mut clauses = initial_admissibility_clauses::<SetTheory>(aba);
// Prevent the empty set
let no_empty_set: Clause = aba
@ -111,10 +111,10 @@ impl Problem for SampleAdmissibleExtension {
}
}
impl MultishotProblem<Num> for EnumerateAdmissibleExtensions {
impl MultishotProblem for EnumerateAdmissibleExtensions {
type Output = Vec<HashSet<Num>>;
fn additional_clauses(&self, aba: &Aba, iteration: usize) -> ClauseList {
fn additional_clauses(&self, aba: &PreparedAba, iteration: usize) -> ClauseList {
match iteration {
0 => {
let mut clauses = initial_admissibility_clauses::<SetTheory>(aba);
@ -186,7 +186,7 @@ impl MultishotProblem<Num> for EnumerateAdmissibleExtensions {
impl Problem for VerifyAdmissibleExtension {
type Output = bool;
fn additional_clauses(&self, aba: &Aba) -> crate::clauses::ClauseList {
fn additional_clauses(&self, aba: &PreparedAba) -> crate::clauses::ClauseList {
let mut clauses = initial_admissibility_clauses::<SetTheory>(aba);
// Force inference on all members of the set
for assumption in aba.assumptions() {
@ -222,7 +222,7 @@ impl Problem for VerifyAdmissibleExtension {
impl Problem for DecideCredulousAdmissibility {
type Output = bool;
fn additional_clauses(&self, aba: &Aba) -> ClauseList {
fn additional_clauses(&self, aba: &PreparedAba) -> ClauseList {
let mut clauses = initial_admissibility_clauses::<SetTheory>(aba);
clauses.push(Clause::from(vec![SetTheory(self.element).pos()]));
clauses

12
src/aba/problems/complete.rs
View file

@ -1,7 +1,7 @@
use std::collections::HashSet;
use crate::{
aba::{Aba, Num, Theory},
aba::{prepared::PreparedAba, Aba, Num, Theory},
clauses::{Clause, ClauseList},
error::Error,
literal::{IntoLiteral, TheoryAtom},
@ -23,7 +23,7 @@ pub struct DecideCredulousComplete {
pub element: Num,
}
fn initial_complete_clauses(aba: &Aba) -> ClauseList {
fn initial_complete_clauses(aba: &PreparedAba) -> ClauseList {
// Take everything from admissibility
let mut clauses = initial_admissibility_clauses::<SetTheory>(aba);
// Additional complete logic
@ -38,10 +38,10 @@ fn initial_complete_clauses(aba: &Aba) -> ClauseList {
clauses
}
impl MultishotProblem<Num> for EnumerateCompleteExtensions {
impl MultishotProblem for EnumerateCompleteExtensions {
type Output = Vec<HashSet<Num>>;
fn additional_clauses(&self, aba: &Aba, iteration: usize) -> ClauseList {
fn additional_clauses(&self, aba: &PreparedAba, iteration: usize) -> ClauseList {
match iteration {
0 => initial_complete_clauses(aba),
idx => {
@ -94,7 +94,7 @@ impl MultishotProblem<Num> for EnumerateCompleteExtensions {
impl Problem for DecideCredulousComplete {
type Output = bool;
fn additional_clauses(&self, aba: &Aba) -> ClauseList {
fn additional_clauses(&self, aba: &PreparedAba) -> ClauseList {
let mut clauses = initial_complete_clauses(aba);
clauses.push(Clause::from(vec![SetTheory(self.element).pos()]));
clauses
@ -105,7 +105,7 @@ impl Problem for DecideCredulousComplete {
}
fn check(&self, aba: &Aba) -> Result {
if aba.contains_assumption(&self.element) {
if aba.contains_atom(&self.element) {
Ok(())
} else {
Err(Error::ProblemCheckFailed(format!(

4
src/aba/problems/conflict_free.rs
View file

@ -1,7 +1,7 @@
use std::collections::HashSet;
use crate::{
aba::{Aba, Num, Theory},
aba::{prepared::PreparedAba, Aba, Num, Theory},
clauses::{Clause, ClauseList},
error::Error,
literal::{IntoLiteral, TheoryAtom},
@ -17,7 +17,7 @@ pub struct ConflictFreeness {
impl Problem for ConflictFreeness {
type Output = bool;
fn additional_clauses(&self, aba: &Aba) -> ClauseList {
fn additional_clauses(&self, aba: &PreparedAba) -> ClauseList {
let mut clauses = vec![];
// Make sure that every assumption in our problem is inferred and every other not
for assumption in aba.assumptions() {

27
src/aba/problems/mod.rs
View file

@ -1,12 +1,12 @@
use cadical::Solver;
use crate::{
clauses::{Atom, ClauseList},
clauses::ClauseList,
error::{Error, Result},
mapper::Mapper,
};
use super::{Aba, Num};
use super::{prepared::PreparedAba, Aba, Num, Theory};
pub mod admissibility;
pub mod complete;
@ -28,7 +28,7 @@ pub struct SolverState<'a> {
#[doc(notable_trait)]
pub trait Problem {
type Output;
fn additional_clauses(&self, aba: &Aba) -> ClauseList;
fn additional_clauses(&self, aba: &PreparedAba) -> ClauseList;
fn construct_output(self, state: SolverState<'_>) -> Self::Output;
fn check(&self, _aba: &Aba) -> Result {
@ -37,9 +37,9 @@ pub trait Problem {
}
#[doc(notable_trait)]
pub trait MultishotProblem<A: Atom> {
pub trait MultishotProblem {
type Output;
fn additional_clauses(&self, aba: &Aba, iteration: usize) -> ClauseList;
fn additional_clauses(&self, aba: &PreparedAba, iteration: usize) -> ClauseList;
fn feedback(&mut self, state: SolverState<'_>) -> LoopControl;
fn construct_output(self, state: SolverState<'_>, total_iterations: usize) -> Self::Output;
@ -58,9 +58,8 @@ impl From<Num> for SetTheory {
}
}
pub fn solve<P: Problem>(problem: P, mut aba: Aba) -> Result<P::Output> {
// Trim the ABA, this is always safe
aba.trim();
pub fn solve<P: Problem>(problem: P, aba: Aba) -> Result<P::Output> {
let aba = aba.prepare();
// Let the problem perform additional checks before starting the solver
problem.check(&aba)?;
// Create a map that will keep track of the translation between
@ -69,7 +68,7 @@ pub fn solve<P: Problem>(problem: P, mut aba: Aba) -> Result<P::Output> {
// Instantiate a new SAT solver instance
let mut sat: Solver = Solver::default();
// Derive clauses from the ABA
let clauses = aba.derive_clauses();
let clauses: ClauseList = aba.derive_clauses::<Theory>().collect();
// Append additional clauses as defined by the problem
let additional_clauses = problem.additional_clauses(&aba);
// Convert the total of our derived clauses using the mapper
@ -99,12 +98,8 @@ pub fn solve<P: Problem>(problem: P, mut aba: Aba) -> Result<P::Output> {
}
}
pub fn multishot_solve<A: Atom, P: MultishotProblem<A>>(
mut problem: P,
mut aba: Aba,
) -> Result<P::Output> {
// Trim the ABA, this is always safe
aba.trim();
pub fn multishot_solve<P: MultishotProblem>(mut problem: P, aba: Aba) -> Result<P::Output> {
let aba = aba.prepare();
// Let the problem perform additional checks before starting the solver
problem.check(&aba)?;
// Create a map that will keep track of the translation between
@ -113,7 +108,7 @@ pub fn multishot_solve<A: Atom, P: MultishotProblem<A>>(
// Instantiate a new SAT solver instance
let mut sat: Solver = Solver::default();
// Derive clauses from the ABA
let clauses = aba.derive_clauses();
let clauses: ClauseList = aba.derive_clauses::<Theory>().collect();
// Convert the total of our derived clauses using the mapper
// and feed the solver with the result
map.as_raw_iter(&clauses)

101
src/aba/theory.rs Normal file
View file

@ -0,0 +1,101 @@
use std::collections::{HashMap, HashSet};
use crate::{
clauses::{Clause, ClauseList},
literal::{IntoLiteral, Literal, TheoryAtom},
};
use super::{prepared::PreparedAba, Num, TheoryHelper};
/// Generate the logic for theory derivation in the given [`Aba`]
///
/// This will need a valid [`TheoryAtom`] that will be used to construct the logic
///
/// # Explanation
///
/// We will mainly operate on heads of rules here. So consider head `p` and all bodies `b`
/// in the set of all bodies of `p`: `bodies(p)`.
/// Every body `b` in `bodies(p)` is a set of atoms. Any set of atoms (any body) can be
/// used to derive `p`. So the following relation must hold:
/// - if `p` is true, at least one body `b` must be true aswell.
/// this only holds, because `p` itself is not assumption (since we're
/// only talking flat ABA)
/// - if `b` in `bodies(p)` is true, `p` must be true aswell
///
/// The entire logic in this function is required to implement this equality in DNF.
///
/// # Extra steps
///
/// - We do some extra work here to prevent atoms that never occur in the head of rule and
/// are not an assumption from ever being true.
/// - heads with a single body are common enough in practice to benefit from special care.
/// A lot of the overhead is due to the fact that multiple bodies are an option, if that's
/// not given for a head `p` we use the simplified translation logic where `p` is true iff
/// `bodies(p)` is true.
pub fn theory_helper<I: TheoryAtom>(aba: &PreparedAba) -> impl Iterator<Item = Clause> + '_ {
// The combined list of rules, such that every
// head is unique and possible contains a list of bodies
let mut rules_combined =
aba.rules
.iter()
.fold(HashMap::<_, Vec<_>>::new(), |mut rules, (head, body)| {
rules.entry(head).or_default().push(body);
rules
});
// All atoms that can be derived by rules
let rule_heads: HashSet<_> = aba.rule_heads().collect();
// For every non-assumption, that is not derivable add a rule without a body,
// such that it cannot be derived at all. This is to prevent the solver from
// guessing this atom on it's own
aba.universe()
.filter(|atom| !aba.contains_assumption(atom))
.filter(|atom| !rule_heads.contains(atom))
.map(|atom| (atom, vec![]))
.collect_into(&mut rules_combined);
// All combined rules
// These are heads with any number of bodies, possibly none
rules_combined
.into_iter()
.flat_map(|(head, bodies)| match &bodies[..] {
// No bodies, add a clause that prevents the head from accuring in the theory
[] => {
vec![Clause::from(vec![I::new(*head).neg()])]
}
// A single body only, this is equivalent to a head that can only be derived by a single rule
[body] => body_to_clauses::<I>(I::new(*head).pos(), body),
// n bodies, we'll need to take extra care to allow any number of bodies to derive this
// head without logic errors
bodies => {
let mut clauses = vec![];
bodies
.iter()
.enumerate()
.flat_map(|(idx, body)| {
body_to_clauses::<I>(TheoryHelper::<I>::new(idx, *head).pos(), body)
})
.collect_into(&mut clauses);
let helpers: Vec<_> = (0..bodies.len())
.map(|idx| TheoryHelper::<I>::new(idx, *head).pos())
.collect();
let mut right_implification: Clause = helpers.iter().cloned().collect();
right_implification.push(I::new(*head).neg());
clauses.push(right_implification);
helpers
.into_iter()
.map(|helper| Clause::from(vec![I::new(*head).pos(), helper.negative()]))
.collect_into(&mut clauses);
clauses
}
})
}
fn body_to_clauses<I: TheoryAtom>(head: Literal, body: &HashSet<Num>) -> ClauseList {
let mut clauses = vec![];
let mut left_implication: Clause = body.iter().map(|elem| I::new(*elem).neg()).collect();
left_implication.push(head.clone().positive());
clauses.push(left_implication);
body.iter()
.map(|elem| vec![head.clone().negative(), I::new(*elem).pos()].into())
.collect_into(&mut clauses);
clauses
}

12
src/clauses.rs
View file

@ -1,8 +1,4 @@
use std::{
fmt::{Debug, Display},
hash::Hash,
ops::{Deref, DerefMut},
};
use std::ops::{Deref, DerefMut};
use crate::literal::Literal;
@ -10,12 +6,6 @@ pub type ClauseList = Vec<Clause>;
pub type RawClause = Vec<RawLiteral>;
pub type RawLiteral = i32;
/// Generic Atom that can be used to construct [`Clause`]s.
#[doc(notable_trait)]
pub trait Atom: Debug + Display + Hash + Eq + Clone + 'static {}
impl<A: Debug + Display + Hash + Eq + Clone + 'static> Atom for A {}
/// A disjunction of [`Literal`]s.
pub struct Clause {
list: Vec<Literal>,

180
src/graph/mod.rs
View file

@ -21,80 +21,112 @@
//! 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)]
use std::collections::{BTreeMap, BTreeSet, HashSet};
use crate::aba::Num;
#[derive(Debug)]
pub struct Graph {
n: usize,
adj_list: Vec<Vec<usize>>,
adj_list: BTreeMap<Num, Vec<Num>>,
}
impl Graph {
pub fn new(n: usize) -> Self {
pub fn new() -> Self {
Self {
n,
adj_list: vec![vec![]; n],
adj_list: BTreeMap::new(),
}
}
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>>,
#[cfg(test)]
pub fn add_vertex(&mut self, vertex: Num) {
self.adj_list.entry(vertex).or_default();
}
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(),
};
pub fn add_edge(&mut self, from: Num, to: Num) {
self.adj_list.entry(from).or_default().push(to);
}
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]);
}
pub fn tarjan_scc(&self) -> Vec<HashSet<Num>> {
struct TarjanState {
index: i32,
stack: Vec<Num>,
on_stack: BTreeSet<Num>,
index_of: BTreeMap<Num, i32>,
lowlink_of: BTreeMap<Num, i32>,
components: Vec<HashSet<Num>>,
}
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;
let mut state = TarjanState {
index: 0,
stack: Vec::new(),
on_stack: Default::default(),
index_of: Default::default(),
lowlink_of: Default::default(),
components: Vec::new(),
};
fn strong_connect(v: Num, graph: &Graph, state: &mut TarjanState) {
state.index_of.insert(v, state.index);
state.lowlink_of.insert(v, state.index);
state.index += 1;
state.stack.push(v);
state.on_stack.insert(v);
for &w in graph.adj_list.get(&v).unwrap_or(&vec![]) {
if !state.index_of.contains_key(&w) {
strong_connect(w, graph, state);
let curr = state.lowlink_of.get(&v).cloned();
let other = state.lowlink_of.get(&w).cloned();
match (curr, other) {
(Some(curr), Some(other)) => {
state.lowlink_of.insert(v, curr.min(other));
}
(Some(first), None) | (None, Some(first)) => {
state.lowlink_of.insert(v, first);
}
(None, None) => {
state.lowlink_of.remove(&v);
}
}
} else if state.on_stack.contains(&w) {
let curr = state.lowlink_of.get(&v).cloned();
let other = state.index_of.get(&w).cloned();
match (curr, other) {
(Some(curr), Some(other)) => {
state.lowlink_of.insert(v, curr.min(other));
}
(Some(first), None) | (None, Some(first)) => {
state.lowlink_of.insert(v, first);
}
(None, None) => {
state.lowlink_of.remove(&v);
}
}
}
}
state.components.push(component);
}
}
for v in 0..graph.n {
if state.index_of[v] == -1 {
strong_connect(v, graph, &mut state);
if state.lowlink_of.get(&v) == state.index_of.get(&v) {
let mut component = HashSet::new();
while let Some(w) = state.stack.pop() {
state.on_stack.remove(&w);
component.insert(w);
if w == v {
break;
}
}
state.components.push(component);
}
}
}
state.components
for v in self.adj_list.keys() {
if !state.index_of.contains_key(v) {
strong_connect(*v, self, &mut state);
}
}
state.components
}
}
#[cfg(test)]
@ -124,52 +156,55 @@ mod tests {
(8, 9),
(9, 8),
];
let mut graph = Graph::new(n_vertices);
let mut graph = Graph::new();
(0..n_vertices).for_each(|v| graph.add_vertex(v));
for &(u, v) in &edges {
graph.add_edge(u, v);
}
let components = tarjan_scc(&graph);
let components = graph.tarjan_scc();
assert_eq!(
components,
vec![
vec![8, 9],
vec![7],
vec![5, 4, 6],
vec![3, 2, 1, 0],
vec![10],
set![8, 9],
set![7],
set![5, 4, 6],
set![3, 2, 1, 0],
set![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);
let edges = vec![];
let mut graph = Graph::new();
(0..n_vertices).for_each(|v| graph.add_vertex(v));
for &(u, v) in &edges {
graph.add_edge(u, v);
}
let components = tarjan_scc(&graph);
let components = graph.tarjan_scc();
// Each node is its own SCC
assert_eq!(
components,
vec![vec![0], vec![1], vec![2], vec![3], vec![4]]
vec![set![0], set![1], set![2], set![3], set![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);
let mut graph = Graph::new();
(0..n_vertices).for_each(|v| graph.add_vertex(v));
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]]);
let components = graph.tarjan_scc();
assert_eq!(components, vec![set![4, 3, 2, 1, 0]]);
// Test 4: A graph with multiple strongly connected component
let n_vertices = 7;
@ -183,16 +218,17 @@ mod tests {
(3, 5),
(4, 5),
];
let mut graph = Graph::new(n_vertices);
let mut graph = Graph::new();
(0..n_vertices).for_each(|v| graph.add_vertex(v));
for &(u, v) in &edges {
graph.add_edge(u, v);
}
let components = tarjan_scc(&graph);
let components = graph.tarjan_scc();
assert_eq!(
components,
vec![vec![5], vec![3], vec![4], vec![6], vec![2, 1, 0],]
vec![set![5], set![3], set![4], set![6], set![2, 1, 0],]
);
}
}

16
src/tests/mod.rs
View file

@ -187,7 +187,6 @@ fn a_chain_with_no_beginning() {
}
#[test]
#[ignore]
fn loops_and_conflicts() {
let aba = DebugAba::default()
.with_assumption('a', 'b')
@ -201,3 +200,18 @@ fn loops_and_conflicts() {
.unwrap();
assert!(!result, "d cannot be credulous complete");
}
#[test]
fn loops_and_conflicts_2() {
let aba = DebugAba::default()
.with_assumption('a', 'e')
.with_assumption('b', 'f')
.with_rule('c', ['d'])
.with_rule('d', ['c'])
.with_rule('d', ['a']);
let element = aba.forward_atom('b').unwrap();
let result =
crate::aba::problems::solve(DecideCredulousComplete { element }, aba.aba().clone())
.unwrap();
assert!(result, "b is credulous complete");
}