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.


Authors :
Lakhdar Saïs
Yakoub Salhi
Saïd Jabbour
Karim Tabia

Any category    Data Mining   

Go to the software webpage