Struct sat::Instance [−] [src]

pub struct Instance {
    // some fields omitted
}

An instance of the SAT problem.

Methods

impl Instance

fn new() -> Instance

Create a new, empty SAT instance.

fn fresh_var(&mut self) -> Literal

Create a fresh variable.

fn assert_any<'a, I>(&mut self, lits: I) where I: IntoIterator<Item=&'a Literal>

Assert that at least one of the provided literals must evaluate to true.

This is a CNF (conjunctive normal form) constraint, which is the basic type of constraint in most solvers.