Initial commit

[?]

7tKuRek2EJdUJ3oucCiWgob6w4k1rmtABND4hJPSvjwL

Nov 23, 2023, 9:11 AM

2W5ET5PZOX3Y3LSBQOXO3DCRDON64VCDXCQUDJFTXEKBJQ5B6ASQC

Dependencies

[2] LEQGSDM7

Change contents

file addition: solver (d--r------)

[2.1]
file addition: src (d--r------)

[0.18]
file addition: solver.rs (----------)

[0.35]

use std::collections::VecDeque;
use std::usize;
// solve() uses a SolveResult generator as iterator.
use genawaiter::sync::Gen;
use log::{debug, trace};

#[derive(Copy, Clone, Debug, PartialEq, Hash, Eq, PartialOrd, Ord)]
pub struct Literal {
id: usize,
sign: bool,
}
impl Literal {
pub(crate) fn new(id: usize, sign: bool) -> Literal {
Literal { id, sign }
}
pub fn id(&self) -> usize {
self.id
}
pub fn sign(&self) -> bool {
self.sign
}
pub(crate) fn negate(&self) -> Literal {
Literal {
id: self.id,
sign: !self.sign,
}
}
}

#[test]
fn test_id() {
let lit = Literal { id: 2, sign: false };
assert_eq!(lit.id(), 2);
}

// TODO: Nogoods from a program

#[derive(Copy, Clone, Debug)]
pub(crate) struct WatchList {
pub(crate) first_watch: usize,
pub(crate) second_watch: usize,
}
#[derive(Copy, Clone, Debug, PartialEq, Eq)]
enum Watch {
First,
Second,
}
/// Solver internal representation of nogoods and assignments
type Nogood = Vec<Option<bool>>;

#[derive(Clone, Debug, PartialEq, Eq)]
pub enum SolveResult {
UnSat,
Sat(Vec<Option<bool>>),
}

#[derive(Clone, Debug, PartialEq)]
enum PropagationResult {
Ok,
Conflict(Nogood),
}
/// Map implementation used by the library.
pub(crate) type Map<K, V> = rustc_hash::FxHashMap<K, V>;

#[derive(Clone, Debug)]
pub struct Solver {
pub(crate) tight: bool,
pub(crate) number_of_variables: usize,
pub(crate) assignments: Vec<Option<bool>>,
pub(crate) decisions: Vec<Literal>,
pub(crate) watch_lists: Vec<WatchList>,
pub(crate) nogoods: Vec<Nogood>,
pub(crate) var_to_nogoods: Vec<Map<usize, bool>>,
pub(crate) nogoods_to_var: Vec<Map<usize, bool>>,
pub(crate) decision_level: usize,
pub(crate) decision_number: usize,
// Stores for each atom that has been decided the (sign, reason_index, decision_level, and decision number)
pub(crate) assignments_log: Vec<(Option<bool>, Option<usize>, usize, usize)>,
pub(crate) chronological_backtracking_level: usize,
}
impl Solver {
pub fn solve(&mut self) -> impl Iterator<Item = SolveResult> + '_ {
Gen::new(|co| async move {
let mut sat = true;

while sat {
if let PropagationResult::Conflict(nogood) = self.propagate() {
trace!("conflict with nogood: {:?}",nogood);
if self.is_top_level_conflict(&nogood) {
sat = false;
co.yield_(SolveResult::UnSat).await;
} else if self.chronological_backtracking_level < self.decision_level {
let (uip, sigma, k) = self.conflict_resolution(&nogood);
debug!("uip: {:?}", &uip);
debug!("sigma: {:?}", sigma);
debug!("k: {:?}", k);
if self.chronological_backtracking_level > k {
self.decision_level = self.chronological_backtracking_level;
} else {
self.decision_level = k;
}
debug!("new_decision_level: {}", self.decision_level);
self.backjump();

// add complement of sigma
self.decision_number += 1;
self.assignments[sigma.id] = Some(!sigma.sign);
self.assignments_log[sigma.id] =
(Some(!sigma.sign), None, k, self.decision_number);
self.record_nogood(uip);
} else {
//get decision literal from this decision_level
let decision_literal = self.decisions[self.decision_level - 1];
self.decision_level -= 1;
self.chronological_backtracking_level = self.decision_level;

self.backjump();

// add complement of the decision literal
self.decision_number += 1;
self.assignments[decision_literal.id] = Some(!decision_literal.sign);
self.assignments_log[decision_literal.id] = (
Some(!decision_literal.sign),
None,
self.decision_level,
self.decision_number,
);
}
} else if self.assignment_complete() {
co.yield_(SolveResult::Sat(self.assignments.clone())).await;

if self.decision_level == 0 {
return;
} else {
// get decision literal from this decision_level
let decision_literal = self.decisions[self.decision_level - 1];
// debug!("flip decision literal {:?}", decision_literal);
self.decision_level -= 1;
debug!("decision_level: {}", self.decision_level);
self.chronological_backtracking_level = self.decision_level;
debug!(
"chronological_backtracking_level: {}",
self.chronological_backtracking_level
);
self.backjump();

// add complement of the decision literal
self.decision_number += 1;
self.assignments[decision_literal.id] = Some(!decision_literal.sign);
self.assignments_log[decision_literal.id] = (
Some(!decision_literal.sign),
None,
self.decision_level,
self.decision_number,
);
}
} else {
self.decide()
}
}
})
.into_iter()
}

fn record_nogood(&mut self, nogood: Nogood) {
self.watch_lists.push(nogood_to_watch_list(&nogood));
self.nogoods.push(nogood);
let nogood_id = self.nogoods.len() - 1;
for variable_id in 0..self.number_of_variables {
if let Some(sign) = self.nogoods[nogood_id][variable_id] {
self.var_to_nogoods[variable_id].insert(nogood_id, sign);
self.nogoods_to_var.push(Map::default());
self.nogoods_to_var[nogood_id].insert(variable_id, sign);
}
}
}

