Struct HornSatisfiability 

pub struct HornSatisfiability {
    literals: Vec<Option<bool>>,
    clauses: Vec<(usize, usize, bool)>,
    idx: Vec<Vec<usize>>,
    satisfiable: bool,
    stack: Vec<usize>,
}

Horn Satisfiability

$\wedge(\wedge_i v_{p_i}\rightarrow v_q = f)$

Fields

literals: Vec<Option<bool>>

clauses: Vec<(usize, usize, bool)>

idx: Vec<Vec<usize>>

satisfiable: bool

stack: Vec<usize>

Implementations

impl HornSatisfiability

pub fn new(size: usize) -> Self

pub fn add_clause( &mut self, p: impl IntoIterator<Item = usize>, q: usize, f: bool, )

pub fn is_satisfiable(&self) -> bool

pub fn solve(&self) -> Option<Vec<bool>>

fn resolve(&mut self)

Examples found in repository

crates/competitive/src/algorithm/horn_satisfiability.rs (line 35)

    pub fn add_clause(&mut self, p: impl IntoIterator<Item = usize>, q: usize, f: bool) {
        let mut count = 0;
        let id = self.clauses.len();
        for p_i in p.into_iter() {
            if self.literals[p_i] != Some(true) {
                self.idx[p_i].push(id);
                count += 1;
            }
        }
        self.clauses.push((count, q, f));
        if count == 0 {
            self.stack.push(id);
            self.resolve();
        }
    }