C++ Reference: class StampingSimplifier

This documentation is automatically generated.

Implements "stamping" as described in "Efficient CNF Simplification based on Binary Implication Graphs", Marijn Heule, Matti Jarvisalo and Armin Biere.

This sample the implications graph with a spanning tree, and then simplify all clauses (subsumption / strengthening) using the implications encoded in this tree. So this allows to consider chain of implications instead of just direct ones, but depending on the problem, only a small fraction of the implication graph will be captured by the tree.

Note that we randomize the spanning tree at each call. This can benefit by having the implication graph be transitively reduced before.
Method
ComputeStamps

Return type: bool

Using a DFS visiting order, we can answer reachability query in O(1) on a tree, this is well known. ComputeStamps() also detect failed literal in the tree and fix them. It can return false on UNSAT.

ComputeStampsForNextRound

Return type: bool

Arguments: bool log_info

When we compute stamps, we might detect fixed variable (via failed literal probing in the implication graph). So it might make sense to do that until we have dealt with all fixed literals before calling DoOneRound().

DoOneRound

Return type: bool

Arguments: bool log_info

This is "fast" (linear scan + sort of all clauses) so we always complete the full round. TODO(user): To save one scan over all the clauses, we could do the fixed and equivalence variable cleaning here too.

ImplicationIsInTree

Return type: bool

Arguments: Literal a, Literal b

ProcessClauses

Return type: bool

SampleTreeAndFillParent

Return type: void

Visible for testing.

StampingSimplifier

Return type: explicit

Arguments: Model* model