/// Analyze conflict and learn UIP nogood
fn conflict_resolution(&self, nogood: &[Option<bool>]) -> (Nogood, Literal, usize) {
let mut nogood = nogood.to_owned();

let sigma = loop {
debug!("delta: {:?}", nogood);
let iter = nogood.iter().enumerate();

// Determine sigma the last literal in delta that has been added to the assignment
let mut sigma = Literal { id: 0, sign: true };
let mut nogood_index = None;
let mut decision_level_sigma = 0;
let mut biggest_decision_number = 0;
for (id, assignment) in iter {
if let Some(sign) = *assignment {
let (_, ng_index, decision_level, decision_number) = self.assignments_log[id];
if decision_number >= biggest_decision_number {
biggest_decision_number = decision_number;
sigma = Literal { id, sign };
nogood_index = ng_index;
decision_level_sigma = decision_level;
}
}
}
debug!("sigma: {:?}", sigma);

// A nogood is a unique implication point if there is no other literal
// from the same decision level as sigma
let mut iter = nogood.iter().enumerate();
let unique = loop {
match iter.next() {
Some((id, &Some(sign))) => {
let literal = Literal { id, sign };
if sigma != literal {
// debug!("literal: {:?}", literal);
let (_, _, decision_level, _) = self.assignments_log[literal.id];
if decision_level == decision_level_sigma {
break false;
}
}
}
Some((_, &None)) => {}
None => break true,
}
};
if unique {
break sigma;
}
// debug!("not unique");
if let Some(nogood_index) = nogood_index {
let reason = &self.nogoods[nogood_index];
debug!("reason: {:?}", reason);
let res = resolve(&nogood, &sigma, reason);
nogood = res;
} else {
// sigma is a decision_literals
// the reason is empty
let reason: Vec<Option<bool>> = vec![None; self.number_of_variables];
// debug!("reason: {:?}", reason);
let res = resolve(&nogood, &sigma, &reason);
nogood = res;
}
};
let mut k = 0;
for (id, assignment) in nogood.iter().enumerate() {
if let Some(sign) = *assignment {
let literal = Literal { id, sign };
if literal != sigma {
let (_, _, decision_level, _) = self.assignments_log[literal.id];
if decision_level > k {
k = decision_level
}
}
}
}
// debug!("k: {}", k);
// debug!("sigma: {:?}", sigma);
(nogood, sigma, k)
}

/// Increase decision level assign truth value to a previously unassigned variable
fn decide(&mut self) {
self.decision_level += 1;
self.decision_number += 1;
debug!("decision_level: {:?}", self.decision_level);
let decision_literal = self.choose();
debug!("decision_literal: {:?}", decision_literal);
self.assignments[decision_literal.id()] = Some(decision_literal.sign);
self.decisions.push(decision_literal);
self.assignments_log[decision_literal.id] = (
Some(decision_literal.sign),
None,
self.decision_level,
self.decision_number,
);
}

fn choose(&self) -> Literal {
for id in 0..self.number_of_variables {
if self.assignments[id] == Some(true) {
continue;
}
if self.assignments[id] == Some(false) {
continue;
}
return Literal { id, sign: true };
}
panic!("Logic error: calling choose on complete assignment-");
}

/// Return true if all variables have a truth value assignment
fn assignment_complete(&self) -> bool {
for id in 0..self.number_of_variables {
if self.assignments[id] == Some(true) {
continue;
}
if self.assignments[id] == Some(false) {
continue;
}
return false;
}
true
}
/// Return true if there is a conflict on decision level 0
fn is_top_level_conflict(&self, nogood: &[Option<bool>]) -> bool {
for (id, assignment) in nogood.iter().enumerate() {
if assignment.is_some() {
let (_, _, decision_level, _) = self.assignments_log[id];
if decision_level > 0 {
return false;
}
}
}
true
}
/// Backjump to decision level x and rewind assignment
fn backjump(&mut self) {
// debug!("backjump to decision_level {}", self.decision_level);
for (id, assignment) in self.assignments.iter_mut().enumerate() {
if let Some(sign) = *assignment {
let lit = Literal { id, sign };
let (_, _, decision_level, decision_number) = self.assignments_log[lit.id];

if decision_level > self.decision_level {
self.assignments_log[lit.id] = (None, None, 0, 0);
*assignment = None;
}
if decision_number > self.decision_number {
self.decision_number = decision_number - 1;
}
}
}

// backtrack decisions
while self.decisions.len() > self.decision_level {
self.decisions.pop();
}
}

/// Run unit propagation and unfounded set check
fn propagate(&mut self) -> PropagationResult {
trace!("propagate");
trace!("assignment: {:?}", self.assignments);
if let PropagationResult::Conflict(nogood) = self.unit_propagation() {
return PropagationResult::Conflict(nogood);
}
if !self.tight {
self.unfounded_loop_learning();
}
PropagationResult::Ok
}

/// Learn a nogood for an unfounded loop
fn unfounded_loop_learning(&mut self) {
todo!()
}

fn unit_propagation(&mut self) -> PropagationResult {
let mut propagation_queue: VecDeque<Literal> = VecDeque::new();
for (id, assignment) in self.assignments.iter().enumerate() {
if let Some(sign) = *assignment {
propagation_queue.push_back(Literal { id, sign });
}
}

loop {
if let Some(p) = propagation_queue.pop_front() {
debug!("prp: {:?}", p);

for (index, sign) in &self.var_to_nogoods[p.id] {
let watch_list = &mut self.watch_lists[*index];
// debug!(
// "wl.0: {} wl.1: {} nogood: {:?}",
// watch_list.first_watch, watch_list.second_watch, self.nogoods[*index]
// );
if watch_list.first_watch == p.id || watch_list.second_watch == p.id {
let dirty_watch = if watch_list.first_watch == p.id {
Watch::First
} else {
Watch::Second
};

if *sign == p.sign {
// propagated literal and nogood literal have the same sign
// try to update watch
if let Some(new_watch) = update_watches(
&self.nogoods_to_var[*index],
&self.assignments,
p,
watch_list.first_watch,
watch_list.second_watch,
) {
if dirty_watch == Watch::First {
watch_list.first_watch = new_watch;
} else {
watch_list.second_watch = new_watch;
}
continue;
} else {
// debug!("one watch could not be updated. it's a conflict or an implication.");
let other_watch = if dirty_watch == Watch::First {
&mut watch_list.second_watch
} else {
&mut watch_list.first_watch
};

// debug!("check the other watch");
let sign = self.nogoods_to_var[*index][other_watch];
match self.assignments[*other_watch] {
Some(x) => {
if sign == x {
// also the other watched literal is in the assignment. it's a conflict
return PropagationResult::Conflict(
self.nogoods[*index].clone(),
);
}
}
None => {
// the other watch is unassigned. we can imply the complement
let complement = !sign;
self.assignments[*other_watch] = Some(complement);
let lit = Literal {
id: *other_watch,
sign: complement,
};
debug!("infer: {:?}", lit);
self.decision_number += 1;
propagation_queue.push_back(lit);
self.assignments_log[*other_watch] = (
Some(complement),
Some(*index),
self.decision_level,
self.decision_number,
);

debug!(
"infer2: {:?} {:?}",
*other_watch,
(Some(complement), Some(*index), self.decision_level)
);
}
}
}
}
}
}
}
if propagation_queue.is_empty() {
return PropagationResult::Ok;
}
}
}
}

