Struct rustsat_kissat::Kissat

pub struct Kissat<'term> { /* private fields */ }

The Kissat solver type

Implementations

impl Kissat<'_>

pub fn commit_id() -> &'static str

Gets the commit ID that Kissat was built from

pub fn version() -> &'static str

Gets the Kissat version

pub fn compiler() -> &'static str

Gets the compiler Kissat was built with

pub fn set_configuration(&mut self, config: Config) -> Result<()>

Sets a pre-defined configuration for Kissat’s internal options

pub fn set_option(&mut self, name: &str, value: c_int) -> Result<()>

Sets the value of a Kissat option. For possible options, check Kissat with kissat --help. Requires state SolverState::Configuring.

pub fn get_option(&self, name: &str) -> Result<c_int>

Gets the value of a Kissat option. For possible options, check Kissat with kissat --help.

pub fn set_limit(&mut self, limit: Limit)

Sets an internal limit for Kissat

pub fn print_stats(&self)

Prints the solver statistics from the Kissat backend

Trait Implementations

impl Default for Kissat<'_>

fn default() -> Self

Returns the “default value” for a type.

impl Drop for Kissat<'_>

fn drop(&mut self)

Executes the destructor for this type.

impl<'a> Extend<&'a Clause> for Kissat<'_>

fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T)

Extends a collection with the contents of an iterator.

fn extend_one(&mut self, item: A)

🔬This is a nightly-only experimental API. (extend_one)

Extends a collection with exactly one element.

fn extend_reserve(&mut self, additional: usize)

🔬This is a nightly-only experimental API. (extend_one)

Reserves capacity in a collection for the given number of additional elements.

impl Extend<Clause> for Kissat<'_>

fn extend<T: IntoIterator<Item = Clause>>(&mut self, iter: T)

Extends a collection with the contents of an iterator.

fn extend_one(&mut self, item: A)

🔬This is a nightly-only experimental API. (extend_one)

Extends a collection with exactly one element.

fn extend_reserve(&mut self, additional: usize)

🔬This is a nightly-only experimental API. (extend_one)

Reserves capacity in a collection for the given number of additional elements.

impl Interrupt for Kissat<'_>

type Interrupter = Interrupter

The interrupter of the solver

fn interrupter(&mut self) -> Self::Interrupter

Gets a thread safe interrupter object that can be used to terminate the solver

impl Solve for Kissat<'_>

fn signature(&self) -> &'static str

Gets a signature of the solver implementation

fn reserve(&mut self, max_var: Var) -> Result<()>

Reserves memory in the solver until a maximum variables, if the solver supports it

fn solve(&mut self) -> Result<SolverResult>

Solves the internal CNF formula without any assumptions.

fn lit_val(&self, lit: Lit) -> Result<TernaryVal>

Gets an assignment of a variable in the solver.

fn add_clause_ref(&mut self, clause: &Clause) -> Result<()>

Adds a clause to the solver by reference. If the solver is in the satisfied or unsatisfied state before, it is in the input state afterwards.

fn solution(&self, high_var: Var) -> Result<Assignment, Error>

Gets a solution found by the solver up to a specified highest variable.

fn full_solution(&self) -> Result<Assignment, Error>

where Self: SolveStats,

Gets a solution found by the solver up to the highest variable known to the solver.

fn var_val(&self, var: Var) -> Result<TernaryVal, Error>

Same as Solve::lit_val, but for variables.

fn add_clause(&mut self, clause: Clause) -> Result<(), Error>

Adds a clause to the solver. If the solver is in the satisfied or unsatisfied state before, it is in the input state afterwards.

fn add_unit(&mut self, lit: Lit) -> Result<(), Error>

Like Solve::add_clause but for unit clauses (clauses with one literal).

fn add_binary(&mut self, lit1: Lit, lit2: Lit) -> Result<(), Error>

Like Solve::add_clause but for clauses with two literals.

fn add_ternary(&mut self, lit1: Lit, lit2: Lit, lit3: Lit) -> Result<(), Error>

Like Solve::add_clause but for clauses with three literals.

fn add_cnf(&mut self, cnf: Cnf) -> Result<(), Error>

Adds all clauses from a Cnf instance.

fn add_cnf_ref(&mut self, cnf: &Cnf) -> Result<(), Error>

Adds all clauses from a Cnf instance by reference.

impl SolveStats for Kissat<'_>

fn stats(&self) -> SolverStats

Gets the available statistics from the solver

fn n_sat_solves(&self) -> usize

Gets the number of satisfiable queries executed.

fn n_unsat_solves(&self) -> usize

Gets the number of unsatisfiable queries executed.

fn n_terminated(&self) -> usize

Gets the number of queries that were prematurely terminated.

fn n_solves(&self) -> usize

Gets the total number of queries executed.

fn n_clauses(&self) -> usize

Gets the number of clauses in the solver.

fn max_var(&self) -> Option<Var>

Gets the variable with the highest index in the solver, if any. If all variables below have been used, the index of this variable +1 is the number of variables in the solver.

fn n_vars(&self) -> usize

Get number of variables. Note: this is only correct if all variables are used in order!

fn avg_clause_len(&self) -> f32

Gets the average length of all clauses in the solver.

fn cpu_solve_time(&self) -> Duration

Gets the total CPU time spent solving.

impl<'term> Terminate<'term> for Kissat<'term>

fn attach_terminator<CB>(&mut self, cb: CB)

where CB: FnMut() -> ControlSignal + 'term,

Sets a terminator callback that is regularly called during solving.

Examples

Terminate solver after 10 callback calls.

use rustsat::solvers::{ControlSignal, Solve, SolverResult, Terminate};
use rustsat_kissat::Kissat;

let mut solver = Kissat::default();

// Load instance

let mut cnt = 1;
solver.attach_terminator(move || {
    if cnt > 10 {
        ControlSignal::Terminate
    } else {
        cnt += 1;
        ControlSignal::Continue
    }
});

let ret = solver.solve().unwrap();

// Assuming an instance is actually loaded and runs long enough
// assert_eq!(ret, SolverResult::Interrupted);

fn detach_terminator(&mut self)

Detaches the terminator

impl Send for Kissat<'_>