SAT Gory details

Carsten released the descriptions of the solvers that compete in the SAT Race 2008.

I was surprized by the description of ManySAT by Youssef Hamadi from Microsoft.

They are basically running several solvers in parallel, and stop as soon as one solver stops. There is some learned clause sharing between the solvers, but there is not much details on the description.

During the qualifications, such approach ended up to be the best one in the parallel track.

The final results will only be published next week but I would like to have your opinion about that use of multi-core machines for improved SAT solving.

It took me a few hours this morning to implement a similar approach in SAT4J: here are some pieces of code to show you how it works

public class ManyCore implements ISolver, OutcomeListener {
 
	/**
	 * 
	 */
	private static final long serialVersionUID = 1L;
 
	private String[] availableSolvers; // = { };
 
	private ISolver[] solvers;
	private int numberOfSolvers;
	private int winnerId;
	private boolean needToWait;
	private boolean resultFound;
	private int remainingSolvers;
 
	public ManyCore(ASolverFactory<? extends ISolver> factory, String ... solverNames) {
		availableSolvers = solverNames;
		Runtime runtime = Runtime.getRuntime();
		long memory = runtime.maxMemory();
		int numberOfCores = runtime.availableProcessors();
		if (memory > 1000000000L) {
			numberOfSolvers = numberOfCores;
		} else {
			numberOfSolvers = 1;
		}
		if (solverNames.length<numberOfSolvers) {
			throw new IllegalArgumentException("I need more solver names to run ManyCore on such computer!");
		}
		solvers = new ISolver[numberOfSolvers];
		for (int i = 0; i < numberOfSolvers; i++) {
			solvers[i] = factory.createSolverByName(
					availableSolvers[i]);
		}
	}
 
       [...]
	@Override
	public IConstr addClause(IVecInt literals) throws ContradictionException {
		for (int i = 0; i < numberOfSolvers; i++) {
			solvers[i].addClause(literals);
		}
		return null;
	}
 
        [...]
 
        	@Override
	public boolean isSatisfiable() throws TimeoutException {
		remainingSolvers = numberOfSolvers;
		needToWait = true;
		for (int i = 0; i < numberOfSolvers; i++) {
			new Thread(new RunnableSolver(i, solvers[i], this)).start();
		}
		try {
			do {
				Thread.sleep(1000);
			} while (needToWait && remainingSolvers > 0);
		} catch (InterruptedException e) {
			// TODO: handle exception
		}
		if (remainingSolvers == 0) {
			throw new TimeoutException();
		}
		return resultFound;
	}
 
        [...]
 
	@Override
	public synchronized void onFinishWithAnswer(boolean finished,
			boolean result, int index) {
		if (finished) {
			winnerId = index;
			resultFound = result;
			for (int i = 0; i < numberOfSolvers; i++) {
				if (i != winnerId)
					solvers[i].expireTimeout();
			}
                        System.out.println("c And the winner is "+availableSolvers[winnerId]);
			needToWait = false;
		} else {
			remainingSolvers--;
		}
	}
 
}
 
interface OutcomeListener {
	void onFinishWithAnswer(boolean finished, boolean result, int index);
}
 
class RunnableSolver implements Runnable {
 
	private final int index;
	private final ISolver solver;
	private final OutcomeListener ol;
 
	public RunnableSolver(int i, ISolver solver, OutcomeListener ol) {
		index = i;
		this.solver = solver;
		this.ol = ol;
	}
 
	@Override
	public void run() {
		try {
			boolean result = solver.isSatisfiable();
			ol.onFinishWithAnswer(true, result, index);
		} catch (TimeoutException e) {
			ol.onFinishWithAnswer(false, false, index);
		}
	}
 
}

The solver can be setup with any SolverFactory, using simply the names of the solvers. Here is an example of setup for up to 4 processors.

	public static ISolver newManyCore() {
		return new ManyCore(org.sat4j.minisat.SolverFactory.instance(),"Default","MiniLearningHeapEZSimpNoRestarts","MiniLearningHeapExpSimp","MiniLearningHeapRsatExpSimp");
	}

There is no clause sharing for the moment, and on a few examples, it looks like paying off. Since I have now a 4 cores computer in my office, I am likely to play a bit with such approach in the next week.

Such approach might be good for some practical applications. Your feedback is welcome.

Carsten released today the results of Q2 qualification phases.

SAT4J is the last solver qualified with 20 benchmarks out of 50 solved within a 20mn timeout on the SAT Race Computer.

Two years ago, the limit was the same but SAT4J was able to solve 30 out of 50 benchmarks (the benchmarks were not the same).

It looks like this year, the use of a preprocessor is very important. Many of the solvers qualified are using a preprocessor (SatELite or Minisat 2 integrated simplifier or their own).

I launched SAT4J both with and without SatELite on the qualification benchmarks with 20mn timeout, 900MB of allowed RAM:

• without preprocessor, SAT4J solved 19 benchmarks (20 during Q2, our cluster is slower than Carsten’s one)
• with preprocessor, SAT4J solved 28 benchmarks

I haven’t decided yet if I will submit SAT4J with SatELite for the race. I submit SAT4J to the race in order for SAT4J users or potential users to have an idea of the kind of performances they can expect from SAT4J. Using SatELite in front of it would biased the results.

