3

I found a way to finding all the solutions using the way described in this link.

This is working fine, but it is slow. As it recalculates the constraints from the start i_e doesn't take advantage of the previous computations.

Now, I saw in this link, that there is a more efficient way to find all the solutions using MiniSat as library. But the way is not described there.

Can you point me to right documentation for finding all the SAT solutions efficiently?

Thanks.

Gaurav Singh
  • 31
  • 1

1 Answers1

4

A more efficient method of finding all SAT solutions is described in the paper ("All-SAT using Minimal Blocking Clauses") by Yu, Subramanyan, Tsiskaridze and Malik.

The basic strategy of iteratively finding solutions and adding blocking clauses is the same, but the blocking clauses are generated using a novel idea, which reduces their size. The blocking clauses produced are smaller than the usual naive partial assignments and therefore encompass more satisfying assignments per iteration, speeding the enumeration process.

As far as I know, there is no public implementation of the ideas contained in this paper that you can download and run.

Kyle Jones
  • 5,492
  • 1
  • 21
  • 30