Module varisat::glue

Compute glue levels of clauses.

The glue level of a propagating clause is the number of distinct decision levels of the clause's variables. This is also called the literal block distance (LBD). For each clause the smallest glue level observed is used as an indicator of how useful that clause is.

Functions

compute_glue

Compute the glue level of a clause.