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.
 
 

309 lines
9.2 KiB

// vim: ts=4 sw=4 et
use colored::{control::ShouldColorize, Colorize};
use core::fmt::{Display, Formatter};
use std::cell::RefCell;
use std::rc::Rc;
#[derive(Debug)]
struct VariableInner {
name: String,
assignment: RefCell<Option<bool>>,
}
#[derive(Clone, Debug)]
pub struct Variable(Rc<VariableInner>);
impl Variable {
pub fn from_name(name: String) -> Variable {
Variable(Rc::new(VariableInner {
name,
assignment: RefCell::new(None),
}))
}
pub fn get_name(&self) -> &String {
&self.0.name
}
pub fn assign(&self, v: bool) {
*self.0.assignment.borrow_mut() = Some(v);
}
pub fn unassign(&self) {
*self.0.assignment.borrow_mut() = None;
}
pub fn get_assignment(&self) -> Option<bool> {
self.0.assignment.borrow().clone()
}
pub fn get_literal(&self, neg: bool) -> Literal {
Literal {
neg,
var: self.clone(),
}
}
pub fn get_pos_literal(&self) -> Literal {
self.get_literal(false)
}
pub fn get_neg_literal(&self) -> Literal {
self.get_literal(true)
}
fn get_uncolored_string(&self) -> String {
let should_color = ShouldColorize::from_env().should_colorize();
macro_rules! cd {
($($s:literal)?) => {
if should_color {
format!("{}", self.0.name)
} else {
format!(concat!($($s, )?"{}"), self.0.name)
}
}
}
match self.get_assignment() {
None => cd!(),
Some(true) => cd!("¹"),
Some(false) => cd!("⁰"),
}
}
}
impl Display for Variable {
fn fmt(&self, fmt: &mut Formatter) -> core::fmt::Result {
let should_color = ShouldColorize::from_env().should_colorize();
macro_rules! cd {
($($s:literal)?$(, $col:ident)?) => {
if should_color {
write!(fmt, "{}", self.0.name$(.$col())?)
} else {
write!(fmt, concat!($($s, )?"{}"), self.0.name)
}
}
}
match self.get_assignment() {
None => cd!(),
Some(true) => cd!("¹", bright_blue),
Some(false) => cd!("⁰", bright_red),
}
}
}
#[derive(Clone, Debug)]
pub struct Literal {
neg: bool,
var: Variable,
}
impl Literal {
pub fn assign(&self, v: bool) {
self.var.assign(v ^ self.neg);
}
pub fn unassign(&self) {
self.var.unassign();
}
pub fn get_assignment(&self) -> Option<bool> {
self.var.get_assignment().map(|x| x ^ 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 {
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),
}
}
}
#[derive(Clone, Debug)]
pub struct Clause {
literals: Vec<Literal>,
}
impl Clause {
pub fn new() -> Clause {
Clause {
literals: Vec::new(),
}
}
pub fn push(&mut self, l: Literal) {
self.literals.push(l);
}
pub fn len(&self) -> usize {
self.literals.len()
}
pub fn iter(&self) -> impl Iterator<Item = &Literal> {
self.literals.iter()
}
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 Display for Clause {
fn fmt(&self, fmt: &mut Formatter) -> core::fmt::Result {
if self.literals.len() == 0 {
write!(fmt, "⊥")
} else {
let mut iter = self.literals.iter();
write!(fmt, "{} ", iter.next().unwrap())?;
for lit in iter {
write!(fmt, " ∨ {}", lit)?;
}
Ok(())
}
}
}
#[cfg(test)]
mod test {
use super::*;
#[test]
fn clause_test() {
let x = Variable::from_name("x".into());
let y = Variable::from_name("y".into());
let z = Variable::from_name("z".into());
let w = Variable::from_name("w".into());
println!(
"names: {} {} {} {}",
x.get_name(),
y.get_name(),
z.get_name(),
w.get_name()
);
println!("x: {}, y: {}, z: {}, w: {}", x, y, z, w);
x.assign(true);
y.assign(false);
z.unassign();
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);
xl.assign(false);
yl.assign(true);
zl.assign(true);
wl.assign(false);
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));
xl.unassign();
yl.unassign();
zl.unassign();
wl.unassign();
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);
x.assign(true);
println!("clause: {}", clause);
println!("value: {:?}", clause.eval());
assert_eq!(clause.eval(), Some(true));
x.assign(false);
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);
y.assign(true);
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);
z.assign(false);
w.assign(true);
println!("clause: {}", clause);
println!("value: {:?}", clause.eval());
assert_eq!(clause.eval(), Some(false));
x.assign(true);
println!("clause: {}", clause);
println!("value: {:?}", clause.eval());
assert_eq!(clause.eval(), Some(true));
y.assign(false);
println!("clause: {}", clause);
println!("value: {:?}", clause.eval());
assert_eq!(clause.eval(), Some(true));
}
}