C++ Reference: class StampingSimplifier

Note: 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