fn update_watches(
nogood_vars: &Map<usize, bool>,
assignments: &[Option<bool>],
p: Literal,
first_watch: usize,
second_watch: usize,
) -> Option<usize> {
for (id, sign) in nogood_vars {
if *id != p.id
&& *id != first_watch
&& *id != second_watch
&& assignments[*id] != Some(*sign)
{
return Some(*id);
}
}
None
}

fn resolve(nogood: &[Option<bool>], sigma: &Literal, reason: &[Option<bool>]) -> Nogood {
// assert sigma in nogood and reason
let mut res = vec![];
for (id, assignment) in nogood.iter().enumerate() {
match *assignment {
Some(sign) => {
let literal = Literal { id, sign };
if literal != *sigma {
res.push(Some(sign))
} else {
res.push(None)
}
}
None => res.push(None),
}
}
let neg_sigma = sigma.negate();
for (id, assignment) in reason.iter().enumerate() {
if let Some(sign) = *assignment {
let literal = Literal { id, sign };
if literal != neg_sigma {
res[id] = Some(sign);
}
}
}
res
}

fn nogood_to_watch_list(nogood: &[Option<bool>]) -> WatchList {
// TODO: special handling for nogoods of size 1
let mut first_watch = 0;
while nogood[first_watch].is_none() {
first_watch += 1;
}
let mut second_watch = nogood.len() - 1;
while nogood[second_watch].is_none() {
second_watch -= 1;
}
WatchList {
first_watch,
second_watch,
}
}
// only for tests
fn create_watch_lists(nogoods: &[Vec<Option<bool>>]) -> Vec<WatchList> {
let mut watch_lists = vec![];
for nogood in nogoods {
// TODO: special handling for nogoods of size 1
watch_lists.push(nogood_to_watch_list(nogood))
}
watch_lists
}
/// only for testing
fn mock_decide(solver: &mut Solver) {
solver.decision_level += 1;
solver.decision_number += 1;
solver.assignments[0] = Some(true);
solver.assignments_log[0] = (
Some(true),
None,
solver.decision_level,
solver.decision_number,
);
}

/// only for testing
fn mock_decide2(solver: &mut Solver) {
solver.decision_level += 1;
solver.decision_number += 1;
solver.assignments[2] = Some(true);
solver.assignments_log[2] = (
Some(true),
None,
solver.decision_level,
solver.decision_number,
);
}
#[test]
fn test_unit_propagation() {
let solver_nogoods = vec![vec![None, Some(true), Some(false)]];
let number_of_variables = 3;
let mut var_to_nogoods: Vec<Map<usize, bool>> = vec![Map::default(); number_of_variables];
let mut nogoods_to_var: Vec<Map<usize, bool>> = vec![Map::default(); solver_nogoods.len()];
for nogood_id in 0..solver_nogoods.len() {
for variable_id in 0..number_of_variables {
if let Some(sign) = solver_nogoods[nogood_id][variable_id] {
var_to_nogoods[variable_id].insert(nogood_id, sign);
nogoods_to_var[nogood_id].insert(variable_id, sign);
}
}
}

let mut solver = Solver {
tight: true,
number_of_variables,
assignments: vec![None, Some(true), None],
decisions: vec![Literal { id: 1, sign: true }],
watch_lists: vec![],
nogoods: solver_nogoods,
var_to_nogoods,
nogoods_to_var,
decision_level: 0,
decision_number: 0,
assignments_log: vec![(None, None, 0, 0); number_of_variables],
chronological_backtracking_level: 0,
};
solver.watch_lists = create_watch_lists(&solver.nogoods);
solver.unit_propagation();
let res = &solver.assignments;
assert_eq!(*res, vec![None, Some(true), Some(true)]);
}

#[test]
fn test_unit_propagation_conflict() {
use crate::convert::Builder;
let builder = Builder {
nogoods: vec![
vec![
Literal { id: 0, sign: true },
Literal { id: 1, sign: false },
],
vec![
Literal { id: 1, sign: true },
Literal { id: 2, sign: false },
],
vec![Literal { id: 1, sign: true }, Literal { id: 2, sign: true }],
],
};
let mut solver = builder.build();

mock_decide(&mut solver); // assign Literal(0)
let prop_result = solver.unit_propagation();
if let PropagationResult::Conflict(nogood) = prop_result {
assert_eq!(nogood, vec![None, Some(true), Some(true)]);
let top_level_conflict = solver.is_top_level_conflict(&nogood);
assert_eq!(top_level_conflict, false);
let (uip, sigma, k) = solver.conflict_resolution(&nogood);
assert_eq!(uip, vec![None, Some(true), None]);
assert_eq!(sigma, Literal { id: 1, sign: true });
if solver.chronological_backtracking_level > k {
solver.decision_level = solver.chronological_backtracking_level;
} else {
solver.decision_level = k;
}
println!("new_decision_level: {}", solver.decision_level);
solver.backjump();

// add complement of sigma
solver.decision_number += 1;
solver.assignments[sigma.id] = Some(!sigma.sign);
solver.assignments_log[sigma.id] = (Some(!sigma.sign), None, k, solver.decision_number);
solver.record_nogood(uip);
let res = solver.unit_propagation();
assert_eq!(res, PropagationResult::Ok);
assert_eq!(solver.assignments, vec![Some(false), Some(false), None]);

mock_decide2(&mut solver); // assign Literal(2)

let res = solver.unit_propagation();
assert_eq!(res, PropagationResult::Ok);
assert_eq!(
solver.assignments,
vec![Some(false), Some(false), Some(true)]
);

assert_eq!(solver.assignment_complete(), true);
}
}

