(Indifferent) Unit and Pure Literals

[SSoelvsten]

For QBF solving, it is useful to discern a literal is unit or pure since these can immediately be removed with a bdd_restrict instead of using the more expensive bdd_exists or bdd_forall. This decreases the BDD size considerably, thereby speeding up computation.

Unit Literals

For BDDs, we may use the more general concept of an indifferent unit literal (IUL) [working title] which are all of the variables that can be restricted without changing the result with respect to bdd_exists:

The variable x is a positive IUL to the BDD f, if all BDD nodes n in f with n.label() = x has n.low() point to the false terminal. Similarly, x is a negative IUL if all n.label() = x has n.high() point to the false terminal.

• Add bdd_isunit(f, x, positive) which returns true if x is an IUL in f. If positive is true, then one checks for x being a positive IUL. Otherwise, one checks for x being a negative one.
• Add bdd_isunit(f, x) where positive is put into the signedness of x.
• Add bdd_units(f, c) which calls the consumer function c with pairs (x, positive) for all IULs in f.
• Add bdd_units(f, c) which calls the consumer function c with x and positive is encoded into its signedness.

Pure Literals

Similarly, one can also identify indifferent pure literals (IPL) [working title] that can be restricted away without changing the result of bdd_forall:

Dually to IUL, x is a positive IPL if all n.low() = true and x is a negative IPL if all n.high() == true.

• Add bdd_ispure(f, x, positive) which returns true if x is an IPL in f. If positive is true, then one checks for x being a positive IUL. Otherwise, one checks for x being a negative one.
• Add bdd_ispure(f, x) where positive is put into the signedness of x.
• Add bdd_pures(f, c) which calls the consumer function c with pairs (x, positive) for all IPLs in f.
• Add bdd_pures(f, c) which calls the consumer function c with x and positive encoded into x's signedness.

All of these functions can be implemented as O(N/B) single-scan algorithms. Both functions can terminate after reaching a variable y > x. The predicates can also make use of fail-fast.

All functions should of course be unit tested.

Additional Context

This idea was identified by Louise Bonderup Dohn while working on her Master's thesis.