Module sat_decision 

Semantic SAT encoding decisions. Clauses and solver literals belong to the adaptor.

Structs

EncodingSelection

A resolved algorithm and the source of that choice, reusable across encoding classes.

PbTermGroup

A contiguous group of weighted terms with an existing representation invariant.

SatIntegerView

A numeric view whose representation constraints remain independently enforced.

Enums

AllDifferentEncoding

Library compositions available for allDifferent.

AmoEncoding

Library algorithms available for asserted and reified at-most-one constraints.

CardinalityEncoding

Provider and algorithm for a cardinality constraint.

CardinalityRelation

Bound direction for a semantic cardinality constraint.

ElementEncoding

Library compositions available for element.

IntegerRelation

Numeric relation between a weighted integer view and its bound.

PbEncoding

Provider and algorithm for signed weighted pseudo-Boolean constraints.

PbTermStructure

Representation structure available to a pseudo-Boolean encoder.

SatEncodingDecision

A Boolean operation whose truth is asserted or bound to a named output.

SelectionProvenance

The origin of a resolved compilation choice.

TableEncoding

Library compositions available for table.