#[test]
pub fn test_solve_1() {
use crate::convert::Builder;
let builder = Builder {
nogoods: vec![
vec![
Literal { id: 0, sign: true },
Literal { id: 1, sign: false },
],
vec![
Literal { id: 1, sign: true },
Literal { id: 2, sign: false },
],
vec![Literal { id: 1, sign: true }, Literal { id: 2, sign: true }],
],
};
let mut solver = builder.build();

let mut solutions = solver.solve();
let res = solutions.next();
assert_eq!(
res,
Some(SolveResult::Sat(vec![Some(false), Some(false), Some(true)]))
);
let res = solutions.next();
assert_eq!(
res,
Some(SolveResult::Sat(vec![
Some(false),
Some(false),
Some(false)
]))
);
let res = solutions.next();
assert_eq!(res, None);
}
#[test]
pub fn test_solve_unsat_1() {
use crate::convert::Builder;
let builder = Builder {
nogoods: vec![
vec![Literal { id: 0, sign: true }],
vec![Literal { id: 0, sign: false }],
],
};
let mut solver = builder.build();

let mut solutions = solver.solve();
let res = solutions.next();
assert_eq!(res, Some(SolveResult::UnSat));
let res = solutions.next();
assert_eq!(res, None);
}
#[test]
pub fn test_solve_unsat_2() {
use crate::convert::Builder;
let builder = Builder {
nogoods: vec![
vec![Literal { id: 1, sign: true }],
vec![Literal { id: 1, sign: false }],
],
};
let mut solver = builder.build();

let mut solutions = solver.solve();
let res = solutions.next();
assert_eq!(res, Some(SolveResult::UnSat));
let res = solutions.next();
assert_eq!(res, None);
}

pub fn create_test_solver() -> Solver {
use crate::convert::Builder;
let builder = Builder {
nogoods: vec![
vec![
Literal { id: 3, sign: false },
Literal { id: 2, sign: true },
],
vec![
Literal { id: 0, sign: false },
Literal { id: 5, sign: true },
],
vec![
Literal { id: 7, sign: false },
Literal { id: 4, sign: false },
Literal { id: 6, sign: true },
],
vec![
Literal { id: 3, sign: false },
Literal { id: 9, sign: true },
],
vec![
Literal { id: 0, sign: false },
Literal { id: 7, sign: false },
Literal { id: 10, sign: true },
],
vec![
Literal { id: 1, sign: false },
Literal { id: 12, sign: true },
],
vec![
Literal { id: 0, sign: true },
Literal { id: 5, sign: false },
Literal {
id: 11,
sign: false,
},
],
vec![
Literal { id: 7, sign: true },
Literal { id: 8, sign: false },
Literal { id: 8, sign: false },
],
vec![
Literal { id: 4, sign: true },
Literal { id: 5, sign: false },
],
vec![
Literal { id: 1, sign: true },
Literal {
id: 12,
sign: false,
},
],
vec![
Literal { id: 3, sign: true },
Literal { id: 2, sign: false },
Literal { id: 9, sign: false },
],
vec![Literal { id: 8, sign: true }, Literal { id: 7, sign: true }],
vec![
Literal { id: 8, sign: false },
Literal { id: 7, sign: false },
],
vec![
Literal { id: 9, sign: true },
Literal { id: 4, sign: false },
Literal { id: 7, sign: true },
],
vec![
Literal { id: 9, sign: true },
Literal { id: 4, sign: true },
Literal { id: 7, sign: false },
],
vec![
Literal { id: 9, sign: false },
Literal { id: 4, sign: true },
Literal { id: 7, sign: true },
],
vec![
Literal { id: 11, sign: true },
Literal { id: 0, sign: true },
],
vec![
Literal {
id: 11,
sign: false,
},
Literal { id: 0, sign: false },
],
vec![
Literal { id: 5, sign: true },
Literal { id: 3, sign: false },
Literal { id: 4, sign: false },
],
vec![
Literal { id: 5, sign: true },
Literal { id: 3, sign: true },
Literal { id: 4, sign: true },
],
vec![
Literal { id: 5, sign: false },
Literal { id: 3, sign: true },
Literal { id: 4, sign: false },
],
vec![
Literal { id: 10, sign: true },
Literal { id: 1, sign: true },
],
vec![
Literal {
id: 10,
sign: false,
},
Literal { id: 1, sign: false },
],
vec![
Literal { id: 12, sign: true },
Literal { id: 0, sign: true },
Literal { id: 7, sign: false },
],
vec![
Literal { id: 12, sign: true },
Literal { id: 0, sign: false },
Literal { id: 7, sign: true },
],
vec![
Literal {
id: 12,
sign: false,
},
Literal { id: 0, sign: false },
Literal { id: 7, sign: false },
],
vec![
Literal { id: 6, sign: true },
Literal { id: 3, sign: false },
],
vec![
Literal { id: 6, sign: false },
Literal { id: 3, sign: true },
],
vec![
Literal { id: 2, sign: true },
Literal { id: 0, sign: false },
Literal { id: 1, sign: false },
],
vec![
Literal { id: 2, sign: true },
Literal { id: 0, sign: true },
Literal { id: 1, sign: true },
],
vec![
Literal { id: 2, sign: false },
Literal { id: 0, sign: true },
Literal { id: 1, sign: false },
],
],
};
builder.build()
}
file addition: lib.rs (----------)

[0.35]

pub mod convert;
pub mod solver;

use thiserror::Error;

#[derive(Error, Debug)]
pub enum AspifError {
#[error("More than one solve item")]
MultipleSolveItems,
#[error("No solve item")]
NoSolveItem,
#[error("ParseError: {msg}")]
ParseError { msg: String },
}
file addition: convert.rs (----------)

[0.35]

use crate::solver::{Literal, Map, Solver, WatchList};
use aspif::AspifProgram;
use log::{debug, info};
use string_interner::symbol::SymbolU32;
use string_interner::StringInterner;

