Allow computing all MUSes using two calls to the SAT solver
Sat4j can currently compute one MUS. It is possible to compute all MUSes using two calls to a SAT solver: the first one to detect all P-prime M-implicant of the formula (see my ECAI 96 paper or my PhD - in french- for details), the second one to compute a minimal hitting set (here it is mandatory to compute prime implicants).
The main issue will be to perform the second step: the first one can be performed by applying MAXSAT SAT several times, and preventing the same solutions to appear by adding blocking clauses.