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

performance fixes done

Browse source
This commit is contained in:
Malte Tammena 2024-04-18 22:19:51 +02:00
parent 3dc977482f
commit 4590221966
13 changed files with 134 additions and 145 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
Cargo.lock generated
View file

@ -10,6 +10,7 @@ dependencies = [
"clap",
"graph-cycles",
"iter_tools",
"lazy_static",
"nom",
"petgraph",
"thiserror",
@ -253,6 +254,12 @@ dependencies = [
"libc",
]
[[package]]
name = "lazy_static"
version = "1.4.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
[[package]]
name = "libc"
version = "0.2.153"

1
Cargo.toml
View file

@ -12,6 +12,7 @@ cadical = "0.1.14"
clap = { version = "4.4.8", features = ["wrap_help", "derive"] }
graph-cycles = "0.1.0"
iter_tools = "0.10.0"
lazy_static = "1.4.0"
nom = "7.1.3"
petgraph = "0.6.4"
thiserror = "1.0.50"

2
src/aba/debug.rs
View file

@ -20,7 +20,7 @@ impl DebugAba {
self
}
pub fn with_rule<'n, B: IntoIterator<Item = char>>(mut self, head: char, body: B) -> Self {
pub fn with_rule<B: IntoIterator<Item = char>>(mut self, head: char, body: B) -> Self {
let head = self.forward(head);
let body: Vec<_> = body
.into_iter()

18
src/aba/mod.rs
View file

@ -27,6 +27,8 @@
//! ```
use std::collections::{HashMap, HashSet};
use crate::literal::RawLiteral;
use self::prepared::PreparedAba;
pub mod debug;
@ -80,6 +82,7 @@ impl Aba {
self.universe().any(|e| *e == *elem)
}
#[cfg(debug_assertions)]
pub fn size(&self) -> usize {
let inverses = self
.inverses
@ -102,3 +105,18 @@ impl Aba {
self.rules.iter().map(|(head, _)| head)
}
}
pub trait Context {
type Base: From<Num> + Into<RawLiteral> + 'static;
type Rule: From<usize> + Into<RawLiteral> + 'static;
}
impl Context for crate::literal::lits::Theory {
type Base = Self;
type Rule = crate::literal::lits::TheoryRuleBodyActive;
}
impl Context for crate::literal::lits::TheorySet {
type Base = Self;
type Rule = crate::literal::lits::TheorySetRuleBodyActive;
}

69
src/aba/prepared.rs
View file

@ -1,26 +1,19 @@
use std::{
collections::{BTreeMap, HashSet},
fs::File,
io::Write,
};
use std::collections::{BTreeMap, HashSet};
use graph_cycles::Cycles;
use iter_tools::Itertools;
use petgraph::{
dot::{Config, Dot},
graph::DiGraph,
};
use crate::{
aba::Num,
args::ARGS,
clauses::Clause,
literal::{
lits::{LoopHelper, TheoryRuleBodyActive},
IntoLiteral, RawLiteral,
IntoLiteral,
},
};
use super::{theory::theory_helper, Aba};
use super::{theory::theory_helper, Aba, Context};
#[derive(Debug, Clone, PartialEq, Eq)]
struct r#Loop {
@ -36,16 +29,10 @@ pub struct PreparedAba {
impl PreparedAba {
/// Translate the ABA into base rules / definitions for SAT solving
pub fn derive_clauses<
Theory: From<Num> + Into<RawLiteral> + 'static,
Helper: From<(usize, Num)> + Into<RawLiteral> + 'static,
TheoryRuleActive: From<usize> + Into<RawLiteral> + 'static,
>(
&self,
) -> impl Iterator<Item = Clause> + '_ {
theory_helper::<Theory, Helper>(self)
.chain(self.derive_loop_breaker::<Theory>())
.chain(self.derive_rule_helper::<Theory, TheoryRuleActive>())
pub fn derive_clauses<Ctx: Context>(&self) -> impl Iterator<Item = Clause> + '_ {
theory_helper::<Ctx>(self)
.chain(self.derive_loop_breaker::<Ctx>())
.chain(self.derive_rule_helper::<Ctx>())
}
/// Derive [`Clause`]s to ground the found loops
@ -78,9 +65,7 @@ impl PreparedAba {
/// ⋄ -l or LH_i
/// ```
/// This will result in `|L| + 1` new clauses per loop.
fn derive_loop_breaker<Theory: From<Num> + IntoLiteral>(
&self,
) -> impl Iterator<Item = Clause> + '_ {
fn derive_loop_breaker<Ctx: Context>(&self) -> impl Iterator<Item = Clause> + '_ {
// Iterate over all loops
self.loops.iter().enumerate().flat_map(|(loop_id, r#loop)| {
// -LH_i or RBA_1 or ... or RBA_n
@ -94,7 +79,7 @@ impl PreparedAba {
let head_clauses = r#loop.heads.iter().map(move |head| {
Clause::from(vec![
LoopHelper::from(loop_id).pos(),
Theory::from(*head).neg(),
Ctx::Base::from(*head).neg(),
])
});
// LH_i or -RBA_x
@ -118,30 +103,25 @@ impl PreparedAba {
/// RBA_i <=> b_1 and ... and b_n
/// ⋄ (-RBA_i or b_1) and ... and (-RBA_i or b_n) and (RBA_i or -b_1 or ... or -b_n)
/// ```
/// we will use [`RuleBodyActive`] for `x_R`.
fn derive_rule_helper<
Theory: From<Num> + Into<RawLiteral> + 'static,
TheoryRuleActive: From<usize> + Into<RawLiteral> + 'static,
>(
&self,
) -> impl Iterator<Item = Clause> + '_ {
/// we will use the `TheoryRuleActive` for `x_R`.
fn derive_rule_helper<Ctx: Context>(&self) -> impl Iterator<Item = Clause> + '_ {
self.rules
.iter()
.enumerate()
.flat_map(|(rule_id, (_head, body))| {
if body.is_empty() {
vec![Clause::from(vec![TheoryRuleActive::from(rule_id).neg()])]
vec![Clause::from(vec![Ctx::Rule::from(rule_id).neg()])]
} else {
let last_clause = body
.iter()
.map(|el| Theory::from(*el).neg())
.chain(std::iter::once(TheoryRuleActive::from(rule_id).pos()))
.map(|el| Ctx::Base::from(*el).neg())
.chain(std::iter::once(Ctx::Rule::from(rule_id).pos()))
.collect();
body.iter()
.map(move |el| {
Clause::from(vec![
TheoryRuleActive::from(rule_id).neg(),
Theory::from(*el).pos(),
Ctx::Rule::from(rule_id).neg(),
Ctx::Base::from(*el).pos(),
])
})
.chain([last_clause])
@ -183,7 +163,7 @@ fn trim_unreachable_rules(aba: &mut Aba) {
}
fn calculate_loops_and_their_support(aba: &Aba) -> Vec<r#Loop> {
let mut graph = DiGraph::<Num, ()>::new();
let mut graph = petgraph::graph::DiGraph::<Num, ()>::new();
let universe = aba
.universe()
.unique()
@ -202,12 +182,18 @@ fn calculate_loops_and_their_support(aba: &Aba) -> Vec<r#Loop> {
});
#[cfg(debug_assertions)]
{
use std::{fs::File, io::Write};
let mut file = File::create("./graph.gv").unwrap();
let dot = Dot::with_config(&graph, &[Config::EdgeNoLabel]);
let dot = petgraph::dot::Dot::with_config(&graph, &[petgraph::dot::Config::EdgeNoLabel]);
write!(file, "{dot:?}").unwrap();
}
let mut loops = vec![];
const LOOP_SIZE_IN_MULT_UNIVERSE_SIZE: f32 = 0.2;
const LOOP_SIZE_IN_MULT_UNIVERSE_SIZE: f32 = 1.0;
let max_loops = if let Some(max) = ARGS.as_ref().and_then(|args| args.max_loops) {
max
} else {
(universe.len() as f32 * LOOP_SIZE_IN_MULT_UNIVERSE_SIZE) as usize
};
let mut output_printed = false;
graph.visit_cycles(|graph, cycle| {
let heads = cycle.iter().map(|idx| graph[*idx]).collect::<HashSet<_>>();
@ -223,7 +209,7 @@ fn calculate_loops_and_their_support(aba: &Aba) -> Vec<r#Loop> {
.map(|(rule_id, _)| rule_id)
.collect();
loops.push(r#Loop { heads, support });
if loops.len() >= (LOOP_SIZE_IN_MULT_UNIVERSE_SIZE * universe.len() as f32) as usize {
if loops.len() >= max_loops {
if ! output_printed {
eprintln!("Too... many... cycles... Aborting cycle detection with {} cycles. Solver? You're on your own now", loops.len());
output_printed = true;
@ -233,6 +219,7 @@ fn calculate_loops_and_their_support(aba: &Aba) -> Vec<r#Loop> {
std::ops::ControlFlow::Continue(())
}
});
eprintln!("{}", loops.len());
loops
}

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

@ -6,7 +6,7 @@ use crate::{
clauses::{Clause, ClauseList},
error::Error,
literal::{
lits::{Theory, TheorySet, TheorySetHelper, TheorySetRuleBodyActive},
lits::{Theory, TheorySet},
IntoLiteral,
},
Result,
@ -38,8 +38,7 @@ pub struct DecideCredulousAdmissibility {
pub fn initial_admissibility_clauses(aba: &PreparedAba) -> ClauseList {
let mut clauses = vec![];
// Create inference for the problem set
aba.derive_clauses::<TheorySet, TheorySetHelper, TheorySetRuleBodyActive>()
.collect_into(&mut clauses);
aba.derive_clauses::<TheorySet>().collect_into(&mut clauses);
// Attack the inference of the aba, if an attack exists
for (assumption, inverse) in &aba.inverses {
[

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

@ -3,7 +3,7 @@ use cadical::Solver;
use crate::{
clauses::ClauseList,
error::{Error, Result},
literal::lits::{Theory, TheoryHelper, TheoryRuleBodyActive},
literal::lits::Theory,
mapper::Mapper,
};
@ -59,9 +59,7 @@ pub fn solve<P: Problem>(problem: P, aba: Aba) -> Result<P::Output> {
// Instantiate a new SAT solver instance
let mut sat: Solver = Solver::default();
// Derive clauses from the ABA
let clauses: ClauseList = aba
.derive_clauses::<Theory, TheoryHelper, TheoryRuleBodyActive>()
.collect();
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
@ -101,9 +99,7 @@ pub fn multishot_solve<P: MultishotProblem>(mut problem: P, aba: Aba) -> Result<
// Instantiate a new SAT solver instance
let mut sat: Solver = Solver::default();
// Derive clauses from the ABA
let clauses: ClauseList = aba
.derive_clauses::<Theory, TheoryHelper, TheoryRuleBodyActive>()
.collect();
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)

99
src/aba/theory.rs
View file

@ -1,15 +1,10 @@
use std::collections::{HashMap, HashSet};
use crate::{
clauses::{Clause, ClauseList},
literal::{IntoLiteral, Literal, RawLiteral},
};
use crate::{clauses::Clause, literal::IntoLiteral};
use super::{prepared::PreparedAba, Num};
use super::{prepared::PreparedAba, Context};
/// Generate the logic for theory derivation in the given [`Aba`]
///
/// This will need a valid [`TheoryAtom`] that will be used to construct the logic
/// Generate the logic for theory derivation in the given [`Aba`](crate::aba::Aba)
///
/// # Explanation
///
@ -32,21 +27,16 @@ use super::{prepared::PreparedAba, Num};
/// 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<
Theory: From<Num> + Into<RawLiteral>,
Helper: From<(usize, Num)> + Into<RawLiteral>,
>(
aba: &PreparedAba,
) -> impl Iterator<Item = Clause> + '_ {
pub fn theory_helper<Ctx: Context>(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
});
// head is unique and possible contains a list of body rule ids
let mut rules_combined = aba.rules.iter().enumerate().fold(
HashMap::<_, Vec<_>>::new(),
|mut rules, (rule_id, (head, _body))| {
rules.entry(head).or_default().push(rule_id);
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,
@ -61,49 +51,48 @@ pub fn theory_helper<
// These are heads with any number of bodies, possibly none
rules_combined
.into_iter()
.flat_map(|(head, bodies)| match &bodies[..] {
.flat_map(|(head, rule_ids)| match &rule_ids[..] {
// No bodies, add a clause that prevents the head from accuring in the theory
[] => {
vec![Clause::from(vec![Theory::from(*head).neg()])]
vec![Clause::from(vec![Ctx::Base::from(*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::<Theory>(Theory::from(*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 => {
// H <=> RBA_rule_id
[rule_id] => {
vec![
Clause::from(vec![
Ctx::Base::from(*head).pos(),
Ctx::Rule::from(*rule_id).neg(),
]),
Clause::from(vec![
Ctx::Base::from(*head).neg(),
Ctx::Rule::from(*rule_id).pos(),
]),
]
}
// n bodies for this head
// ```text
// H <=> RBA_1 or ... or RBA_n
// ⋄ (-H or RBA_1 or ... or RBA_n) and (-RBA_1 or H) and ... (-RBA_n or H)
// ````
rule_ids => {
let mut clauses = vec![];
bodies
rule_ids
.iter()
.enumerate()
.flat_map(|(idx, body)| {
body_to_clauses::<Theory>(Helper::from((idx, *head)).pos(), body)
.map(|rule_id| {
Clause::from(vec![
Ctx::Base::from(*head).pos(),
Ctx::Rule::from(*rule_id).neg(),
])
})
.collect_into(&mut clauses);
let helpers: Vec<_> = (0..bodies.len())
.map(|idx| Helper::from((idx, *head)).pos())
let last_clause = rule_ids
.iter()
.map(|rule_id| Ctx::Rule::from(*rule_id).pos())
.chain(std::iter::once(Ctx::Base::from(*head).neg()))
.collect();
let mut right_implification: Clause = helpers.iter().cloned().collect();
right_implification.push(Theory::from(*head).neg());
clauses.push(right_implification);
helpers
.into_iter()
.map(|helper| Clause::from(vec![Theory::from(*head).pos(), helper.negative()]))
.collect_into(&mut clauses);
clauses.push(last_clause);
clauses
}
})
}
fn body_to_clauses<Theory: From<Num> + Into<RawLiteral>>(
head: Literal,
body: &HashSet<Num>,
) -> ClauseList {
let mut clauses = vec![];
let mut left_implication: Clause = body.iter().map(|elem| Theory::from(*elem).neg()).collect();
left_implication.push(head.clone().positive());
clauses.push(left_implication);
body.iter()
.map(|elem| vec![head.clone().negative(), Theory::from(*elem).pos()].into())
.collect_into(&mut clauses);
clauses
}

12
src/args.rs
View file

@ -1,6 +1,11 @@
use std::path::PathBuf;
use clap::{Parser, Subcommand};
use lazy_static::lazy_static;
lazy_static! {
pub static ref ARGS: Option<Args> = Args::try_parse().ok();
}
#[derive(Debug, Parser)]
#[command(
@ -17,8 +22,13 @@ use clap::{Parser, Subcommand};
pub struct Args {
#[command(subcommand)]
pub problem: Problems,
#[arg(long, short)]
/// File to load the aba from
#[arg(long, short, value_name = "PATH")]
pub file: PathBuf,
/// Maximum number of loops to break before starting the solving process.
/// Will use the number of atoms by default.
#[arg(long, short = 'l', value_name = "COUNT")]
pub max_loops: Option<usize>,
}
#[allow(clippy::enum_variant_names)]

26
src/literal.rs
View file

@ -44,10 +44,6 @@ pub mod lits {
pub struct Theory(Num);
into_raw!(Theory from Num);
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct TheoryHelper(usize, Num);
into_raw!(TheoryHelper from usize, Num);
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct TheoryRuleBodyActive(usize);
into_raw!(TheoryRuleBodyActive from usize);
@ -56,10 +52,6 @@ pub mod lits {
pub struct TheorySet(Num);
into_raw!(TheorySet from Num);
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct TheorySetHelper(usize, Num);
into_raw!(TheorySetHelper from usize, Num);
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct TheorySetRuleBodyActive(usize);
into_raw!(TheorySetRuleBodyActive from usize);
@ -83,10 +75,8 @@ pub enum Literal {
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum RawLiteral {
Theory(lits::Theory),
TheoryHelper(lits::TheoryHelper),
TheoryRuleBodyActive(lits::TheoryRuleBodyActive),
TheorySet(lits::TheorySet),
TheorySetHelper(lits::TheorySetHelper),
TheorySetRuleBodyActive(lits::TheorySetRuleBodyActive),
LoopHelper(lits::LoopHelper),
}
@ -113,22 +103,6 @@ impl<T: Into<RawLiteral>> IntoLiteral for T {
}
}
impl Literal {
pub fn negative(self) -> Self {
Self::Neg(self.into_inner())
}
pub fn positive(self) -> Self {
Self::Pos(self.into_inner())
}
pub fn into_inner(self) -> RawLiteral {
match self {
Literal::Pos(inner) | Literal::Neg(inner) => inner,
}
}
}
impl std::ops::Deref for Literal {
type Target = RawLiteral;

18
src/main.rs
View file

@ -14,6 +14,7 @@ use aba::{
},
Num,
};
use args::ARGS;
use clap::Parser;
use crate::error::{Error, Result};
@ -40,14 +41,19 @@ trait IccmaFormattable {
}
fn __main() -> Result {
let args = args::Args::parse();
let args = match &*ARGS {
Some(args) => args,
None => {
args::Args::parse();
unreachable!()
}
};
let content = read_to_string(&args.file).map_err(Error::OpeningAbaFile)?;
let aba = parser::aba_file(&content)?;
let result = match args.problem {
let result = match &args.problem {
args::Problems::VerifyAdmissibility { set } => aba::problems::solve(
VerifyAdmissibleExtension {
assumptions: set.into_iter().collect(),
assumptions: set.iter().cloned().collect(),
},
aba,
)?
@ -60,13 +66,13 @@ fn __main() -> Result {
aba::problems::solve(SampleAdmissibleExtension, aba)?.fmt_iccma()
}
args::Problems::DecideCredulousAdmissibility { query } => {
aba::problems::solve(DecideCredulousAdmissibility { element: query }, aba)?.fmt_iccma()
aba::problems::solve(DecideCredulousAdmissibility { element: *query }, aba)?.fmt_iccma()
}
args::Problems::EnumerateComplete => {
aba::problems::multishot_solve(EnumerateCompleteExtensions::default(), aba)?.fmt_iccma()
}
args::Problems::DecideCredulousComplete { query } => {
aba::problems::solve(DecideCredulousComplete { element: query }, aba)?.fmt_iccma()
aba::problems::solve(DecideCredulousComplete { element: *query }, aba)?.fmt_iccma()
}
}?;
let mut stdout = std::io::stdout().lock();

8
src/mapper.rs
View file

@ -1,7 +1,5 @@
use std::collections::HashMap;
use cadical::Solver;
use crate::{
clauses::{Clause, RawClause},
literal::{Literal, RawLiteral},
@ -41,7 +39,11 @@ impl Mapper {
}
}
pub fn reconstruct<'s>(&'s self, sat: &'s Solver) -> impl Iterator<Item = Literal> + 's {
#[cfg(debug_assertions)]
pub fn reconstruct<'s>(
&'s self,
sat: &'s cadical::Solver,
) -> impl Iterator<Item = Literal> + 's {
self.map.iter().flat_map(|(lit, raw)| {
sat.value(*raw as i32).map(|result| match result {
true => Literal::Pos(*lit),

4
src/parser.rs
View file

@ -39,11 +39,11 @@ use crate::aba::{Aba, Num};
use crate::error::Result;
pub fn aba_file(input: &str) -> Result<Aba> {
let (input, number_of_atoms) = p_line(input)?;
let (input, _number_of_atoms) = p_line(input)?;
let (_, aba) = all_consuming(aba)(input)?;
#[cfg(debug_assertions)]
{
if aba.size() != number_of_atoms as usize {
if aba.size() != _number_of_atoms as usize {
eprintln!("Number of atoms did not match p-line!");
}
}