Struct satoxid::constraints::ExactlyK

pub struct ExactlyK<I> {
    pub lits: I,
    pub k: u32,
}

This constraint encodes the requirement that exactly k of lits are true.

Example

let constraint = ExactlyK {
    k: 2,
    lits: vec!["a", "b", "c", "d"].into_iter(),
};

encoder.add_constraint(constraint);

let model = encoder.solve().unwrap();
let true_lits = model.vars().filter(|l| l.is_pos()).count();
assert!(true_lits == 2);

Fields

lits: I

k: u32

Trait Implementations

impl<I: Clone> Clone for ExactlyK<I>

fn clone(&self) -> ExactlyK<I>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<V, I> Constraint<V> for ExactlyK<I> where
    V: SatVar,
    I: Iterator + Clone,
    I::Item: Into<VarType<V>> + Debug, 

fn encode<S: Backend>(self, solver: &mut S, varmap: &mut VarMap<V>)

Encode Self as an constraint using solver.

impl<V, I> ConstraintRepr<V> for ExactlyK<I> where
    V: SatVar,
    I: Iterator + Clone,
    I::Item: Into<VarType<V>> + Debug, 

fn encode_constraint_implies_repr<S: Backend>(
    self,
    repr: Option<i32>,
    solver: &mut S,
    varmap: &mut VarMap<V>
) -> i32

Encode if Self is satisified, that repr is true. Otherwise repr is not constrained and can be true or false.

fn encode_constraint_equals_repr<S: Backend>(
    self,
    repr: Option<i32>,
    solver: &mut S,
    varmap: &mut VarMap<V>
) -> i32

Encode if and only if Self is satisified, that repr is true.

fn encode_constraint_repr_cheap<B: Backend>(
    self,
    repr: Option<i32>,
    backend: &mut B,
    varmap: &mut VarMap<V>
) -> i32

Encode that repr is true if the constraint is satisfied. The implementation can decide if it has the semantics of encode_constraint_implies_repr or encode_constraint_equals_repr, depending on what is cheaper to encode.

impl<I> Debug for ExactlyK<I> where
    I: Iterator + Clone,
    I::Item: Debug, 

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

Formats the value using the given formatter.