Struct sat::Instance

pub struct Instance { /* 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.