Struct TwoProduct 

pub struct TwoProduct<Sub = Pairwise> { /* private fields */ }

Implementations of the 2-product at-most-1 encoding.

References

• Jingchao Chen: A New SAT Encoding of the At-Most-One Constraint, ModRef 2010.

Trait Implementations

impl<Sub: Debug> Debug for TwoProduct<Sub>

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

Formats the value using the given formatter.

impl<Sub: Default> Default for TwoProduct<Sub>

fn default() -> TwoProduct<Sub>

Returns the “default value” for a type.

impl<'de, Sub> Deserialize<'de> for TwoProduct<Sub>

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl<Sub> Encode for TwoProduct<Sub>

where Sub: Encode + From<Vec<Lit>>,

fn n_lits(&self) -> usize

Gets the number of literals in the encoding

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

where Col: CollectClauses,

Encodes and enforces the at-most-1 constraint

impl<Sub> EncodeStats for TwoProduct<Sub>

fn n_clauses(&self) -> usize

Gets the number of clauses in the encoding

fn n_vars(&self) -> u32

Gets the number of auxiliary variables in the encoding

impl<Sub> Extend<Lit> for TwoProduct<Sub>

fn extend<T: IntoIterator<Item = Lit>>(&mut self, iter: T)

Extends a collection with the contents of an iterator.

fn extend_one(&mut self, item: A)

🔬This is a nightly-only experimental API. (extend_one)

Extends a collection with exactly one element.

fn extend_reserve(&mut self, additional: usize)

🔬This is a nightly-only experimental API. (extend_one)

Reserves capacity in a collection for the given number of additional elements.

impl<Sub> From<Vec<Lit>> for TwoProduct<Sub>

fn from(lits: Vec<Lit>) -> Self

Converts to this type from the input type.

impl<Sub> FromIterator<Lit> for TwoProduct<Sub>

fn from_iter<T: IntoIterator<Item = Lit>>(iter: T) -> Self

Creates a value from an iterator.

impl<Sub> IterInputs for TwoProduct<Sub>

type Iter<'a> = Copied<Iter<'a, Lit>> where Sub: 'a

The iterator type

fn iter(&self) -> Self::Iter<'_>

Gets an iterator over copies of the input literals

impl<Sub> Serialize for TwoProduct<Sub>

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.