pub struct MaxSatSolver { /* private fields */ }Expand description
Core-guided MaxSAT solver
Uses unsatisfiable cores to iteratively improve the solution. This is a basic implementation of the OLL (One-at-a-time Lower bounds Lifting) algorithm.
Implementations§
Source§impl MaxSatSolver
impl MaxSatSolver
Sourcepub fn new(config: MaxSatConfig) -> Self
pub fn new(config: MaxSatConfig) -> Self
Create a new MaxSAT solver
Sourcepub fn add_hard(&mut self, lits: impl IntoIterator<Item = Lit>)
pub fn add_hard(&mut self, lits: impl IntoIterator<Item = Lit>)
Add a hard clause
Sourcepub fn add_soft(&mut self, lits: impl IntoIterator<Item = Lit>, weight: Weight)
pub fn add_soft(&mut self, lits: impl IntoIterator<Item = Lit>, weight: Weight)
Add a soft clause with weight
Sourcepub fn solve_linear(&mut self) -> MaxSatResult
pub fn solve_linear(&mut self) -> MaxSatResult
Solve using linear search (simplest MaxSAT algorithm)
Iteratively adds constraints to forbid solutions with higher cost
Sourcepub fn solve(&mut self) -> MaxSatResult
pub fn solve(&mut self) -> MaxSatResult
Solve the MaxSAT instance
This is the main entry point - currently uses linear search
Sourcepub fn stats(&self) -> &MaxSatStats
pub fn stats(&self) -> &MaxSatStats
Get statistics
Sourcepub fn reset_stats(&mut self)
pub fn reset_stats(&mut self)
Reset statistics
Auto Trait Implementations§
impl Freeze for MaxSatSolver
impl RefUnwindSafe for MaxSatSolver
impl Send for MaxSatSolver
impl Sync for MaxSatSolver
impl Unpin for MaxSatSolver
impl UnsafeUnpin for MaxSatSolver
impl UnwindSafe for MaxSatSolver
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
Source§impl<T> Instrument for T
impl<T> Instrument for T
Source§fn instrument(self, span: Span) -> Instrumented<Self>
fn instrument(self, span: Span) -> Instrumented<Self>
Source§fn in_current_span(self) -> Instrumented<Self>
fn in_current_span(self) -> Instrumented<Self>
Source§impl<T> IntoEither for T
impl<T> IntoEither for T
Source§fn into_either(self, into_left: bool) -> Either<Self, Self>
fn into_either(self, into_left: bool) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left is true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read moreSource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left(&self) returns true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read more