Struct SolverConfig 

pub struct SolverConfig {

    pub timeout_ms: u64,
    pub parallel: bool,
    pub num_threads: usize,
    pub proof: bool,
    pub model: bool,
    pub theory_mode: TheoryMode,
    pub simplify: bool,
    pub max_conflicts: u64,
    pub max_decisions: u64,
    pub restart_strategy: RestartStrategy,
    pub enable_clause_minimization: bool,
    pub enable_clause_subsumption: bool,
    pub enable_variable_elimination: bool,
    pub variable_elimination_limit: usize,
    pub enable_blocked_clause_elimination: bool,
    pub enable_symmetry_breaking: bool,
    pub enable_inprocessing: bool,
    pub inprocessing_interval: u64,
}

Solver configuration

Fields

timeout_ms: u64

Timeout in milliseconds (0 = no timeout)

parallel: bool

Enable parallel solving

num_threads: usize

Number of threads for parallel solving

proof: bool

Enable proof generation

model: bool

Enable model generation

theory_mode: TheoryMode

Theory checking mode

simplify: bool

Enable preprocessing/simplification

max_conflicts: u64

Maximum number of conflicts before giving up (0 = unlimited)

max_decisions: u64

Maximum number of decisions before giving up (0 = unlimited)

restart_strategy: RestartStrategy

Restart strategy for SAT solver

enable_clause_minimization: bool

Enable clause minimization (recursive minimization of learned clauses)

enable_clause_subsumption: bool

Enable learned clause subsumption

enable_variable_elimination: bool

Enable variable elimination during preprocessing

variable_elimination_limit: usize

Variable elimination limit (max clauses to produce)

enable_blocked_clause_elimination: bool

Enable blocked clause elimination during preprocessing

enable_symmetry_breaking: bool

Enable symmetry breaking predicates

enable_inprocessing: bool

Enable inprocessing (periodic preprocessing during search)

inprocessing_interval: u64

Inprocessing interval (number of conflicts between inprocessing)

Implementations

impl SolverConfig

pub fn fast() -> Self

Create a configuration optimized for speed (minimal preprocessing) Best for easy problems or when quick results are needed

pub fn balanced() -> Self

Create a balanced configuration (default) Good balance between preprocessing and solving speed

pub fn thorough() -> Self

Create a configuration optimized for hard problems Uses aggressive preprocessing and symmetry breaking

pub fn minimal() -> Self

Create a minimal configuration (almost all features disabled) Useful for debugging or when you want full control

pub fn with_proof(self) -> Self

Enable proof generation

pub fn with_timeout(self, timeout_ms: u64) -> Self

Set timeout in milliseconds

pub fn with_max_conflicts(self, max_conflicts: u64) -> Self

Set maximum number of conflicts

pub fn with_max_decisions(self, max_decisions: u64) -> Self

Set maximum number of decisions

pub fn with_parallel(self, num_threads: usize) -> Self

Enable parallel solving

pub fn with_restart_strategy(self, strategy: RestartStrategy) -> Self

Set restart strategy

pub fn with_theory_mode(self, mode: TheoryMode) -> Self

Set theory mode

Trait Implementations

impl Clone for SolverConfig

fn clone(&self) -> SolverConfig

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for SolverConfig

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for SolverConfig

fn default() -> Self

Returns the “default value” for a type.