Solving MAXSAT and saying a few words about it.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 

482 lines
15 KiB

// vim: ts=4 sw=4 et
use colored::{control::ShouldColorize, Colorize};
use core::fmt::{Display, Formatter};
use std::collections::hash_map::HashMap;
use std::collections::hash_set::HashSet;
pub type Variable = crate::variable::Variable<bool>;
/// A literal -- that is, an expression which is either a variable or the negation of a variable.
#[derive(Clone, Debug)]
pub struct Literal {
neg: bool,
var: Variable,
}
impl Literal {
/// Constructs a literal from a variable.
pub fn from_var(var: Variable, neg: bool) -> Literal {
Literal { neg, var }
}
/// Assign a value to the literal. Note that if the literal is negated, the assignment to the
/// underlying variable is also negated.
pub fn assign(&self, v: bool) {
self.var.assign(v ^ self.neg);
}
/// Removes the assignment from the underlying variable.
pub fn unassign(&self) {
self.var.unassign();
}
/// Gets the assignment of the literal. This evaluates the literal based on the assignment to
/// the underlying variable.
pub fn get_assignment(&self) -> Option<bool> {
self.var.get_assignment().map(|x| x ^ self.neg)
}
/// Returns a clone of the underlying variable.
pub fn get_variable(&self) -> Variable {
self.var.clone()
}
/// Returns `true` iff the literal is a negation of the underlying variable.
pub fn is_neg(&self) -> bool {
self.neg
}
}
impl Display for Literal {
fn fmt(&self, fmt: &mut Formatter) -> core::fmt::Result {
let should_color = ShouldColorize::from_env().should_colorize();
macro_rules! cd {
($($s:literal)?, $($n:literal)?, $($coln:ident, $colt:ident)?) => {
if should_color {
write!(fmt, "{}{}", {concat!($($n, )?"")}$(.$coln())?.bold(), self.var.get_uncolored_string()$(.$colt())?.bold())
} else {
write!(fmt, concat!($($s, )?$($n, )?"{}"), self.var)
}
}
}
macro_rules! nd {
($($s:literal)?$(, $coln:ident, $colt:ident)?) => {
if self.neg {
#[cfg(not(no_unicode))]
{ cd!($($s)?, "¬", $($coln, $colt)?) }
#[cfg(no_unicode)]
{ cd!($($s)?, "~", $($coln, $colt)?) }
} else {
cd!($($s)?, , $($coln, $colt)?)
}
}
}
match (self.get_assignment(), self.neg) {
(None, _) => nd!(),
(Some(true), true) => nd!("¹", bright_blue, bright_blue),
(Some(true), false) => nd!("¹", bright_cyan, bright_cyan),
(Some(false), true) => nd!("⁰", yellow, yellow),
(Some(false), false) => nd!("⁰", bright_red, bright_red),
}
}
}
/// A disjunctive clause of literals.
#[derive(Clone, Debug)]
pub struct Clause {
literals: Vec<Literal>,
}
impl Clause {
/// Creates a new empty clause.
pub fn new() -> Clause {
Clause {
literals: Vec::new(),
}
}
/// Disjoins (ORs) a literal with the clause.
pub fn push(&mut self, l: Literal) {
self.literals.push(l);
}
/// Returns the number of literals in the clause.
pub fn len(&self) -> usize {
self.literals.len()
}
/// Returns an iterator through all the literals in the clause.
pub fn iter(&self) -> impl Iterator<Item = &Literal> {
self.literals.iter()
}
/// Returns a mutable iterator through all the literals in the clause.
pub fn iter_mut(&mut self) -> impl Iterator<Item = &mut Literal> {
self.literals.iter_mut()
}
/// Swaps the literals at two indicies.
pub fn swap(&mut self, i: usize, j: usize) {
self.literals.swap(i, j);
}
/// If all the literals in the clause are assigned, return the truth value of the clause.
/// Otherwise, return `None`.
pub fn eval(&self) -> Option<bool> {
self.literals.iter().fold(Some(false), |r, o| {
r.and_then(|b| o.get_assignment().map(|v| v | b))
})
}
}
impl core::ops::Index<usize> for Clause {
type Output = Literal;
fn index(&self, idx: usize) -> &Self::Output {
&self.literals[idx]
}
}
impl core::ops::IndexMut<usize> for Clause {
fn index_mut(&mut self, idx: usize) -> &mut Self::Output {
&mut self.literals[idx]
}
}
impl Display for Clause {
fn fmt(&self, fmt: &mut Formatter) -> core::fmt::Result {
if self.literals.len() == 0 {
#[cfg(not(no_unicode))]
{
write!(fmt, "⊥")?;
}
#[cfg(no_unicode)]
{
write!(fmt, "FALSE")?;
}
} else {
let mut iter = self.literals.iter();
write!(fmt, "{}", iter.next().unwrap())?;
for lit in iter {
#[cfg(not(no_unicode))]
{
write!(fmt, " ∨ {}", lit)?;
}
#[cfg(no_unicode)]
{
write!(fmt, " v {}", lit)?;
}
}
}
Ok(())
}
}
/// Represents a list of clauses.
#[derive(Debug)]
pub struct ClauseList {
clauses: Vec<Clause>,
}
impl ClauseList {
/// Creates a new, empty list of clauses.
pub fn new() -> ClauseList {
ClauseList {
clauses: Vec::new(),
}
}
/// Creates a copy of the clause list. Note that the underlying variables still share a
/// reference.
pub fn copy(&self) -> ClauseList {
ClauseList {
clauses: self.clauses.clone(),
}
}
/// Adds a clause to the list.
pub fn push(&mut self, clause: Clause) {
self.clauses.push(clause);
}
/// Returns the number of clauses in the list.
pub fn len(&self) -> usize {
self.clauses.len()
}
/// Returns an iterator over all the clauses in the list.
pub fn iter(&self) -> impl Iterator<Item = &Clause> {
self.clauses.iter()
}
/// Returns a mutable iterator over all the clauses in the list.
pub fn iter_mut(&mut self) -> impl Iterator<Item = &mut Clause> {
self.clauses.iter_mut()
}
/// Returns a `HashSet` over all the variables referenced in the clauses in the list. Note that
/// the returned variables share a reference with the ones in the clause list.
pub fn get_vars(&self) -> HashSet<Variable> {
let mut set = HashSet::new();
for clause in self.iter() {
for lit in clause.iter() {
set.insert(lit.get_variable().clone());
}
}
set
}
/// Returns a vector containing all the clauses in the list.
pub fn into_vec(self) -> Vec<Clause> {
self.clauses
}
}
// Properly creates new variables that don't share assignments with the old ones
/// Note that cloning a clause list gives a new list whose variables do not share references with
/// the ones from the old list. Use `copy` if you don't want this.
impl Clone for ClauseList {
fn clone(&self) -> Self {
let mut map = HashMap::<_, Variable>::new();
let mut clauselist = ClauseList::new();
for clause in self.iter() {
let mut newclause = Clause::new();
for lit in clause.iter() {
let key = lit.get_variable().get_ptr();
if map.contains_key(&key) {
newclause.push(map.get(&key).unwrap().get_literal(lit.is_neg()));
} else {
let var = lit.get_variable().duplicate();
newclause.push(var.get_literal(lit.is_neg()));
map.insert(key, var);
}
}
clauselist.push(newclause);
}
clauselist
}
}
impl core::ops::Index<usize> for ClauseList {
type Output = Clause;
fn index(&self, idx: usize) -> &Self::Output {
&self.clauses[idx]
}
}
impl core::ops::IndexMut<usize> for ClauseList {
fn index_mut(&mut self, idx: usize) -> &mut Self::Output {
&mut self.clauses[idx]
}
}
impl Display for ClauseList {
fn fmt(&self, fmt: &mut Formatter) -> core::fmt::Result {
for clause in self.iter() {
write!(fmt, "{}\n", clause)?;
}
Ok(())
}
}
#[macro_export]
/// Defines a DSL which allows for the declaration of many variables at once. See the unit tests
/// for examples.
macro_rules! clause_vars {
[] => {};
[$varname:ident$(,)?] => {
let $varname = $crate::clause::Variable::from_name(stringify!($varname).into());
};
[$varname:ident, $($varnames:ident),+] => {
let $varname = $crate::clause::Variable::from_name(stringify!($varname).into());
clause_vars![$($varnames),+]
};
}
/// Defines a DSL for assigning many variables at once. See the unit tests for examples.
#[macro_export]
macro_rules! assign_vars {
{ } => {};
{$var:ident = 1; $($vars:ident$( = $vals:tt)?;)*} =>
{
$var.assign(true);
assign_vars! { $($vars$( = $vals)?;)* } //$($vars = $vals;)* }
};
{$var:ident = 0; $($vars:ident$( = $vals:tt)?;)*} =>
{
$var.assign(false);
assign_vars! { $($vars$( = $vals)?;)* }
};
{$var:ident; $($vars:ident$( = $vals:tt)?;)*} =>
{
$var.unassign();
assign_vars! { $($vars$( = $vals)?;)* }
};
}
#[allow(unused_macros)]
macro_rules! add_terms {
($varname:ident) => {};
($varname:ident - $literal:ident $(| $($rest:tt)*)? ) => {
$varname.push($literal.get_neg_literal());
add_terms!($varname $($($rest)*)?)
};
($varname:ident $literal:ident $(| $($rest:tt)*)? ) => {
$varname.push($literal.get_pos_literal());
add_terms!($varname $($($rest)*)?)
};
}
/// Defines a DSL for constructing clauses using a convenient syntax. See the unit tests for
/// examples.
#[macro_export]
macro_rules! make_clause {
{ } => { Clause::new() };
( $($contents:tt)* ) => {{
let mut clause = $crate::clause::Clause::new();
add_terms!(clause $($contents)*);
clause
}};
}
#[cfg(test)]
mod test {
use super::*;
#[test]
fn clause_test() {
clause_vars![x, y, z, w];
println!(
"names: {} {} {} {}",
x.get_name(),
y.get_name(),
z.get_name(),
w.get_name()
);
println!("x: {}, y: {}, z: {}, w: {}", x, y, z, w);
assign_vars! {
x = 1;
y = 0;
z;
}
println!("x: {}, y: {}, z: {}, w: {}", x, y, z, w);
assert_eq!(x.get_assignment(), Some(true));
assert_eq!(y.get_assignment(), Some(false));
assert_eq!(z.get_assignment(), None);
assert_eq!(w.get_assignment(), None);
let xl = x.get_literal(false);
let yl = y.get_literal(true);
let zl = z.get_pos_literal();
let wl = w.get_neg_literal();
println!("xl: {}, yl: {}, zl: {}, wl: {}", xl, yl, zl, wl);
assert_eq!(xl.get_assignment(), Some(true));
assert_eq!(yl.get_assignment(), Some(true));
assert_eq!(zl.get_assignment(), None);
assert_eq!(wl.get_assignment(), None);
assign_vars! {
xl = 0;
yl = 1;
zl = 1;
wl = 0;
}
println!("assigned literals");
println!("x: {}, y: {}, z: {}, w: {}", x, y, z, w);
assert_eq!(x.get_assignment(), Some(false));
assert_eq!(y.get_assignment(), Some(false));
assert_eq!(z.get_assignment(), Some(true));
assert_eq!(w.get_assignment(), Some(true));
println!("xl: {}, yl: {}, zl: {}, wl: {}", xl, yl, zl, wl);
assert_eq!(xl.get_assignment(), Some(false));
assert_eq!(yl.get_assignment(), Some(true));
assert_eq!(zl.get_assignment(), Some(true));
assert_eq!(wl.get_assignment(), Some(false));
assign_vars! {
xl;
yl;
zl;
wl;
}
println!("unassigned literals");
println!("x: {}, y: {}, z: {}, w: {}", x, y, z, w);
assert_eq!(x.get_assignment(), None);
assert_eq!(y.get_assignment(), None);
assert_eq!(z.get_assignment(), None);
assert_eq!(w.get_assignment(), None);
println!("xl: {}, yl: {}, zl: {}, wl: {}", xl, yl, zl, wl);
assert_eq!(xl.get_assignment(), None);
assert_eq!(yl.get_assignment(), None);
assert_eq!(zl.get_assignment(), None);
assert_eq!(wl.get_assignment(), None);
let mut clause = Clause::new();
println!("clause: {}", clause);
println!("value: {:?}", clause.eval());
assert_eq!(clause.eval(), Some(false));
clause.push(xl);
println!("clause: {}", clause);
println!("value: {:?}", clause.eval());
assert_eq!(clause.eval(), None);
assign_vars! { x = 1; }
println!("clause: {}", clause);
println!("value: {:?}", clause.eval());
assert_eq!(clause.eval(), Some(true));
assign_vars! { x = 0; }
println!("clause: {}", clause);
println!("value: {:?}", clause.eval());
assert_eq!(clause.eval(), Some(false));
clause.push(yl);
println!("clause: {}", clause);
println!("value: {:?}", clause.eval());
assert_eq!(clause.eval(), None);
assign_vars! { y = 1; }
println!("clause: {}", clause);
println!("value: {:?}", clause.eval());
assert_eq!(clause.eval(), Some(false));
clause.push(zl);
clause.push(wl);
println!("clause: {}", clause);
println!("value: {:?}", clause.eval());
assert_eq!(clause.eval(), None);
assign_vars! { z = 0; w = 1; }
println!("clause: {}", clause);
println!("value: {:?}", clause.eval());
assert_eq!(clause.eval(), Some(false));
assign_vars! { x = 1; }
println!("clause: {}", clause);
println!("value: {:?}", clause.eval());
assert_eq!(clause.eval(), Some(true));
assign_vars! { y = 0; }
println!("clause: {}", clause);
println!("value: {:?}", clause.eval());
assert_eq!(clause.eval(), Some(true));
let clause2 = make_clause!(-x | -y | z | w);
let mut clauselist = ClauseList::new();
clauselist.push(clause);
clauselist.push(clause2);
println!("clause listing:");
for clause in clauselist.iter() {
println!("{}", clause);
}
let clauselist2 = clauselist.clone();
println!("clause2 listing:");
for clause in clauselist2.iter() {
println!("{}", clause);
}
for clause in clauselist2.iter() {
for lit in clause.iter() {
lit.unassign();
}
}
println!("clause listing:");
for clause in clauselist.iter() {
println!("{}", clause);
}
println!("clause2 listing:");
for clause in clauselist2.iter() {
println!("{}", clause);
}
}
}