Iteration through all possible solutions didn't find all possible solutions
Hello, I downloaded a dimacs translation of the Linux kernel 2.6.33 (http://formulas.linux-variability-analysis-tools.googlecode.com/hg/2.6.33.3-2var.dimacs, I removed the 2 blank lines at the end of the file). And tried it to reason it with Sat4j 2.3.4 (http://forge.ow2.org/project/download.php?group_id=228&file_id=19075). I tried 2 different possibilities to iterate through all possible solutions:
- With a loop over problem.isSatisfiable() (c.f. http://www.sat4j.org/howto.php#models).
- With the ModelIterator (c.f http://www.sat4j.org/maven21/org.sat4j.core/apidocs/org/sat4j/tools/ModelIterator.html). I saved all found solutions to my hard disk and compared each other with a diff tool. Only the first 6 solutions are different, all other models are equal to the 6st solution. I tried also another possibility; iterating through all variables and adding a constraint to the complete model, that this variable must be true. Excerpt from my code:
Reader reader = new DimacsReader(solver);
for (int i = 1; i <= problem.nVars(); i++) {
int[] varAssignment = {i};
int configNo = 0;
List<int[]> foundSolutions = new ArrayList<int[]>();
try {
solver.addClause(new VecInt(varAssignment));
if(solver.isSatisfiable()) {
System.out.println("Created Configuration No. " + configNo);
int[] newModel = problem.model();
if (!compareSolutions(foundSolutions, newModel)) {
saveModel(folder, configNo);
foundSolutions.add(newModel);
configNo++;
}
}
} catch (ContradictionException e) {
System.out.println("Empty clause added. This model will be skipped.");
}
reader.parseInstance(filename); // Reset model
}
The third options find more than 6 different solutions. Can anybody explain my why the documented iterators only find 6 solutions? I guess this is a bug, or did I used sat4J wrong?
Best regards, Sascha El-Sharkawy