otter_sat 0.0.9

A library for determining the satisfiability of boolean formulas written in conjunctive normal form, developed to support investigation into solvers by researchers, developers, or anyone curious.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31

//! Schedulers, used to interrupt a solve for some task.
//!
//! These return true if an interrupt is due, and false otherwise.
//!
//! For the moment, scheduling during a solve is experimental.

use crate::context::GenericContext;

impl<R: rand::Rng + std::default::Default> GenericContext<R> {
    /// Returns whether it is time for a interrupt based on whether fresh conflicts are a multiple of the current luby element.
    pub fn luby_fresh_conflict_interrupt(&self) -> bool {
        self.counters.fresh_conflicts % (self.config.luby_u * self.counters.luby.current()) == 0
    }

    /// Returns whether it is time for a interrupt based on whether total conflicts is multiple of the configured interval.
    #[inline(always)]
    pub fn conflict_total_interrupt(&self) -> bool {
        self.config
            .scheduler
            .conflict
            .is_some_and(|interval| (self.counters.total_conflicts % (interval as usize)) == 0)
    }

    /// Returns whether it is time for a interrupt based on whether total restarts is multiple of the configured interval.
    pub fn restart_interrupt(&self) -> bool {
        self.config
            .scheduler
            .restart
            .is_some_and(|interval| (self.counters.restarts % (interval as usize)) == 0)
    }
}