Struct ResolutionResolver 

pub struct ResolutionResolver { /* private fields */ }

ConflictResolver which resolves conflicts according to the CDCL procedure.

This conflict resolver will derive a nogood that is implied by the constraints already present in the solver. This new nogood is added as a constraint to the solver, and the solver backtracks to the decision level at which the new constraint propagates.

The ResolutionResolver can be used in two AnalysisModes:

• AnalysisMode::OneUIP - Resolves until finding the unit implication point.
• AnalysisMode::AllDecision - Resolves until the learned nogood contains only decisions.

For an in-depth explanation and overview of CDCL and UIP, see [1].

Bibliography

[1] J. Marques-Silva, I. Lynce, and S. Malik, ‘Conflict-driven clause learning SAT solvers’, Handbook of satisfiability, pp. 131–153, 2009.

Implementations

impl ResolutionResolver

pub fn new(mode: AnalysisMode, should_minimise: bool) -> ResolutionResolver

Trait Implementations

impl Clone for ResolutionResolver

fn clone(&self) -> ResolutionResolver

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl ConflictResolver for ResolutionResolver

fn resolve_conflict(&mut self, context: &mut ConflictAnalysisContext<'_>)

Resolve a conflicting state in the solver so that search can proceed.

fn log_statistics(&self, statistic_logger: StatisticLogger)

Logs statistics of the conflict resolver using the provided StatisticLogger.

impl Debug for ResolutionResolver

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

Formats the value using the given formatter.

impl Default for ResolutionResolver

fn default() -> ResolutionResolver

Returns the “default value” for a type.