Stay organized with collections
Save and categorize content based on your preferences.
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.
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.
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().
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.
[[["Easy to understand","easyToUnderstand","thumb-up"],["Solved my problem","solvedMyProblem","thumb-up"],["Other","otherUp","thumb-up"]],[["Missing the information I need","missingTheInformationINeed","thumb-down"],["Too complicated / too many steps","tooComplicatedTooManySteps","thumb-down"],["Out of date","outOfDate","thumb-down"],["Samples / code issue","samplesCodeIssue","thumb-down"],["Other","otherDown","thumb-down"]],["Last updated 2024-08-06 UTC."],[[["The `StampingSimplifier` class implements a CNF simplification technique based on sampling a spanning tree from the binary implication graph."],["This simplification process uses the implications encoded in the tree to perform subsumption and strengthening of clauses."],["While it considers chains of implications, it may only capture a fraction of the full implication graph due to the tree sampling."],["The spanning tree is randomized on each call, potentially benefiting from prior transitive reduction of the implication graph."],["The `StampingSimplifier` includes methods like `ComputeStamps`, `DoOneRound`, and `ProcessClauses` to carry out the simplification process."]]],["The `StampingSimplifier` class implements a \"stamping\" technique for CNF simplification. It samples an implications graph with a randomized spanning tree to simplify clauses through subsumption and strengthening, enabling the consideration of implication chains. Key actions include `ComputeStamps` to assess reachability and detect failed literals, `ComputeStampsForNextRound` to handle fixed variables, and `DoOneRound` to perform a full simplification round. Other methods are available for clause processing, sampling, and testing.\n"]]
