#include <sat_inprocessing.h>

Public Member Functions
	StampingSimplifier (Model *model)

bool	DoOneRound (bool log_info)

bool	ComputeStampsForNextRound (bool log_info)

void	SampleTreeAndFillParent ()
	Visible for testing.

bool	ComputeStamps ()

bool	ImplicationIsInTree (Literal a, Literal b) const

bool	ProcessClauses ()

Detailed Description

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: we randomize the spanning tree at each call. This can benefit by having the implication graph be transitively reduced before.

Definition at line 195 of file sat_inprocessing.h.

Constructor & Destructor Documentation

◆ StampingSimplifier()

operations_research::sat::StampingSimplifier::StampingSimplifier ( Model * model )

inlineexplicit

Definition at line 197 of file sat_inprocessing.h.

Member Function Documentation

◆ ComputeStamps()

bool operations_research::sat::StampingSimplifier::ComputeStamps ( )

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.

Compute sizes.

Compute starts in the children_ vector for each node.

Fill children. This messes up starts_.

Reset starts to correct value.

Perform a DFS from each root to compute the stamps.

Failed literal detection. If the negation of top is in the same tree, we can fix the LCA of top and its negation to false.

Find the LCA.

Definition at line 748 of file sat_inprocessing.cc.

◆ ComputeStampsForNextRound()

bool operations_research::sat::StampingSimplifier::ComputeStampsForNextRound ( 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().

Todo: (user): compute some dtime, it is always zero currently.

Definition at line 690 of file sat_inprocessing.cc.

◆ DoOneRound()

bool operations_research::sat::StampingSimplifier::DoOneRound ( 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.

We need a DAG so that we don't have cycle while we sample the tree.

Todo: (user): We could probably deal with it if needed so that we don't need to do equivalence detection each time we want to run this.

Note: num_removed_literals_ do not count the literals of the subsumed clauses.

Definition at line 655 of file sat_inprocessing.cc.

◆ ImplicationIsInTree()

bool operations_research::sat::StampingSimplifier::ImplicationIsInTree	(	Literal	a,
		Literal	b ) const

inline

Definition at line 223 of file sat_inprocessing.h.

◆ ProcessClauses()

bool operations_research::sat::StampingSimplifier::ProcessClauses ( )

Note: we might fix literal as we perform the loop here, so we do need to deal with them.

For a and b in the clause, if not(a) => b is present, then the clause is subsumed. If a => b, then a can be removed, and if not(a) => not(b) then b can be removed. Nothing can be done if a => not(b).

The sort should be dominant.

We found an implication: top_entry => this entry.

Failed literal?

not(span[i]) => span[i] so span[i] true. And the clause is satisfied (so we count as as subsumed).

span[i] => not(span[i]) so span[i] false.

not(a) => b : subsumption. a => not(b), we cannot deduce anything, but it might make sense to see if not(b) implies anything instead of just keeping top_entry. See

Todo: below.

not(a) => not(b), we can remove b.

a => b, we can remove a.

Todo: (user): Note that it is okay to still use top_entry, but we might miss the removal of b if b => c. Also the paper do things differently. Make sure we don't miss any simplification opportunites by not changing top_entry. Same in the other branches.

Strengthen the clause.

Definition at line 833 of file sat_inprocessing.cc.

◆ SampleTreeAndFillParent()

void operations_research::sat::StampingSimplifier::SampleTreeAndFillParent ( )

Visible for testing.

Todo: (user): Better algo to not select redundant parent.

Todo: (user): if parents_[x] = y, try not to have parents_[not(y)] = not(x) because this is not as useful for the simplification power.

Todo: (user): More generally, we could sample a parent while probing so that we consider all hyper binary implications (in the case we don't add them to the implication graph already).

We look for a random lit that implies i. For that we take a random literal in the direct implications of not(i) and reverse it.

We found an interesting parent.

Definition at line 713 of file sat_inprocessing.cc.

The documentation for this class was generated from the following files:

ortools/sat/sat_inprocessing.h
ortools/sat/sat_inprocessing.cc

Public Member Functions