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

fix admissibility, unify with verification

Browse source
This commit is contained in:
Malte Tammena 2023-12-07 15:13:15 +01:00
parent 7b24b2b96a
commit 328cd79636
7 changed files with 213 additions and 205 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -4,56 +4,42 @@ use crate::{
aba::{inference_helper, Aba, Inference},
clauses::{Atom, Clause, ClauseList},
literal::{InferenceAtom, InferenceAtomHelper, IntoLiteral},
mapper::Mapper,
};
use super::{LoopControl, MultishotProblem};
use super::{LoopControl, MultishotProblem, Problem, SolverState};
#[derive(Default, Debug)]
pub struct Admissibility<A: Atom> {
found: Vec<HashSet<A>>,
}
pub struct VerifyAdmissibility<A: Atom> {
pub assumptions: Vec<A>,
}
#[derive(Debug)]
pub struct SetInference<A: Atom>(A);
#[derive(Debug)]
pub struct SetInferenceHelper<A: Atom>(usize, A);
impl<A: Atom> MultishotProblem<A> for Admissibility<A> {
type Output = Vec<HashSet<A>>;
fn additional_clauses(&self, aba: &Aba<A>, iteration: usize) -> ClauseList {
match iteration {
0 => {
fn initial_clauses<A: Atom>(aba: &Aba<A>) -> ClauseList {
let mut clauses = vec![];
// Create inference for the problem set
inference_helper::<SetInference<_>, _>(aba).collect_into(&mut clauses);
// Prevent the empty set
let no_empty_set: Clause = aba
.inverses
.keys()
.map(|assumption| SetInference::new(assumption.clone()).pos())
.collect();
clauses.push(no_empty_set);
// Attack the inference of the aba, if an attack exists
for (assumption, inverse) in &aba.inverses {
[
// For any assumption `a` and it's inverse `b`:
// Inference(a) <=> not SetInference(b) and not SetInference(a)
// Inference(a) <=> not SetInference(b)
Clause::from(vec![
Inference::new(assumption.clone()).pos(),
SetInference::new(inverse.clone()).pos(),
]),
Clause::from(vec![
Inference::new(assumption.clone()).neg(),
SetInference::new(inverse.clone()).neg(),
]),
Clause::from(vec![
Inference::new(assumption.clone()).neg(),
SetInference::new(assumption.clone()).neg(),
]),
Clause::from(vec![
SetInference::new(inverse.clone()).pos(),
SetInference::new(assumption.clone()).pos(),
Inference::new(assumption.clone()).pos(),
]),
// Prevent attacks from the opponent to the selected set
// For any assumption `a` and it's inverse `b`:
// Inference(b) and SetInference(a) => bottom
@ -68,18 +54,68 @@ impl<A: Atom> MultishotProblem<A> for Admissibility<A> {
SetInference::new(assumption.clone()).neg(),
SetInference::new(inverse.clone()).neg(),
]),
// Prevent attacks from the set to the opponent
// For any assumption `a` and it's inverse `b`:
// Inference(a) and SetInference(b) => bottom
Clause::from(vec![
Inference::new(assumption.clone()).neg(),
SetInference::new(inverse.clone()).neg(),
]),
]
.into_iter()
.collect_into(&mut clauses);
}
clauses
}
fn construct_found_set<A: Atom>(state: SolverState<'_, A>) -> HashSet<A> {
state
.aba
.inverses
.keys()
.filter_map(|assumption| {
let literal = SetInference::new(assumption.clone()).pos();
let raw = state.map.get_raw(&literal)?;
match state.solver.value(raw) {
Some(true) => Some(assumption.clone()),
_ => None,
}
})
.collect()
}
impl<A: Atom> Problem<A> for Admissibility<A> {
type Output = HashSet<A>;
fn additional_clauses(&self, aba: &Aba<A>) -> ClauseList {
let mut clauses = initial_clauses(aba);
// Prevent the empty set
let no_empty_set: Clause = aba
.inverses
.keys()
.map(|assumption| SetInference::new(assumption.clone()).pos())
.collect();
clauses.push(no_empty_set);
clauses
}
fn construct_output(self, state: SolverState<'_, A>) -> Self::Output {
if state.sat_result {
construct_found_set(state)
} else {
HashSet::new()
}
}
}
impl<A: Atom> MultishotProblem<A> for Admissibility<A> {
type Output = Vec<HashSet<A>>;
fn additional_clauses(&self, aba: &Aba<A>, iteration: usize) -> ClauseList {
match iteration {
0 => {
let mut clauses = initial_clauses(aba);
// Prevent the empty set
let no_empty_set: Clause = aba
.inverses
.keys()
.map(|assumption| SetInference::new(assumption.clone()).pos())
.collect();
clauses.push(no_empty_set);
clauses
}
idx => {
@ -103,24 +139,19 @@ impl<A: Atom> MultishotProblem<A> for Admissibility<A> {
}
}
fn feedback(
&mut self,
aba: &Aba<A>,
sat_result: bool,
solver: &cadical::Solver,
map: &Mapper,
) -> LoopControl {
if !sat_result {
fn feedback(&mut self, state: SolverState<'_, A>) -> LoopControl {
if !state.sat_result {
return LoopControl::Stop;
}
// TODO: Somehow query the mapper about things instead of this
let found = aba
let found = state
.aba
.inverses
.keys()
.filter_map(|assumption| {
let literal = SetInference::new(assumption.clone()).pos();
let raw = map.get_raw(&literal)?;
match solver.value(raw) {
let raw = state.map.get_raw(&literal)?;
match state.solver.value(raw) {
Some(true) => Some(assumption.clone()),
_ => None,
}
@ -132,9 +163,7 @@ impl<A: Atom> MultishotProblem<A> for Admissibility<A> {
fn construct_output(
mut self,
_aba: &Aba<A>,
_sat_result: bool,
_solver: &cadical::Solver,
_state: SolverState<'_, A>,
_total_iterations: usize,
) -> Self::Output {
// Re-Add the empty set
@ -143,6 +172,33 @@ impl<A: Atom> MultishotProblem<A> for Admissibility<A> {
}
}
impl<A: Atom> Problem<A> for VerifyAdmissibility<A> {
type Output = bool;
fn additional_clauses(&self, aba: &Aba<A>) -> crate::clauses::ClauseList {
let mut clauses = initial_clauses(aba);
// Force inference on all members of the set
for assumption in aba.assumptions() {
let inf = SetInference::new(assumption.clone());
if self.assumptions.contains(assumption) {
clauses.push(Clause::from(vec![inf.pos()]))
} else {
clauses.push(Clause::from(vec![inf.neg()]))
}
}
clauses
}
fn construct_output(self, state: SolverState<'_, A>) -> Self::Output {
state.sat_result
}
fn check(&self, aba: &Aba<A>) -> bool {
// Make sure that every assumption is part of the ABA
self.assumptions.iter().all(|a| aba.contains_assumption(a))
}
}
impl<A: Atom> InferenceAtom<A> for SetInference<A> {
type Helper = SetInferenceHelper<A>;

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

@ -1,12 +1,10 @@
use cadical::Solver;
use crate::{
aba::{Aba, Inference, Inverse},
clauses::{Clause, ClauseList},
literal::{InferenceAtom, IntoLiteral},
};
use super::Problem;
use super::{Problem, SolverState};
pub struct ConflictFreeness {
pub assumptions: Vec<char>,
@ -44,8 +42,8 @@ impl Problem<char> for ConflictFreeness {
clauses
}
fn construct_output(self, sat_result: bool, _: &Aba<char>, _: &Solver) -> Self::Output {
sat_result
fn construct_output(self, state: SolverState<'_, char>) -> Self::Output {
state.sat_result
}
fn check(&self, aba: &Aba<char>) -> bool {

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

@ -10,7 +10,6 @@ use super::Aba;
pub mod admissibility;
pub mod conflict_free;
pub mod verify_admissibility;
#[derive(Debug, PartialEq, Eq, Clone, Copy)]
pub enum LoopControl {
@ -18,10 +17,17 @@ pub enum LoopControl {
Stop,
}
pub struct SolverState<'a, A: Atom + 'a> {
aba: &'a Aba<A>,
sat_result: bool,
solver: &'a Solver,
map: &'a Mapper,
}
pub trait Problem<A: Atom> {
type Output;
fn additional_clauses(&self, aba: &Aba<A>) -> ClauseList;
fn construct_output(self, sat_result: bool, aba: &Aba<A>, solver: &Solver) -> Self::Output;
fn construct_output(self, state: SolverState<'_, A>) -> Self::Output;
fn check(&self, _aba: &Aba<A>) -> bool {
true
@ -31,20 +37,8 @@ pub trait Problem<A: Atom> {
pub trait MultishotProblem<A: Atom> {
type Output;
fn additional_clauses(&self, aba: &Aba<A>, iteration: usize) -> ClauseList;
fn feedback(
&mut self,
aba: &Aba<A>,
sat_result: bool,
solver: &Solver,
map: &Mapper,
) -> LoopControl;
fn construct_output(
self,
aba: &Aba<A>,
sat_result: bool,
solver: &Solver,
total_iterations: usize,
) -> Self::Output;
fn feedback(&mut self, state: SolverState<'_, A>) -> LoopControl;
fn construct_output(self, state: SolverState<'_, A>, total_iterations: usize) -> Self::Output;
fn check(&self, _aba: &Aba<A>) -> bool {
true
@ -62,7 +56,12 @@ pub fn solve<A: Atom, P: Problem<A>>(problem: P, aba: &Aba<A>) -> Result<P::Outp
map.as_raw_iter(&additional_clauses)
.for_each(|raw| sat.add_clause(raw));
if let Some(sat_result) = sat.solve() {
Ok(problem.construct_output(sat_result, aba, &sat))
Ok(problem.construct_output(SolverState {
aba,
sat_result,
solver: &sat,
map: &map,
}))
} else {
Err(Error::SatCallInterrupted)
}
@ -94,11 +93,24 @@ pub fn multishot_solve<A: Atom, P: MultishotProblem<A>>(
let rec = map.reconstruct(&sat).collect::<Vec<_>>();
eprintln!("{rec:#?}");
}
let control = problem.feedback(aba, sat_result, &sat, &map);
let control = problem.feedback(SolverState {
aba,
sat_result,
solver: &sat,
map: &map,
});
if control == LoopControl::Stop {
break sat_result;
}
iteration += 1;
};
Ok(problem.construct_output(aba, final_result, &sat, iteration))
Ok(problem.construct_output(
SolverState {
aba,
sat_result: final_result,
solver: &sat,
map: &map,
},
iteration,
))
}

74
src/aba/problems/verify_admissibility.rs
View file

@ -1,74 +0,0 @@
use crate::{
aba::{inference_helper, Aba, Inference, Inverse},
clauses::{Atom, Clause},
literal::{InferenceAtom, IntoLiteral},
};
use super::{admissibility::SetInference, Problem};
pub struct VerifyAdmissibility<A: Atom> {
pub assumptions: Vec<A>,
}
impl<A: Atom> Problem<A> for VerifyAdmissibility<A> {
type Output = bool;
fn additional_clauses(&self, aba: &Aba<A>) -> crate::clauses::ClauseList {
let mut clauses = vec![];
// Create inference for the problem set
inference_helper::<SetInference<_>, _>(aba).collect_into(&mut clauses);
// Force inference on all members of the set
aba.inverses
.keys()
.cloned()
.map(|assumption| {
if self.assumptions.contains(&assumption) {
Clause::from(vec![SetInference::new(assumption).pos()])
} else {
Clause::from(vec![SetInference::new(assumption).neg()])
}
})
.collect_into(&mut clauses);
// Attack the inference of the aba, if an attack exists
for elem in aba.universe() {
for assumption in self.assumptions.iter() {
clauses.push(Clause::from(vec![
SetInference::new(assumption.clone()).neg(),
Inverse {
from: assumption.clone(),
to: elem.clone(),
}
.neg(),
Inference::new(elem.clone()).neg(),
]))
}
for assumption in aba.assumptions() {
clauses.push(Clause::from(vec![
SetInference::new(assumption.clone()).neg(),
Inverse {
from: assumption.clone(),
to: elem.clone(),
}
.neg(),
SetInference::new(elem.clone()).neg(),
]))
}
}
clauses
}
fn construct_output(
self,
sat_result: bool,
_: &crate::aba::Aba<A>,
_: &cadical::Solver,
) -> Self::Output {
sat_result
}
fn check(&self, aba: &Aba<A>) -> bool {
// Make sure that every assumption is part of the ABA
self.assumptions.iter().all(|a| aba.contains_assumption(a))
}
}

4
src/args.rs
View file

@ -21,6 +21,7 @@ pub struct Args {
pub file: PathBuf,
}
#[allow(clippy::enum_variant_names)]
#[derive(Debug, Subcommand)]
pub enum Problems {
#[clap(visible_alias = "ve-ad")]
@ -30,4 +31,7 @@ pub enum Problems {
},
#[clap(visible_alias = "ee-ad")]
EnumerateAdmissibility,
/// Will only return the empty extension if no other is found
#[clap(visible_alias = "se-ad")]
SampleAdmissibility,
}

20
src/main.rs
View file

@ -3,7 +3,7 @@
use std::{collections::HashSet, fmt::Write, fs::read_to_string};
use aba::problems::{admissibility::Admissibility, verify_admissibility::VerifyAdmissibility};
use aba::problems::admissibility::{Admissibility, VerifyAdmissibility};
use clap::Parser;
use crate::error::{Error, Result};
@ -35,10 +35,10 @@ mod tests;
fn __main() -> Result {
let args = args::Args::parse();
match args.problem {
args::Problems::VerifyAdmissibility { set } => {
let content = read_to_string(&args.file).map_err(Error::OpeningAbaFile)?;
let aba = parser::aba_file(&content)?;
match args.problem {
args::Problems::VerifyAdmissibility { set } => {
let result = aba::problems::solve(
VerifyAdmissibility {
assumptions: set.into_iter().collect(),
@ -48,11 +48,13 @@ fn __main() -> Result {
print_bool_result(result);
}
args::Problems::EnumerateAdmissibility => {
let content = read_to_string(&args.file).map_err(Error::OpeningAbaFile)?;
let aba = parser::aba_file(&content)?;
let result = aba::problems::multishot_solve(Admissibility::default(), &aba)?;
print_witnesses_result(result)?;
}
args::Problems::SampleAdmissibility => {
let result = aba::problems::solve(Admissibility::default(), &aba)?;
print_witness_result(result)?;
}
}
Ok(())
}
@ -69,8 +71,11 @@ fn print_bool_result(result: bool) {
}
fn print_witnesses_result(result: Vec<HashSet<u32>>) -> Result {
result.into_iter().try_for_each(|set| {
let set = set
result.into_iter().try_for_each(print_witness_result)
}
fn print_witness_result(result: HashSet<u32>) -> Result {
let set = result
.into_iter()
.try_fold(String::new(), |mut list, num| -> Result<_, Error> {
write!(list, " {num}")?;
@ -78,5 +83,4 @@ fn print_witnesses_result(result: Vec<HashSet<u32>>) -> Result {
})?;
println!("w{set}");
Ok(())
})
}

66
src/tests/mod.rs
View file

@ -2,21 +2,25 @@ use std::collections::HashSet;
use crate::aba::{
problems::{
admissibility::Admissibility, conflict_free::ConflictFreeness,
verify_admissibility::VerifyAdmissibility,
admissibility::{Admissibility, VerifyAdmissibility},
conflict_free::ConflictFreeness,
},
Aba,
};
#[test]
fn simple_conflict_free_verification() {
let aba = Aba::new()
fn simple_aba_example_1() -> Aba<char> {
Aba::new()
.with_assumption('a', 'r')
.with_assumption('b', 's')
.with_assumption('c', 't')
.with_rule('p', ['q', 'a'])
.with_rule('q', [])
.with_rule('r', ['b', 'c']);
.with_rule('r', ['b', 'c'])
}
#[test]
fn simple_conflict_free_verification() {
let aba = simple_aba_example_1();
let set_checks = vec![
(vec![], true),
(vec!['a'], true),
@ -40,12 +44,7 @@ fn simple_conflict_free_verification() {
#[test]
fn simple_admissible_verification() {
let aba = Aba::new()
.with_assumption('a', 'c')
.with_assumption('b', 'd')
.with_rule('c', vec!['a'])
.with_rule('c', vec!['b'])
.with_rule('d', vec!['a']);
let aba = simple_aba_example_1();
let set_checks = vec![
(vec![], true),
(vec!['a', 'b'], false),
@ -66,25 +65,34 @@ fn simple_admissible_verification() {
}
#[test]
fn simple_admissible_thing() {
let aba = Aba::new()
.with_assumption('a', 'r')
.with_assumption('b', 's')
.with_assumption('c', 't')
.with_rule('p', vec!['q', 'a'])
.with_rule('q', vec![])
.with_rule('r', vec!['b', 'c']);
let expected: Vec<HashSet<char>> = vec![
set!(),
set!('a', 'b'),
set!('a', 'c'),
set!('b'),
set!('b', 'c'),
set!('c'),
];
fn simple_admissible_example() {
let aba = simple_aba_example_1();
let expected: Vec<HashSet<char>> = vec![set!(), set!('b'), set!('b', 'c'), set!('c')];
let result = crate::aba::problems::multishot_solve(Admissibility::default(), &aba).unwrap();
for elem in &expected {
assert!(result.contains(elem));
assert!(
result.contains(elem),
"{elem:?} was expected but not found in result"
);
}
for elem in &result {
assert!(
expected.contains(elem),
"{elem:?} was found in the result, but is not expected!"
);
}
}
#[test]
fn simple_admissible_example_with_defense() {
let aba = simple_aba_example_1().with_rule('t', vec!['a', 'b']);
let expected: Vec<HashSet<char>> = vec![set!(), set!('a', 'b'), set!('b'), set!('b', 'c')];
let result = crate::aba::problems::multishot_solve(Admissibility::default(), &aba).unwrap();
for elem in &expected {
assert!(
result.contains(elem),
"{elem:?} was expected but not found in result"
);
}
for elem in &result {
assert!(