Function varisat::analyze_conflict::minimize_clause

fn minimize_clause<'a>(
    ctx: Const<TrailP, Const<ProofP<'a>, Const<ImplGraphP, Const<ClauseAllocP, Mut<VsidsP, Mut<AnalyzeConflictP, Ref<Context<'a>>>>>>>>
)

Performs recursive clause minimization.

Note: Requires AnalyzeConflict's var_flags to be set for exactly the variables of the unminimized claused. This also sets some more var_flags, but lists them in to_clean.

This routine tries to remove some redundant literals of the learned clause. The idea is to detect literals of the learned clause that are already implied by other literals of the clause.

This is done by performing a DFS in the implication graph (following edges in reverse) for each literal (apart from the asserting one). The search doesn't expand literals already known to be implied by literals of the clause. When a decision literal that is not in the clause is found, it means that the literal is not redundant.

There are two optimizations used here: The first one is to stop the search as soon as a literal of a decision level not present in the clause is found. If the DFS would be continued it would at some point reach the decision of that level. That decision belongs to a level not in the clause and thus itself can't be in the clause. Checking whether the decision level is among the clause's decision levels is done approximately using a Bloom filter.

The other optimization is to avoid duplicating work during the DFS searches. When one literal is found to be redundant that means the whole search stayed within the implied literals. We remember this and will not expand any of these literals for the following DFS searches.

In this implementation the var_flags array here has two purposes. At the beginning it is set for all the literals of the clause. It is also used to mark the literals visited during the DFS. This allows us to combine the already-visited-check with the literal-present-in-clause check. It also allows for a neat implementation of the second optimization. When the search finds the literal to be non-redundant, we clear var_flags for the literals we visited, resetting it to the state at the beginning of the DFS. When the literal was redundant we keep it as is. This means the following DFS will not expand these literals.