Browse Source

removed broken (for the time being) SAT solver

clause_generator
Thomas Johnson 3 years ago
parent
commit
52855a4129
  1. 5
      src/main.rs
  2. 425
      src/sat.rs

5
src/main.rs

@ -1,14 +1,9 @@
// vim: ts=4 sw=4 et
//#![feature(trace_macros)]
//#![feature(log_syntax)]
#[macro_use]
/// TODO: document this
pub mod clause;
/// I made this before I knew I didn't need it. :/
pub mod hash_wrapper;
/// The documentation of this one is mostly for the developer, but does describe the API.
pub mod sat;
fn main() {}

425
src/sat.rs

@ -1,425 +0,0 @@
// vim: ts=4 sw=4 et
use crate::clause::*;
use std::collections::hash_map::HashMap;
use std::collections::BTreeSet;
/// A structure representing a decision to assign a variable made by the solver, containing at
/// least the variable which was changed, the value it's currently set to, and the number of
/// clauses which were deactivated by the decision.
enum Decision {
/// Indicates that the solver ran out of implications, so it's guessing.
// variable whose value was decided, value of the variable
Arbitrary(Variable, bool, usize),
/// Indicates that previous decisions have left unit clauses, implying certain variables are
/// true. The vector is part of the implication graph -- it contains the indices of the
/// decisions that led to this one, for clause learning and non-chronological backtracking.
// variable whose value was decided, value of the variable, indicies of decisions that caused
// this one
ForcedByUnit(Variable, bool, usize, Vec<usize>),
/// Indicates that the solver already tried the other value of this variable without changing
/// anything else.
// variable whose value was decided, value of the variable
ForcedByExhaustion(Variable, bool, usize),
}
impl Decision {
/// Gets the variable that the decision was made with.
fn var(&self) -> &Variable {
use Decision::*;
match self {
Arbitrary(var, _, _) => &var,
ForcedByUnit(var, _, _, _) => &var,
ForcedByExhaustion(var, _, _) => &var,
}
}
/// Gets the value that the variable is assigned to.
fn val(&self) -> bool {
use Decision::*;
match self {
Arbitrary(_, b, _) => *b,
ForcedByUnit(_, b, _, _) => *b,
ForcedByExhaustion(_, b, _) => *b,
}
}
/// Sets the field indicating the number of clauses moved.
fn set_clauses_moved(&mut self, n: usize) {
use Decision::*;
match self {
Arbitrary(_, _, k) => *k = n,
ForcedByUnit(_, _, k, _) => *k = n,
ForcedByExhaustion(_, _, k) => *k = n,
}
}
/// Gets the field indicating the number of clauses moved.
fn get_clauses_moved(&self) -> usize {
use Decision::*;
match self {
Arbitrary(_, _, k) => *k,
ForcedByUnit(_, _, k, _) => *k,
ForcedByExhaustion(_, _, k) => *k,
}
}
}
/// A structure describing the state of a conflict-driven clause learning solver.
///
/// All operations done by the solver are done on an instance of this struct.
pub struct CDCLState {
/// A list of clauses whose values cannot be known without knowing the values of variables that
/// have not been assigned by the solver yet, as well as how many unassigned variables are in
/// each clause.
///
/// Each clause itself has its literals partitioned in to two parts, with the boundary at the
/// number of unassigned variables that is stored with each clause.
clauses: Vec<(Clause, usize)>,
/// A list of clauses which are known to be true, because one of their literals is true.
///
/// Thanks to the fact that the decisions are a stack, we are guaranteed that as long as
/// whenever we move clauses to the end of the inactive list, when a decision is being unmade
/// and clauses are being moved to the active list, the clauses that are being moved are at the
/// end of the inactive list.
inactive_clauses: Vec<(Clause, usize)>,
/// A stack of decisions made by the solver, in chronological order. Whenever this stack is
/// pushed, a number of clauses must be moved from the active list to the inactive list. When it
/// is popped, they must be moved back.
///
/// This must be treated as a stack, since each clause is associated with a list of variable
/// which were defined at the time; therefore, undeciding something which was not the last
/// decision may move clauses to the active list which are ignoring variables because they were
/// undefined at the time the clause was deactiviated. Rectifying this situation is more
/// trouble than it's worth.
decisions: Vec<Decision>,
/// This is a table which goes from a variable to the index of the decision that assigned it.
dec_table: HashMap<Variable, usize>,
/// This is set to `true` once the search space has been exhausted.
finished: bool,
}
impl CDCLState {
/// Moves a clause at a given index to the end of the inactive list.
fn deactivate_clause(&mut self, idx: usize) -> bool {
let last = self.clauses.len() - 1;
self.clauses.swap(idx, last);
match self.clauses.pop() {
Some(clause) => {
self.inactive_clauses.push(clause);
true
}
None => false,
}
}
/// Moves the last clause of the inactive list to the active list.
fn activate_clause(&mut self) -> bool {
match self.inactive_clauses.pop() {
Some(clause) => {
self.clauses.push(clause);
true
}
None => false,
}
}
/// Sets the number of clauses deactivated in the last decision.
///
/// # Panics
///
/// Will panic if there are no decisions.
fn set_n_clauses_moved(&mut self, n: usize) {
self.decisions.last_mut().unwrap().set_clauses_moved(n);
}
/// Examines the last decision on the stack, and adjusts the __clause list__, __first inactive
/// index__, __variable assignment__, and __decision table__ accordingly.
///
/// # Return Value
///
/// Iff the decision leads to an empty clause, return false. (Changes will still be made; they
/// must be undone with `reverse_last_decision` as usual.)
///
/// # Panics
///
/// If the decision stack is empty, this function will panic.
fn enact_last_decision(&mut self) -> bool {
let decision = self.decisions.last_mut().unwrap();
decision.var().assign(decision.val());
self.dec_table
.insert(decision.var().clone(), self.decisions.len() - 1);
let mut clauses_moved = 0;
for i in 0..self.clauses.len() {
let (clause, part) = &mut self.clauses[i];
let mut j = 0;
while j < *part {
// `part` changes in the loop, so it can't be a range loop.
let v = clause[j].get_assignment();
match v {
None => {
j += 1;
}
Some(true) => {
clauses_moved += 1;
self.deactivate_clause(i);
break;
}
Some(false) => {
clause.swap(j, *part);
*part -= 1;
if *part == 0 {
self.set_n_clauses_moved(clauses_moved);
return false;
}
}
}
}
}
self.set_n_clauses_moved(clauses_moved);
true
}
/// Does essentially the reverse of `enact_last_decision`. Panics under the same conditions.
fn reverse_last_decision(&mut self) {
let decision = self.decisions.last().unwrap();
let dv = decision.var().clone();
dv.unassign();
self.dec_table.remove(&decision.var());
for _i in 0..decision.get_clauses_moved() {
self.activate_clause();
}
for (clause, part) in self.clauses.iter_mut() {
while &clause[*part].get_variable() == &dv {
*part += 1;
}
}
}
/// This takes a decision on the decision stack and calls `enact_last_decision`, and backtracks
/// and tries again if there's a conflict.
fn enact_and_backtrack(&mut self) -> bool {
// Now we need to enact the decision, and handle a conflict if it happens.
// TODO: This section could seriously stand to be optimized.
while !self.enact_last_decision() {
// The condition above means that the last operation led to a conflict. Here we do the
// clause learning and non-chronological backtracking.
//
// First we make sure the last iteration is complete. This is done by the condititon on
// this loop.
let mut causes = BTreeSet::new();
// Here we recursively get all the decisions we made that we weren't logically forced
// into making. (Exhaustion is not a logically forced choice; it's the result of
// finding a solution, not a contradiction.)
self.get_causes(self.decisions.len(), &mut causes);
// We keep track of the most recently chosen variable that helped cause the
// contradiction, which is the last step of non-chronological backtracking.
//
// Here's the subtlety about exhaustion. As mentioned above, exahustion is not a
// logically forced choice, and thus it gets added to set of causes. However, we *do
// not* want to backtrack to a decision forced by exhaustion, because then we'll be
// searching the same space twice. (In fact, if it weren't for the learned clause, it
// would cause a loop if we did this and were not very careful about it!)
//
// TODO: When the feature gets stabilized, use `last()` on `BTreeSet`.
let backtrack_point = {
let mut btpo = None;
for causeidx in causes.iter().rev().map(|x| *x) {
if let Decision::Arbitrary(..) = self.decisions[causeidx] {
btpo = Some(causeidx);
}
}
match btpo {
Some(n) => n,
None => {
// Nothing caused this choice; that means it was a unit clause at the
// start, and the fact that it's now a contradiction means that we've
// exhausted all the possibilities. We're done.
self.finished = true;
return false;
}
}
};
let forced_var = self.decisions[backtrack_point].var().clone();
let forced_val = !self.decisions[backtrack_point].val();
// We construct a new clause that says that at least one of the things that caused this
// conflict need to be set otherwise.
let mut newclause = Clause::new();
for idx in causes.iter().rev() {
let var = self.decisions[*idx].var();
newclause.push(var.get_literal(self.decisions[*idx].val()));
}
// Here we do the backtracking. (I saved it for now so that the backtrack point was
// still on the stack to simplify the above code.)
//
// Note that the variables are in the order you would expect if the clause had been in
// the list all along -- in particular, if each variable had been moved to the other
// side of the parition in the order that its value was chosen.
while self.decisions.len() < backtrack_point {
self.reverse_last_decision();
self.decisions.pop();
}
// Now we push the clause, with only the most recently forced variable on the active
// side of the partition. We know that calling `enact_last_decision` will deactivate
// this clause immediately due to the decision pushed below.
self.inactive_clauses.push((newclause, 1));
// And finally, we push the decision as it it had been made by the new unit clause. The
// effect is that the state of the solver is as if we had just made a decision on our
// new clause.
self.decisions.push(Decision::ForcedByUnit(
forced_var,
forced_val,
0,
causes.into_iter().collect(),
));
// And then, of course, we have to enact the decision, which is done by the condition
// in the loop's next iteration.
}
true
}
// This one could use a bit of cleanup -- it's a naïve way to do it.
/// Finds the index of a unit clause, if one exists. TODO: Make this better. It's currently a
/// linear search that gets started from the beginning every time it's needed.
fn find_unit_clause(&self) -> Option<usize> {
for (i, (_, part)) in self.clauses.iter().enumerate() {
if *part == 1 {
return Some(i);
}
}
None
}
/// Given the index of a decision, recursively find all decisions that weren't forced by a unit
/// clause that led to the decision being made.
fn get_causes(&self, idx: usize, causes: &mut BTreeSet<usize>) {
use Decision::*;
match &self.decisions[idx] {
Arbitrary(_, _, _) | ForcedByExhaustion(_, _, _) => {
causes.insert(idx);
}
ForcedByUnit(_, _, _, cause_list) => {
for cause in cause_list {
self.get_causes(*cause, causes);
}
}
}
}
/// When we are forced to make a choice to continue, this function is what picks a variable to
/// assign and what to assign to it. TODO: Pick a non-naïve algorithm.
fn pick_variable(&self) -> Option<(Variable, bool)> {
if !self.clauses.is_empty() {
let lit = &self.clauses[0].0[0];
Some((lit.get_variable().clone(), !lit.is_neg()))
} else {
None
}
}
/// This 'advances' the state of the solver in the following sense: If there's a forced choice
/// of variable, choose it. If not, and there's an arbitrary choice of variable, choose it. If
/// not, backtrack to the last arbitrary choice, and try the other alternative. After making
/// the choice (whichever it was), check for conflicts and backtrack if one was found. Keep
/// backtracking until there isn't a conflict. If that doesn't happen (conflicts all the way
/// up), then we're out of search space, so return false. Otherwise, return true.
fn advance(&mut self) -> bool {
match self.find_unit_clause() {
Some(idx) => {
// There's a unit clause that's going to forcing us to assign a variable.
let (clause, _) = &self.clauses[idx];
// Keep track of all the causes for clause learning and non-chronological
// backtracking if we need it.
let mut causes = Vec::new();
for i in 1..clause.len() {
causes.push(*self.dec_table.get(&clause[i].get_variable()).unwrap());
}
// Push the decision.
self.decisions.push(Decision::ForcedByUnit(
clause[0].get_variable().clone(),
!clause[0].is_neg(),
0,
causes,
));
// We enact this decision and handle conflicts (backtrack) if the need arises.
self.enact_and_backtrack()
// And we have made progress, either downward or sideways.
}
None => {
// We're being forced to assign a value to an arbitrary variable.
let picked = self.pick_variable();
// But there might not be an arbitrary variable to assign to, in which case we've
// exhausted the latest choice.
match picked {
Some((var, val)) => {
// We have made an arbitrary decision about which variable to assign. Now
// we just push it on to the decision stack and enact the decision.
self.decisions.push(Decision::Arbitrary(var, val, 0));
self.enact_and_backtrack()
}
None => {
// There isn't an unassigned literal to choose. We've found a solution, and
// now we're looking for another.
let (var, val) = {
// First, let's look for an arbitrary decision that was made
// previously. (Note that another exhaustion-forced decision is not
// acceptable.) While we're doing so, let's unwind the decision stack.
let mut maybe_var_val = None;
for _didx in (0..self.decisions.len()).rev() {
self.reverse_last_decision();
let last = self.decisions.pop().unwrap();
match last {
Decision::Arbitrary(var, val, _) => {
maybe_var_val = Some((var, val));
break;
}
_ => (),
}
}
// Then, we take note of the variable we're backtracking on, and the
// negation of its value.
if let Some((var, val)) = maybe_var_val {
(var, !val)
} else {
self.finished = true;
return false;
}
};
// We push the backtrack onto the decision stack, and then enact. Business
// as usual.
self.decisions
.push(Decision::ForcedByExhaustion(var, val, 0));
self.enact_and_backtrack()
}
}
}
}
}
/// This proceeds until the solver finds a solution, or runs out of search space. It returns a
/// `Some` if a solution was found, and a `None` otherwise. The variables will be set to the
/// values required for the solution.
///
/// ___Do not tamper with the variable assignments before or between invocations of this
/// function.___
pub fn get_next_solution(&mut self) -> Option<()> {
if self.finished {
return None;
}
loop {
self.advance();
if self.finished {
break None;
}
if self.clauses.len() == 0 {
break Some(());
}
}
}
}
mod test {}
Loading…
Cancel
Save