Browse Source

Added untested MAXSAT-to-ILP reduction

karmarkar
Thomas Johnson 3 years ago
parent
commit
397b310929
  1. 73
      src/karmarkar.rs

73
src/karmarkar.rs

@ -1,5 +1,6 @@
// vim: ts=4 sw=4 et
use crate::clause;
use core::fmt::{Display, Formatter};
use core::mem;
use core::ops::{Add, AddAssign, Mul, MulAssign, Neg, Shl};
@ -9,8 +10,6 @@ use nalgebra::{DMatrix, DVector, Vector};
pub type Fl = f64;
// In case it wasn't clear, variable names and algorithm details are ripped straight from the
// Wikipedia page. Some day I'll go back and understand the algorithm in greater depth, I promise.
#[allow(non_upper_case_globals)]
pub static DEFAULT_α: Fl = 0.25;
#[allow(non_upper_case_globals)]
@ -1047,6 +1046,76 @@ impl BMIPSolver {
}
}
fn clause_to_inequality(
clause: &clause::Clause,
varmap: &HashMap<clause::Variable, Variable>,
) -> LeqInequality {
let mut expr = Expr::from(0.0);
for literal in clause.iter() {
if literal.is_neg() {
expr += 1.0;
expr += -varmap.get(&literal.get_variable()).unwrap();
} else {
expr += varmap.get(&literal.get_variable()).unwrap();
}
}
expr << 1.0
}
/// Accepts a ClauseList and a list of weights. Entries correspond between the lists. If the weight
/// is `None`, the clause is hard; otherwise, it's soft with the given weight. If the weight list
/// is too short, the clauses with no weight assumed to be hard.
pub fn clause_list_to_constraints<T: Copy>(
clause_list: &mut clause::ClauseList,
weights: &Vec<Option<T>>,
) -> (
Vec<LeqInequality>,
LinearCombination,
HashMap<clause::Variable, Variable>,
)
where
Fl: From<T>,
{
let mut weightmap = HashMap::new();
let mut counter = 0;
for (i, clause) in clause_list.iter_mut().enumerate() {
if let Some(Some(weight)) = weights.get(i) {
counter += 1;
let b = clause::Variable::from_name(format!("_b{}", counter));
weightmap.insert(b.clone(), Fl::from(*weight));
clause.push(b.get_pos_literal());
}
}
let mut varmap = HashMap::new();
let mut objective = LinearCombination::new();
let vars = clause_list.get_vars();
for var in &vars {
let lvar = Variable::from_name(var.get_name().clone());
weightmap
.get(&var)
.map(|x| objective.insert_variable(lvar.clone(), *x));
varmap.insert(var.clone(), lvar);
}
let mut constraints = Vec::new();
for clause in clause_list.iter() {
constraints.push(clause_to_inequality(&clause, &varmap));
}
(constraints, objective, varmap)
}
pub fn ilp_maxsat<T: Copy>(mut clause_list: clause::ClauseList, weights: &Vec<Option<T>>)
where
Fl: From<T>,
{
let (ineqs, objective, varmap) = clause_list_to_constraints(&mut clause_list, weights);
let varset = varmap.values().cloned();
let mut solver = BMIPSolver::from_ineqs_and_objective(ineqs, varset, objective);
solver.solve();
for (bv, lv) in varmap {
lv.get_assignment().map(|x| x > 0.5).map(|x| bv.assign(x));
}
}
#[cfg(test)]
mod test {
use super::*;

Loading…
Cancel
Save