Struct BiOptSat

pub struct BiOptSat<O, PBE = GeneralizedTotalizer, CE = Totalizer, ProofW = BufWriter<File>, OInit = DefaultInitializer, BCG = fn(Assignment) -> Clause>
where
    ProofW: Write,
{ /* private fields */ }

The BiOptSat algorithm type

Generics

• O: the SAT solver oracle
• PBE: pseudo-Boolean objective encoding
• CE: cardinality objective encoding
• ProofW: the proof writer
• OInit: the oracle initializer
• BCG: the blocking clause generator

Trait Implementations

impl<'learn, 'term, PBE, CE, ProofW, OInit, BCG> CoreBoost for BiOptSat<CaDiCaL<'learn, 'term>, PBE, CE, ProofW, OInit, BCG>

where ProofW: Write + 'static, (PBE, CE): MergeOllRef<PBE = PBE, CE = CE>, OInit: Initialize<CaDiCaL<'learn, 'term>>,

fn core_boost( &mut self, opts: CoreBoostingOptions, ) -> MaybeTerminatedError<bool>

Performs core boosting. Returns false if instance is unsat.

impl<O, PBE, CE, ProofW, OInit, BCG> ExtendedSolveStats for BiOptSat<O, PBE, CE, ProofW, OInit, BCG>

where O: SolveStats, ProofW: Write, PBE: EncodeStats, CE: EncodeStats,

fn oracle_stats(&self) -> SolverStats

Gets statistics from the internal oracle

fn encoding_stats(&self) -> Vec<EncodingStats>

Gets statistics from the objective encodings

impl<O, PBE, CE, ProofW, OInit, BCG> Init for BiOptSat<O, PBE, CE, ProofW, OInit, BCG>

where O: SolveIncremental + Interrupt + PhaseLit + LimitConflicts, ProofW: Write, PBE: BoundUpperIncremental + FromIterator<(Lit, usize)>, CE: BoundUpperIncremental + FromIterator<Lit>, OInit: Initialize<O>, BCG: Fn(Assignment) -> Clause,

fn new<Cls>( clauses: Cls, objs: Vec<Objective>, var_manager: VarManager, opts: KernelOptions, block_clause_gen: BCG, ) -> Result<Self>

where Cls: IntoIterator<Item = Clause>,

Initializes a default solver with a configured oracle and options. The oracle should not have any clauses loaded yet.

type Oracle = O

type BlockClauseGen = BCG

fn from_instance( inst: Instance, opts: KernelOptions, block_clause_gen: Self::BlockClauseGen, ) -> Result<Self>

Initialization of the algorithm using an Instance rather than iterators

impl<'term, 'learn, PBE, CE, ProofW, OInit, BCG> InitCert for BiOptSat<CaDiCaL<'term, 'learn>, PBE, CE, ProofW, OInit, BCG>

where ProofW: Write + 'static, PBE: BoundUpperIncremental + FromIterator<(Lit, usize)>, CE: BoundUpperIncremental + FromIterator<Lit>, OInit: Initialize<CaDiCaL<'term, 'learn>>, BCG: Fn(Assignment) -> Clause,

fn new_cert<Cls>( clauses: Cls, objs: Vec<Objective>, var_manager: VarManager, opts: KernelOptions, proof: Proof<Self::ProofWriter>, block_clause_gen: BCG, ) -> Result<Self>

where Cls: IntoIterator<Item = (Clause, AbsConstraintId)>,

Initializes a default solver with a configured oracle and options. The oracle should not have any clauses loaded yet.

type ProofWriter = ProofW

fn from_instance_cert( inst: Instance, opts: KernelOptions, proof: Proof<Self::ProofWriter>, block_clause_gen: <Self as Init>::BlockClauseGen, ) -> Result<Self>

Initialization of the algorithm using an Instance rather than iterators

impl<O, PBE, CE, ProofW, OInit, BCG> KernelFunctions for BiOptSat<O, PBE, CE, ProofW, OInit, BCG>

where ProofW: Write + Write, O: Interrupt,

fn pareto_front(&self) -> ParetoFront

Gets the Pareto front discovered so far

fn stats(&self) -> Stats

Gets tracked statistics from the solver

fn attach_logger<L: WriteSolverLog + 'static>(&mut self, logger: L)

Attaches a logger to the solver

fn detach_logger(&mut self) -> Option<Box<dyn WriteSolverLog>>

Detaches a logger from the solver

fn interrupter(&mut self) -> Interrupter

Gets an iterrupter to the solver

impl<'learn, 'term, ProofW, OInit, BCG> Solve for BiOptSat<CaDiCaL<'term, 'learn>, GeneralizedTotalizer, Totalizer, ProofW, OInit, BCG>

where BCG: Fn(Assignment) -> Clause, ProofW: Write + 'static,

fn solve(&mut self, limits: Limits) -> MaybeTerminatedError

Solves the instance under given limits. If not fully solved, returns an early termination reason.

fn all_stats(&self) -> (Stats, Option<SolverStats>, Option<Vec<EncodingStats>>)

Gets all statistics from the solver