However, if using SatELite makes such a difference, why not using it?

I think it would be nice to know clearly which solvers use a preprocessor.

You liked the head-tail data structure? You loved the 2-watched literal scheme? Here is a nice challenge from Roberto Sebastiani

SAT solvers are currently used as boolean enumerators inside SMT solvers. The theory solver listen to events such as boolean propagation and backtrack.

SAT solvers based on a lazy data structure such as the watched literals are not aware of the number of satisfied clauses. As such, they only stop when all the variables are set to a truth value.

If it is not a big deal for SAT, it is one in SMT, due to the sometimes heavy cost of boolean propagation in the theory.

The SMT community is thus looking for a way to prevent non necessary assignments:

• no longer assign values when all the clauses are satisfied
• do not assign values to variables appearing only in satisfied clauses

If the impact might not be that big for classical SAT solvers, it might be useful for some applications that need to work on partial assignments (implicants) instead of full assignments (models).

Have fun!

I am currently wondering which SAT solver people are using right now.

From what I can see around me, I would say that:
- SAT solvers developers are using their own
- Many persons are using Chaff since it is for sure the most famous SAT solver around.
- In 2003/2005, many persons were using Siege V4, because it was the fastest solver around.
- Since 2003, a growing number of people is using Minisat, because it is not too complicated to understand, can be easily tailored for its own use, it is really fast on most benchmarks, and it is open source.
- Some people just move to the SAT competition/Race winners each year.
- Some others do choose their SAT solver because of the language used (C/C++/C#/Java…).

But I might be completely wrong

What is your own feeling about this?

[update 1] The license used to distribute the software is also one reason of the choice of the solver.
One user reported to not use Chaff/Berkmin/Siege because of their licenses.

The same user also reports to use BDD packages in parallel to SAT solvers.

[update 2] I added a poll to let people vote for their preferred solver. Let me know if yours is missing.

[update 3] number of google hits for “solvername SAT solver” on February 1, 2008.

• GRASP: 9600
• Chaff : 9230
• SATO: 3770
• Siege: 2200
• SATZ: 1750
• Minisat 1560
• RELSAT: 712
• SAT4J: 658
• KCNFS: 198
• RSAT: 141
• Picosat: 117
• OKlibrary: 10

Asking for “March SAT solver” provides 25000 answers because of March being matched with the month.

Hi all,

as I recently (finally…) became a Debian Developer I now could easily package several SAT solvers and have them integrated with Debian. For those of us using Debian (or Ubuntu) this would greatly simplify the installation of the solvers. However, as you might know, Debian requires proper and free licensing. As such I need to check the licenses of the solvers to see whether this is possible at all.

However, first of all, I’d like to know whether people have any objections against doing this.

Best,

Michael

One of the decision that we will need to take for the next competitions is to jump or not to 64 bits architecture.

This year, I tried to compile the solvers for the 64 bits architecture: many of them were no longer working.

Current computer sold are multi-core 64 bits processors, so the number of SAT solver designers having access to a 64 bits computer is growing.

The main advantage of using native 64 bits solvers is to use the full power of the underlying computers.

The main disadvantage of using 64 bits computer is that the program uses more memory since integers are now 64 bits big, that’s also true for pointers.
As a consequence, given the same amount of main memory (2 GB for instance), the same solver compiled in 64 bits might run out of memory while the same solver compiled in 32 bits just work fine.

This is especially an issue for the industrial category where the benchmarks are big.

I am especially interested in the feedback of solver designers that already jumped to the 64 bits architecture.

–Daniel

The source code of the SAT solvers participating to the SAT competition 2007, competition division, is now available from the SAT Competition Web site.

It is available as a single 10 6MB large archive.

That code should compile fine on any linux system. Please post a comment here if you experience some problems when compiling those solvers.

Note that the “-m32″ flag was used to compile the solvers for a 32 bits architecture. Owners of 64 bits computers might want to remove it. Note that some solvers simply won’t work on a 64 architecture.

[Update] The sample CNF files contained in the initial archive have been removed.

[Update2 (11/7/2007)] Missing rsat.sh script added in the archive.

Armin also mentioned in his presentation that the way the watched literals are implemented matters.

The implementation of watched literals with a fixed place for the two watched literals on top of the clause is really easy to implement. I use the implementation of the very first version of Minisat. The only change is that I discarded the test to see if the first watched literal is satisfied. In practice, ignoring that test makes usually the solver solve more benchmarks. (On the 100 SAT Race 2006 Benchmarks, using the Luby 512 configuration with all options enabled, enabling the test allows the solver to solve 57 (28 SAT/ 29 UNSAT) benchs in 807mn against 61 (29 SAT/ 31 UNSAT) in 788mn without).

Each clause is added in a list maintained for each literal, that need to be updated each time the watched literals are changing.

I know that in C/C++, a representation based on pointer arithmetics is possible. I cannot use it in Java

What is your experience on the subject?

More precisely, I would like to know if anybody has tried to implement the list of watched clauses the mchaff/picosat way and if it really pays off.

After taking a look at Armin’s invited talk slides at the SAT 07 conference, I decided to give a try to the rapid restart strategy mentioned by Armin.
Read the rest of this entry »