This is an algorithm for enumerating the Top-k models of a CNF propositional formula. A Top-k model is defined as a model with less than k models preferred to it with respect to a preference relation. This algorithm is implemented on the top of the Minisat2.2 solver.

Any category    Data Mining