Struct DynamicPolyWatchdogCell 

pub struct DynamicPolyWatchdogCell<'totdb> { /* private fields */ }

Dynamic polynomial watchdog structure with a RefCell to a totalizer database rather than owning it.

References

• [1] Tobias Paxian and Sven Reimer and Bernd Becker: Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT, SAT 2018.

Implementations

impl<'totdb> DynamicPolyWatchdogCell<'totdb>

pub fn new( structure: &'totdb Structure, db: &'totdb RefCell<&'totdb mut Db>, ) -> Self

Constructs a new DPW encoding referencing a totalizer database

pub fn depth(&self) -> usize

Gets the maximum depth of the tree

Trait Implementations

impl BoundUpper for DynamicPolyWatchdogCell<'_>

fn encode_ub<Col, R>( &mut self, range: R, collector: &mut Col, var_manager: &mut dyn ManageVars, ) -> Result<(), OutOfMemory>

where Col: CollectClauses, R: RangeBounds<usize>,

Lazily builds the pseudo-boolean encoding to enable upper bounds within a given range. var_manager is the variable manager to use for tracking new variables. A specific encoding might ignore the upper or lower end of the range.

fn enforce_ub(&self, ub: usize) -> Result<Vec<Lit>, EnforceError>

Returns assumptions/units for enforcing an upper bound (weighted sum of lits <= ub). Make sure that BoundUpper::encode_ub has been called adequately and nothing has been called afterwards.

fn coarse_ub(&self, ub: usize) -> usize

Gets the next smaller upper bound value that can be easily encoded. This is used for coarse convergence, e.g., with the DynamicPolyWatchdog encoding.

impl BoundUpperIncremental for DynamicPolyWatchdogCell<'_>

fn encode_ub_change<Col, R>( &mut self, range: R, collector: &mut Col, var_manager: &mut dyn ManageVars, ) -> Result<(), OutOfMemory>

where Col: CollectClauses, R: RangeBounds<usize>,

Lazily builds the change in pseudo-boolean encoding to enable upper bounds from within the range. A change might be added literals or changed bounds. var_manager is the variable manager to use for tracking new variables. A specific encoding might ignore the lower or upper end of the range.

impl<'totdb> Debug for DynamicPolyWatchdogCell<'totdb>

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

Formats the value using the given formatter.

impl Encode for DynamicPolyWatchdogCell<'_>

fn weight_sum(&self) -> usize

Get the sum of weights in the encoding

fn next_higher(&self, val: usize) -> usize

Gets the next higher value possible to be achieved by the weighted sum. Might simply return val + 1 if no stronger value can be inferred.

fn next_lower(&self, val: usize) -> usize

Gets the next lower value possible to be achieved by the weighted sum. Might simply return val - 1 if no stronger value can be inferred.

impl EncodeIncremental for DynamicPolyWatchdogCell<'_>

fn reserve(&mut self, var_manager: &mut dyn ManageVars)

Reserves all variables this encoding might need