#[derive(Default)]
pub struct LiteralMapper {
aspif_literals: Map<u64, usize>,
pub bodies: Map<Vec<Literal>, usize>,
literal_count: usize,
supports: Map<usize, Vec<(Vec<Literal>, Vec<Literal>)>>,
}
impl LiteralMapper {
fn u64_to_solver_literal(&mut self, a: &u64) -> Literal {
if let Some((_key, value)) = self.aspif_literals.get_key_value(a) {
Literal::new(*value, true)
} else {
self.aspif_literals.insert(*a, self.literal_count);
let literal = Literal::new(self.literal_count, true);
self.literal_count += 1;
literal
}
}
fn i64_to_solver_literal(&mut self, a: &i64) -> Literal {
if *a >= 0 {
let b = *a as u64;
if let Some((_key, value)) = self.aspif_literals.get_key_value(&b) {
Literal::new(*value, true)
} else {
self.aspif_literals.insert(b, self.literal_count);
let literal = Literal::new(self.literal_count, true);
self.literal_count += 1;
literal
}
} else {
let b = -a as u64;
if let Some((_key, value)) = self.aspif_literals.get_key_value(&b) {
Literal::new(*value, false)
} else {
self.aspif_literals.insert(b, self.literal_count);
let literal = Literal::new(self.literal_count, false);
self.literal_count += 1;
literal
}
}
}
/// Returns corresponding solver literal if the body already exist in the LiteralMap
/// else creates a new entry and returns the literal
fn body2solver_literal(&mut self, body: &[Literal]) -> Literal {
if let Some((_key, value)) = self.bodies.get_key_value(body) {
Literal::new(*value, true)
} else {
self.bodies.insert(body.to_owned(), self.literal_count);
let literal = Literal::new(self.literal_count, true);
self.literal_count += 1;
literal
}
}
/// Returns corresponding solver literal if the body already exist in the LiteralMap
fn get_body_literal(&self, body: &[Literal]) -> Option<Literal> {
self.bodies
.get(body)
.map(|value| Literal::new(*value, true))
}

/// This function creates rule nogoods as in Definition 1 in *Advanced Conflict-Driven Disjunctive Answer Set Solving*
/// It also collects support body clauses for atom wise shifted rules as in *Advanced Conflict-Driven Disjunctive Answer Set Solving*
fn write_rule_nogood(&mut self, rule: &aspif::Rule, nogoods: &mut Vec<Vec<Literal>>) {
let body_clause = match &rule.body {
aspif::Body::NormalBody { elements } => {
// Create clause that makes the body true
let mut body_clause = vec![];
for e in elements {
body_clause.push(self.i64_to_solver_literal(e));
}
// TODO: is sort and dedup here necessary ?
body_clause.sort();
body_clause.dedup();
body_clause
}
aspif::Body::WeightBody {
lowerbound: _,
elements: _,
} => {
panic!("Unsupported Body")
}
};
match &rule.head {
aspif::Head::Disjunction { elements } => {
let ori_body_lit = self.body2solver_literal(&body_clause);
debug!("Body_lit:{:?} -> {:?}", ori_body_lit, body_clause);
// Create rule nogood
let mut rule_nogood = vec![];
for e in elements {
let head_lit = self.u64_to_solver_literal(e);
let neg_head_lit = head_lit.negate();
rule_nogood.push(neg_head_lit)
}
rule_nogood.push(ori_body_lit);

debug!("Rule nogood: {rule_nogood:?}");
nogoods.push(rule_nogood);

// Shift head atoms to the new body
for (idx, e) in elements.iter().enumerate() {
let new_head_lit = self.u64_to_solver_literal(e);
let mut body_extension = vec![];
for (idx2, e) in elements.iter().enumerate() {
if idx2 != idx {
let lit2 = self.u64_to_solver_literal(e);
let neg_lit = lit2.negate();
body_extension.push(neg_lit);
}
}
// debug!("Support for {new_head_lit:?}: {:?}{:?}",body_clause,body_extension);
self.supports
.entry(new_head_lit.id())
.and_modify(|e| e.push((body_clause.clone(), body_extension.clone())))
.or_insert(vec![(body_clause.clone(), body_extension)]);
}
}
aspif::Head::Choice { elements } => {
panic!("Unsupported Head : Choice")
}
};
}

/// This function creates support nogoods as in Definition 2 in *Advanced Conflict-Driven Disjunctive Answer Set Solving*
fn write_support_nogoods(&mut self, nogoods: &mut Vec<Vec<Literal>>) {
for (k, support) in &self.supports {
let mut support_nogood = vec![];
// Create support nogoods
support_nogood.push(Literal::new(*k, true));
for (old_body, extension) in support {
let mut new_body = old_body.clone();
new_body.extend_from_slice(extension);
if let Some(lit) = self.get_body_literal(&new_body) {
// new_body is known
let neg_lit = lit.negate();
support_nogood.push(neg_lit);
} else if let Some(lit) = self.get_body_literal(old_body) {
let neg_lit = lit.negate();
support_nogood.push(neg_lit);
for lit in extension {
let neg_lit = lit.negate();
support_nogood.push(neg_lit);
}
} else {
unreachable!()
}
}

debug!("Support nogood: {:?}", support_nogood);
nogoods.push(support_nogood);
}
}

/// This function creates conjunction nogoods as in Definition 3 in *Advanced Conflict-Driven Disjunctive Answer Set Solving*
fn write_conjuction_nogoods(&self, nogoods: &mut Vec<Vec<Literal>>) {
for (body, lit_id) in &self.bodies {
debug!("CNG lit:{} body{:?}", lit_id, body);
let mut conjunction_nogood1 = vec![];
let lit = Literal::new(*lit_id, true);
let neg_lit = Literal::new(*lit_id, false);
conjunction_nogood1.push(neg_lit);
for l in body.iter() {
conjunction_nogood1.push(*l);
let mut conjunction_nogoodn = vec![lit];
conjunction_nogoodn.push(l.negate());
debug!("Conjunction nogood: {:?}", conjunction_nogoodn);
nogoods.push(conjunction_nogoodn);
}

debug!("Conjunction nogood: {:?}", conjunction_nogood1);
nogoods.push(conjunction_nogood1);
}
}
}

#[test]
fn test_aspif_i64_to_solver_literal() {
let mut lm = LiteralMapper::default();
let l0 = Literal::new(0, true);
let l1 = Literal::new(1, false);
let l2 = Literal::new(0, false);
let l3 = Literal::new(1, true);
let sl0 = lm.i64_to_solver_literal(&12);
let sl1 = lm.i64_to_solver_literal(&-2);
let sl2 = lm.i64_to_solver_literal(&-12);
let sl3 = lm.i64_to_solver_literal(&-2);
let sl4 = lm.i64_to_solver_literal(&2);
assert_eq!(l0, sl0);
assert_eq!(l1, sl1);
assert_eq!(l2, sl2);
assert_eq!(l1, sl3);
assert_eq!(l3, sl4);
}
#[test]
fn test_aspif_u64_to_solver_literal() {
let mut lm = LiteralMapper::default();
let l0 = Literal::new(0, true);
let l1 = Literal::new(1, false);
let l2 = Literal::new(0, false);
let l3 = Literal::new(1, true);
let sl0 = lm.u64_to_solver_literal(&12);
let sl1 = lm.i64_to_solver_literal(&-2);
let sl2 = lm.i64_to_solver_literal(&-12);
let sl3 = lm.u64_to_solver_literal(&2);

assert_eq!(l0, sl0);
assert_eq!(l1, sl1);
assert_eq!(l2, sl2);
assert_eq!(l3, sl3);
}
#[test]
fn test_body_to_solver_literal() {
// TODO
// let mut lm = LiteralMapper::default();
// let la = Literal::new(0, true);
// let lb = Literal::new(1, false);
// let lc = Literal::new(0, false);
// let ld = Literal::new(1, true);
// let sl0 = lm.body2solver_literal(&[la,lb]);
// let sl1 = lm.body2solver_literal(&[lb,lc]);
// let sl2 = lm.body2solver_literal(&[lc,ld]);
// let sl3 = lm.body2solver_literal(&[lb,ld]);

// let l0 = Literal::new(2, true);
// let l1 = Literal::new(3, true);
// let l2 = Literal::new(4, true);
// let l3 = Literal::new(5, true);

// assert_eq!(l0, sl0);
// assert_eq!(l1, sl1);
// assert_eq!(l2, sl2);
// assert_eq!(l3, sl3);
}

