Utilise (counter-)model counts for stable models

[ellmau]

Is your feature request related to a problem? Please describe.
The currently implemented naive approach to lazily evaluated and filtered iterators over all possible two-valued interpretations is not smart and performant enough.

Describe the solution you'd like
Using the counts of (counter-)models might allow one to reduce the search space, by following these steps:

• choose the smallest count of still undecided statements
• follow the paths to the count-defined outcome (i.e. model vs counter-model)
  • Filter impossible interpretations on the fly (e.g. model-path for the statement is followed implies that only hi-child nodes of the said statement need to be followed)
• restrict the other acceptance conditions according to partial interpretation based on the path
• repeat till all statements are set
• check for stability
• when all paths are explored, the statement-variable of the bdd can be set to the inverse truth-value without further checking.

Describe alternatives you've considered

• A limit, where the approach is substituted by a brute-force approach
• A similar approach with facet-counts