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.
 
 

66 lines
1.3 KiB

// vim: ts=4 sw=4 et
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 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) }
}
#[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)
}
}
pub struct Clause {
pub literals: Vec<Literal>,
}