pub type SymbolMapper = Map<Vec<Literal>, SymbolU32>;

fn insert_into_symbol_mapper(
symbol_mapper: &mut SymbolMapper,
literal_mapper: &mut LiteralMapper,
symbol: SymbolU32,
condition: &[i64],
) {
let mut new_condition = vec![];
for e in condition {
new_condition.push(literal_mapper.i64_to_solver_literal(e));
}
// TODO: This is buggy if there could be multiple symbols with the same condition
// q :- not p.
// p :- not q.
// #show t:p.
symbol_mapper.insert(new_condition, symbol);
}

use petgraph::algo::tarjan_scc;
use petgraph::graph::{DiGraph, NodeIndex};

/// Create a (directed) positive atom dependency graph
/// The graph will be used to compute scc's which correspond to loops of the program
pub fn graph_from_aspif(aspif_program: &AspifProgram) {
let mut literal_mapper = LiteralMapper::default();
let mut positive_atom_dependency_graph: DiGraph<u32, ()> = DiGraph::default();

for statement in &aspif_program.statements {
debug!("stmt:{:?}", statement);
match statement {
aspif::Statement::Rule(rule) => {
let body_clause = match &rule.body {
aspif::Body::NormalBody { elements } => {
let mut body_clause = vec![];
for e in elements {
body_clause.push(literal_mapper.i64_to_solver_literal(e));
}
body_clause.sort();
body_clause
}
aspif::Body::WeightBody {
lowerbound: _,
elements: _,
} => {
panic!("Unsupported Body")
}
};
match &rule.head {
aspif::Head::Disjunction { elements } => {
for body_lit in &body_clause {
if body_lit.sign() {
for head_atom_id in elements {
while positive_atom_dependency_graph.node_count()
<= *head_atom_id as usize
{
let _a = positive_atom_dependency_graph.add_node(0);
}
let a = NodeIndex::from(*head_atom_id as u32);
while positive_atom_dependency_graph.node_count()
<= body_lit.id()
{
let _a = positive_atom_dependency_graph.add_node(0);
}
let b = NodeIndex::from(body_lit.id() as u32);
positive_atom_dependency_graph.add_edge(a, b, ());
}
}
}
}
aspif::Head::Choice { elements } => {
panic!("Unsupported Head : Choice")
}
}
}
// aspif::Statement::Minimize(_) => todo!(),
// aspif::Statement::Projection(_) => todo!(),
aspif::Statement::Output(_) => {}
// aspif::Statement::External { atom, init } => todo!(),
// aspif::Statement::Assumption(_) => todo!(),
// aspif::Statement::Heuristic {
// modifier,
// atom,
// k,
// priority,
// condition,
// } => todo!(),
// aspif::Statement::Edge { u, v, condition } => todo!(),
// aspif::Statement::NumericTheoryTerm { id, w } => todo!(),
// aspif::Statement::SymbolicTheoryTerm { id, string } => todo!(),
// aspif::Statement::CompoundTheoryTerm { id, t, terms } => todo!(),
// aspif::Statement::TheoryAtomElements {
// id,
// theory_terms,
// literals,
// } => todo!(),
// aspif::Statement::TheoryAtom {
// atom,
// symbolic_term,
// theory_atom_elements,
// theory_operation,
// } => todo!(),
// aspif::Statement::TheoryDirective {
// symbolic_term,
// theory_atom_elements,
// theory_operation,
// } => todo!(),
// aspif::Statement::Comment => todo!(),
_ => {
panic!("Unsupported Statement");
}
}
}

debug!("positive_atom_dependency_graph: {positive_atom_dependency_graph:?}");
info!("Strongly connected components ...");
let components = tarjan_scc(&positive_atom_dependency_graph);

for scc in components {
debug!("{scc:?}");
}
}

