How to find solutions randomly (nondeterministically) in SAT4J?

Question

In the code examples from the SAT4J documentation, calling the solver multiple times on the same SAT problem always yields the same solution, even if multiple possible solutions exist - that is, the result is deterministic.

I'm looking for a way to get different solutions on multiple runs, that is, a nondeterministic/random result. For each possible solution, there should be a non-zero probability for the solution to be picked. Ideally, every solution should be picked with the same probability, but that's not a strict requirement.

I'm aware of the possibility to (deterministically) iterate over all solutions and just take a random one, but that's not a feasible solution in my case since there are too many solutions to begin with, and calculating them all takes too long.

Answer 1

Yes, Sat4j is by default deterministic: it will always find the same solution if you run it several times on the same problem from the command line.

The way to add some non determinism in the heuristics is to use the RandomWalkDecorator, as found for instance in the GreedySolver in org.sat4j.minisat.SolverFactory.

Note however that if you several times such solver from the command line :

java -jar org.sat4j.core.jar GreedySolver file.cnf

you will still be deterministic, since the pseudo random numbers generator is seeded by a constant.

Thus you need to ask several models within your Java code.

As mentioned in your question, you can use a ModelIterator decorator with a bound for that:

ISolver solver = SolverFactory.newGreedySolver();
ModelIterator mi = new ModelIterator(solver,10); // look for 10 models