Struct cadical::Solver

pub struct Solver<C: Callbacks = Timeout> { /* private fields */ }

The CaDiCaL incremental SAT solver. The literals are unwrapped positive and negative integers, exactly as in the DIMACS format. The common IPASIR operations are presented in a safe Rust interface.

Examples

let mut sat: cadical::Solver = Default::default();
sat.add_clause([1, 2]);
sat.add_clause([-1, 2]);
assert_eq!(sat.solve(), Some(true));
assert_eq!(sat.value(2), Some(true));

Implementations

impl<C: Callbacks> Solver<C>

pub fn new() -> Self

Constructs a new solver instance.

pub fn with_config(config: &str) -> Result<Self, Error>

Constructs a new solver with one of the following pre-defined configurations of advanced internal options:

• default: set default advanced internal options
• plain: disable all internal preprocessing options
• sat: set internal options to target satisfiable instances
• unsat: set internal options to target unsatisfiable instances

pub fn signature(&self) -> &str

Returns the name and version of the CaDiCaL library.

pub fn add_clause<I>(&mut self, clause: I)where
    I: IntoIterator<Item = i32>,

Adds the given clause to the solver. Negated literals are negative integers, positive literals are positive ones. All literals must be non-zero and different from i32::MIN.

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

Solves the formula defined by the added clauses. If the formula is satisfiable, then Some(true) is returned. If the formula is unsatisfiable, then Some(false) is returned. If the solver runs out of resources or was terminated, then None is returned.

pub fn solve_with<I>(&mut self, assumptions: I) -> Option<bool>where
    I: Iterator<Item = i32>,

Solves the formula defined by the set of clauses under the given assumptions.

pub fn status(&self) -> Option<bool>

Returns the status of the solver as returned by the last call to solve or solve_with. The state becomes None if a new clause is added.

pub fn value(&self, lit: i32) -> Option<bool>

Returns the value of the given literal in the last solution. The state of the solver must be Some(true). The returned value is None if the formula is satisfied regardless of the value of the literal.

pub fn failed(&self, lit: i32) -> bool

Checks if the given assumed literal (passed to solve_with) was used in the proof of the unsatisfiability of the formula. The state of the solver must be Some(false).

pub fn max_variable(&self) -> i32

Returns the maximum variable index in the problem as maintained by the solver.

Examples

let mut sat: cadical::Solver = Default::default();
sat.add_clause([1, -3]);
assert_eq!(sat.max_variable(), 3);
assert_eq!(sat.num_variables(), 2);
assert_eq!(sat.num_clauses(), 1);

pub fn num_variables(&self) -> i32

Returns the number of active variables in the problem. Variables become active if a clause is added with it. They become inactive, if they are eliminated or become fixed at the root level.

pub fn num_clauses(&self) -> usize

Returns the number of active irredundant clauses. Clauses become inactive if they are satisfied, subsumed or eliminated.

pub fn set_limit(&mut self, name: &str, limit: i32) -> Result<(), Error>

Sets a solver limit with the corresponding name to the given value. These limits are only valid for the next solve or solve_with call and reset to their default values, which disables them. The following limits are supported:

• preprocessing: the number of preprocessing rounds to be performed during the search (defaults to 0).
• localsearch: the number of local search rounds to be performed during the search (defaults to 0).
• terminate: this value is regularly decremented and aborts the solver when it reaches zero (defaults to 0).
• conflicts: decremented when a conflict is detected and aborts the solver when it becomes negative (defaults to -1).
• decisions: decremented when a decision is made and aborts the solver when it becomes negative (defaults to -1).

pub fn set_callbacks(&mut self, cbs: Option<C>)

Sets the callbacks to be called while the solver is running.

Examples

let mut sat: cadical::Solver = Default::default();
sat.add_clause([1, 2]);
sat.set_callbacks(Some(cadical::Timeout::new(0.0)));
assert_eq!(sat.solve(), None);

pub fn get_callbacks(&mut self) -> Option<&mut C>

Returns a mutable reference to the callbacks.

pub fn write_dimacs(&mut self, path: &Path) -> Result<(), Error>

Writes the problem in DIMACS format to the given file.

pub fn read_dimacs(&mut self, path: &Path) -> Result<i32, Error>

Reads a problem in DIMACS format from the given file. You must call this function during configuration time, before adding any clauses. Returns the number of variables as reported by the loader.

Trait Implementations

impl<C: Callbacks> Default for Solver<C>

fn default() -> Self

Returns the “default value” for a type.

impl<C: Callbacks> Drop for Solver<C>

fn drop(&mut self)

Executes the destructor for this type.

impl<C: Callbacks + Send> Send for Solver<C>

CaDiCaL does not use thread local variables, so it is possible to move it between threads. However it cannot be used queried concurrently (for example getting the value from multiple threads at once), so we do not implement Sync.