pub struct Builder {
pub(crate) nogoods: Vec<Vec<Literal>>,
}
impl Builder {
pub fn from_aspif(aspif_program: &AspifProgram) -> (Self, SymbolMapper, StringInterner) {
let mut interner = StringInterner::default();
let mut literal_mapper = LiteralMapper::default();
let mut symbol_mapper = SymbolMapper::default();

let mut nogoods = vec![];

for statement in &aspif_program.statements {
match statement {
aspif::Statement::Rule(rule) => {
literal_mapper.write_rule_nogood(rule, &mut nogoods);
}
// aspif::Statement::Minimize(_) => todo!(),
// aspif::Statement::Projection(_) => todo!(),
aspif::Statement::Output(output) => {
let sym = interner.get_or_intern(&output.string);
insert_into_symbol_mapper(
&mut symbol_mapper,
&mut literal_mapper,
sym,
&output.condition,
)
}
// aspif::Statement::External { atom, init } => todo!(),
// aspif::Statement::Assumption(_) => todo!(),
// aspif::Statement::Heuristic {
// modifier,
// atom,
// k,
// priority,
// condition,
// } => todo!(),
// aspif::Statement::Edge { u, v, condition } => todo!(),
// aspif::Statement::NumericTheoryTerm { id, w } => todo!(),
// aspif::Statement::SymbolicTheoryTerm { id, string } => todo!(),
// aspif::Statement::CompoundTheoryTerm { id, t, terms } => todo!(),
// aspif::Statement::TheoryAtomElements {
// id,
// theory_terms,
// literals,
// } => todo!(),
// aspif::Statement::TheoryAtom {
// atom,
// symbolic_term,
// theory_atom_elements,
// theory_operation,
// } => todo!(),
// aspif::Statement::TheoryDirective {
// symbolic_term,
// theory_atom_elements,
// theory_operation,
// } => todo!(),
// aspif::Statement::Comment => todo!(),
_ => {
panic!("Unsupported Statement");
}
}
}
literal_mapper.write_support_nogoods(&mut nogoods);
literal_mapper.write_conjuction_nogoods(&mut nogoods);

(Builder { nogoods }, symbol_mapper, interner)
}
pub fn build(self) -> Solver {
let mut number_of_variables = 0;
for nogood in &self.nogoods {
for lit in nogood {
if lit.id() + 1 > number_of_variables {
number_of_variables = lit.id() + 1;
}
}
}
let mut solver_nogoods = vec![];
for nogood in self.nogoods {
let mut solver_nogood = vec![None; number_of_variables];
for (id, item) in solver_nogood.iter_mut().enumerate() {
if nogood.contains(&Literal::new(id, true)) {
*item = Some(true);
} else if nogood.contains(&Literal::new(id, false)) {
*item = Some(false);
}
}
debug!("Solver nogood: {:?}", solver_nogood);
solver_nogoods.push(solver_nogood);
}

let mut watch_lists = vec![];
for nogood in &solver_nogoods {
// TODO: special handling for nogoods of size 1
let mut left_watch = 0;
while nogood[left_watch].is_none() {
left_watch += 1;
}
let mut right_watch = nogood.len() - 1;
while nogood[right_watch].is_none() {
right_watch -= 1;
}
watch_lists.push(WatchList {
first_watch: left_watch,
second_watch: right_watch,
})
}

let mut var_to_nogoods: Vec<Map<usize, bool>> = vec![Map::default(); number_of_variables];
let mut nogoods_to_var: Vec<Map<usize, bool>> = vec![Map::default(); solver_nogoods.len()];
for nogood_id in 0..solver_nogoods.len() {
for (variable_id, map) in var_to_nogoods
.iter_mut()
.enumerate()
.take(number_of_variables)
{
if let Some(sign) = solver_nogoods[nogood_id][variable_id] {
map.insert(nogood_id, sign);
nogoods_to_var[nogood_id].insert(variable_id, sign);
}
}
}

Solver {
tight: true,
number_of_variables,
assignments: vec![None; number_of_variables],
decisions: vec![],
watch_lists,
nogoods: solver_nogoods,
var_to_nogoods,
nogoods_to_var,
decision_level: 0,
decision_number: 0,
assignments_log: vec![(None, None, 0, 0); number_of_variables],
chronological_backtracking_level: 0,
}
}
}

#[test]
fn test_write_rule_nogood() {
let mut lm = LiteralMapper::default();
let l0 = Literal::new(0, true);
let l1 = Literal::new(1, false);
let l2 = Literal::new(2, true);
let l3 = Literal::new(3, false);

let mut nogoods = vec![];
// Rule with empty body and empty head `:-.` the corresponding rule nogood should contain only the literal corresponding to the empty body
if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 0 0 0").unwrap() {
lm.write_rule_nogood(&rule, &mut nogoods);
assert_eq!(nogoods[0], vec![l0])
}
// Rule with one head and empty body `a.`
if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 1 1 0 0").unwrap() {
lm.write_rule_nogood(&rule, &mut nogoods);
assert_eq!(nogoods[1], vec![l1, l0])
}

// :- not a.
if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 0 0 1 -1").unwrap() {
lm.write_rule_nogood(&rule, &mut nogoods);
assert_eq!(nogoods[2], vec![l2])
}

// a :- not a.
if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 1 1 0 1 -1").unwrap() {
lm.write_rule_nogood(&rule, &mut nogoods);
assert_eq!(nogoods[3], vec![l1, l2])
}

// b :- not a.
if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 1 2 0 1 -1").unwrap() {
lm.write_rule_nogood(&rule, &mut nogoods);
assert_eq!(nogoods[4], vec![l3, l2])
}
// a;b :- not a.
if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 2 1 2 0 1 -1").unwrap() {
lm.write_rule_nogood(&rule, &mut nogoods);
assert_eq!(nogoods[5], vec![l1, l3, l2])
}
}

#[test]
fn test_write_nogoods() {
let mut lm = LiteralMapper::default();

let na = Literal::new(0, false);
let ne = Literal::new(1, false);
let b1 = Literal::new(2, true);
let nb = Literal::new(3, false);
let mut nogoods = vec![];
// b :- a, not e.
if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 1 4 0 2 1 -3").unwrap() {
lm.write_rule_nogood(&rule, &mut nogoods);
assert_eq!(nogoods[0], vec![nb, b1])
}
let nd = Literal::new(4, false);
let b2 = Literal::new(5, true);
// a :- b, not d.
if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 1 1 0 2 4 -5").unwrap() {
lm.write_rule_nogood(&rule, &mut nogoods);
assert_eq!(nogoods[1], vec![na, b2])
}
let b3 = Literal::new(6, true);
let nc = Literal::new(7, false);
// c;d :- b.
if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 2 2 5 0 1 4").unwrap() {
lm.write_rule_nogood(&rule, &mut nogoods);
assert_eq!(nogoods[2], vec![nc, nd, b3])
}
let b4 = Literal::new(8, true);
// b :- d, c.
if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 1 4 0 2 5 2").unwrap() {
lm.write_rule_nogood(&rule, &mut nogoods);
assert_eq!(nogoods[3], vec![nb, b4])
}
let b5 = Literal::new(9, true);
// a;c :- not e.
if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 2 1 2 0 1 -3").unwrap() {
lm.write_rule_nogood(&rule, &mut nogoods);
assert_eq!(nogoods[4], vec![na, nc, b5])
}
let b6 = Literal::new(10, true);
// e :- not a, not c.
if let aspif::Statement::Rule(rule) = aspif::read_statement_line("1 0 1 3 0 2 -1 -2").unwrap() {
lm.write_rule_nogood(&rule, &mut nogoods);
assert_eq!(nogoods[5], vec![ne, b6])
}
}
#[test]
fn test_collect_atom_support() {
//TODO
}
// pub struct GroundDisjunctiveRule {
// head: Vec<u32>,
// body: Body,
// }
// impl GroundDisjunctiveRule {
// fn new(head: &[u32], pbody: &[u32], nbody: &[u32]) -> Self {
// let mut head_atoms = Vec::from(head);
// head_atoms.dedup();
// let body = Body::new(pbody, nbody);
// GroundDisjunctiveRule {
// head: head_atoms,
// body,
// }
// }
// }
// #[derive(PartialEq, Clone, Debug)]
// pub enum Body {
// // Body contains a Contradiction and can never be satisfied
// Contradiction,
// Conditions {
// positive_body: Vec<u32>,
// negative_body: Vec<u32>,
// },
// }
// impl Body {
// fn new(pbody: &[u32], nbody: &[u32]) -> Self {
// let mut positive_body = Vec::from(pbody);
// positive_body.dedup();
// let mut negative_body = Vec::from(nbody);
// negative_body.dedup();
// for a1 in &negative_body {
// for a2 in &positive_body {
// if a1 == a2 {
// return Body::Contradiction;
// }
// }
// }
// Body::Conditions {
// positive_body,
// negative_body,
// }
// }
// }
// type SolversAtoms = u32;
// fn atoms(program: &[GroundDisjunctiveRule]) -> Vec<SolversAtoms> {
// Vec::default()
// }
// fn bodies(program: &[GroundDisjunctiveRule]) -> Vec<SolversAtoms> {
// Vec::default()
// }
file addition: examples (d--r------)

