sat_solver::sat::solver

Trait SolverConfig

Source 
pub trait SolverConfig: Debug + Clone {
    type Assignment: Assignment;
    type VariableSelector: VariableSelection<Self::Literal>;
    type Literal: Literal;
    type LiteralStorage: LiteralStorage<Self::Literal>;
    type Restarter: Restarter;
    type Propagator: Propagator<Self::Literal, Self::LiteralStorage, Self::Assignment>;
    type ClauseManager: ClauseManagement;
}
Expand description

A trait that defines the configuration for a SAT solver.

This trait uses associated types to specify the concrete types for various components of a SAT solver. This allows for a highly generic Solver trait that can be instantiated with different underlying implementations for its parts.

Required Associated Types§

Source

type Assignment: Assignment

The type used for managing variable assignments (e.g. VecAssignment). Must implement crate::sat::assignment::Assignment.

Source

type VariableSelector: VariableSelection<Self::Literal>

The type used for the variable selection heuristic (e.g. Vsids, Random). Must implement crate::sat::variable_selection::VariableSelection.

Source

type Literal: Literal

The type used to represent literals (e.g. PackedLiteral, StructLiteral). Must implement crate::sat::literal::Literal.

Source

type LiteralStorage: LiteralStorage<Self::Literal>

The type used for storing literals within a clause (e.g. Vec<L>, SmallVec<[L; N]>). Must implement crate::sat::clause_storage::LiteralStorage.

Source

type Restarter: Restarter

The type used for the restart strategy (e.g. Luby, Geometric). Must implement crate::sat::restarter::Restarter.

Source

type Propagator: Propagator<Self::Literal, Self::LiteralStorage, Self::Assignment>

The type used for the unit propagation mechanism (e.g. WatchedLiterals, UnitSearch). Must implement crate::sat::propagation::Propagator.

Source

type ClauseManager: ClauseManagement

The type used for managing the clause database (e.g. LbdClauseManagement). Must implement crate::sat::clause_management::ClauseManagement.

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§