permanganate 0.2.0

Graph and Boolean SAT solver for Numberlink and Flow Free
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

use std::ops::Index;

use itertools::Itertools;
use varisat::Lit;

fn invert(lit: Lit) -> Lit {
    match lit.is_negative() {
        true => lit.var().positive(),
        false => lit.var().negative(),
    }
}

pub(crate) fn exactly_one(vars: Vec<Lit>) -> Vec<Vec<Lit>> {
    let mut clauses = Vec::with_capacity(vars.len() * (vars.len() + 1) / 2 + 1);

    // no two are true; (!A + !B) * (!A + !C) * ...
    clauses.extend(vars.iter()
        .combinations(2)
        .map(|pair| vec![invert(**pair.index(0)), invert(**pair.index(1))])
    );
    // at least one var is true; A + B + C + ...
    clauses.push(vars);

    clauses
}