Trait satoxid::Solver

pub trait Solver: Backend {
    fn solve(&mut self) -> bool;
    fn value(&self, var: i32) -> bool;
}

A trait for Backends with are capable of solving SAT Problems.

Required methods

fn solve(&mut self) -> bool

Solve the encoded SAT problem. Returns true if the problem is satisfiable.

fn value(&self, var: i32) -> bool

Returns if the integer SAT variable is true in the model or not.

This function should panic if solve wasn’t called previously or wasn’t able to solve the problem.

Implementations on Foreign Types

impl Solver for Solver

fn solve(&mut self) -> bool

fn value(&self, var: i32) -> bool

Implementors