Skip to content

Bugfix/Collection/DPLL/Doc/Metrics: fix wrong calculation of required resolutions to eliminate a variable

dreinhar requested to merge dreinhar/autotool-fork-dreinhar:master into master

While eliminating all variables, for selecting the variable causing least resolutions you have to multiply the amount of negative and positive clauses. The wrong code squared the number of positive clauses. Hence the documentation, i. e. the experimental results, had to be altered too.

Merge request reports