[0.18]
file addition: versuch.rs (----------)

[0.56825]

use anyhow::Result;
use clap::Parser;
use log::{debug, error, info, warn};
use solver::convert::Builder;
use solver::solver::create_test_solver;
use std::fs;
use std::io;
use std::path::PathBuf;

/// Solver
#[derive(Parser, Debug)]
#[clap(name = "solver")]
#[clap(version, author)]
struct Opt {
/// Input file in aspif format
#[clap(name = "FILE", parse(from_os_str))]
file: Option<PathBuf>,
/// Verbose mode (-v, -vv, -vvv, etc)
#[clap(short = 'v', long = "verbose", parse(from_occurrences))]
verbose: usize,
}

pub enum Reader<'a> {
File(io::BufReader<fs::File>),
Stdin(io::StdinLock<'a>),
}
impl<'a> io::Read for Reader<'a> {
fn read(&mut self, buf: &mut [u8]) -> io::Result<usize> {
match self {
Self::File(reader) => reader.read(buf),
Self::Stdin(guard) => guard.read(buf),
}
}
}
impl<'a> io::BufRead for Reader<'a> {
fn fill_buf(&mut self) -> io::Result<&[u8]> {
match self {
Self::File(reader) => reader.fill_buf(),
Self::Stdin(guard) => guard.fill_buf(),
}
}
fn consume(&mut self, amt: usize) {
match self {
Self::File(reader) => reader.consume(amt),
Self::Stdin(guard) => guard.consume(amt),
}
}
}
fn main() {
let opt = Opt::parse();

stderrlog::new()
.module(module_path!())
.verbosity(opt.verbose * 4)
.module("solver")
.module("solver::convert")
.init()
.unwrap();
if let Err(err) = run(opt) {
error!("{:?}", err);
std::process::exit(1);
}
}
fn run(opt: Opt) -> Result<()> {
let stdin = io::stdin();
let input = match opt.file {
Some(path) => {
let file = fs::File::open(path)?;
Reader::File(io::BufReader::new(file))
}
None => {
let guard = stdin.lock();
Reader::Stdin(guard)
}
};

// let mut out = std::io::stdout();

info!("Reading input ...");
let parse_result = match input {
Reader::File(buf_reader) => aspif::read_aspif(buf_reader)?,
Reader::Stdin(buf_reader) => aspif::read_aspif(buf_reader)?,
};

info!("Translate to nogoods (wip) ...");
let (builder, symbol_mapper, interner) = match parse_result {
aspif::ParseResult::Complete(aspif_program) => {
info!("Create a (directed) positive atom dependecy graph (wip)...");
let res = solver::convert::graph_from_aspif(&aspif_program);
info!("Create a builder (wip) ...");
Builder::from_aspif(&aspif_program)
}
aspif::ParseResult::Incomplete(_) => {
warn!("Could not read complete aspif program.");
panic!("Could not read complete aspif program.");
}
};

info!("Build solver ...");
let mut solver = builder.build();
for (condition, symbol) in &symbol_mapper {
println!("condition:{:?} symbol:{} ",condition, interner.resolve(*symbol).unwrap());
}
// let mut solver = create_test_solver();
info!("Solve ...");
use solver::solver::SolveResult;
let mut solutions = solver.solve().enumerate();

loop {
if let Some((c, res)) = solutions.next() {
match res {
SolveResult::Sat(assignments) => {
print!("Solution {}: ", c + 1);
for (condition, symbol) in &symbol_mapper {
let mut satisfied = true;
for literal in condition {
match assignments[literal.id()] {
Some(sign) => satisfied = sign == literal.sign(),
None => panic!("Partial assignment!"),
}
if !satisfied {
break;
};
}
if satisfied {
print!("{} ", interner.resolve(*symbol).unwrap());
}
// debug!("condition: {:?} sym: {}",condition,interner.resolve(*symbol).unwrap());
}
let mut string = String::new();
for (id, e) in assignments.iter().enumerate() {
match e {
Some(true) => string = format!("{} {}", string, id),
Some(false) => string = format!("{} ~{}", string, id),
None => {}
}
}
debug!("solution: {string}");
println!();
}
SolveResult::UnSat => {
println!("UNSAT");
}
}
} else {
println!("EXHAUSTED");
break;
}
}
Ok(())
}
file addition: Cargo.toml (----------)

[0.18]

[package]
name = "solver"
version = "0.1.0"
authors = ["robauke"]
description = "A CDNL solver."
edition = "2021"
# documentation = "https://docs.rs/versuch"

[dependencies]
rustc-hash = "1.1.0"
genawaiter = { version = "0.99" }
string-interner = "0.14"
fnv = "1.0" # deterministic HashMap
petgraph = "0.6"
aspif = { git = "https://github.com/sthiele/aspif-parser", branch = "st/wip" }
# aspif = {path = "../../aspif-parser"}

clap = { version = "3.0", features = ["derive"] }
anyhow = "1.0"
log = "0.4"
thiserror = "1.0"
stderrlog = "0.5"
file addition: README.md (----------)

[2.1]

# Versuch

Produce aspif output with clingo:

```sh
clingo test.lp --pre=aspif > test.aspif
```

Run versuch:

```sh
cargo run --example versuch test.aspif -v
```
file addition: Cargo.toml (----------)

[2.1]

[workspace]
members = [
"solver",
]