During his invited talk at the SAT conference, Moshe Vardi made the point that the SAT competition might harm the SAT community in the long term because the part of the community interested in practical aspects of SAT solving roughly reached monoculture.
It is true that since the first SAT competition in 2002, the diversity of SAT solvers is reduced: 4 CDCL solvers only in 2002 while nowadays around 2/3 of the solvers, and basically all the ones tailored for application benchmarks, are CDCL ones.
Moshes Vardi claims that researchers are currently focusing on an approach known to work well currently but might miss to build the approach that will work well in the future. His main point was that CDCL solvers are still based on the resolution proof system while more powerful proof systems exists (e.g. extended resolution, cutting planes, etc).
Replacing resolution inference by cutting planes has already been investigated by various researchers (Chai and Kuellmann in Galena, Heidi Dixon in PBChaff, Sheini and Sakalah in Pueblo, etc) but the results are currently not convincing: see e.g. SAT4J at the Pseudo Boolean evaluation: the resolution proof system based one (SAT4J Pseudo Resolution) performs globally better than the cutting planes proof system based one (SAT4J Pseudo Cutting Planes).
In my opinion, there are pretty positive consequences of the SAT competition that make the SAT competition a good thing for the SAT community:
- The competition is supported by the community: with about 50 SAT solvers from about 30 teams from all over the world each time, it is a widely adopted event in the SAT community.
- The competition emphasize state-of-the-art solvers regularly: it is easy for anybody willing to evaluate SAT technology to grab a recent efficient solver an give it a try.
- The competition spreads coding tricks and algorithmic improvements among solvers designers: by forcing competitors to release the source code of their solvers for research purposes, technical details that are not found in scientific papers are available to anybody willing to dive into those details.
- Maybe even more important: the SAT competition allowed the availability of many robust, efficient, easy to embed SAT solvers that allowed people outside the SAT community to find new use of SAT technology. SAT solvers moved from proof of concept software to highly reliable and carefully designed software.
Regarding monoculture, the competition has several categories that allow various kind of SAT solvers to be awarded. The competition also tried to point out singular solvers (Allen van Gelder’s purse score). We are open to any suggestions that could favor the emergence of new generations of SAT solvers.
The results of the SAT competition have been released last week..
It looks like many of the top solvers in the application are using dynamic restarts:
Restarts strategies have been a hot topic in the community recently and this is likely to continue in the future.
The results of the MAX SAT Evaluation 2008 are available online.
What’s new this year?
Compared to the other years, there is now a distinction between random,crafted and industrial maxsat instances, as it is done for SAT.
The distinction betwen Random and Crafted instances is not really clear (should MAXCUT/RANDOM be really classified as crafted instances instead of Random?).
On my side, the good news is that SAT4J MAXSAT provided some reasonable results on a few classes of benchmarks (especially in the partial max sat industrial category).
For those following the MAXSAT evaluation, you might wonder what makes the worst solver of the 2006 and 2007 evaluations perform better this year.
There are two main changes this year:
- the pseudo boolean solver used behind SAT4J MAXSAT is no longer based on cutting planes but on resolution (as in Satzoo, PBS, etc).
- The encoding into SAT does not add extra variables if a binate covering problem is recognized, i.e. when the only soft constraints are unit.
Furthermore, since we have for the first time “real” problems in the maxsat evaluation, approaches based on a CDCL solver have more chances to show up.
Taking into account the fact that the SAT solver in SAT4J finished last during the SAT Race 2008 
, my guess is that the approach used in SAT4J Maxsat is quite competitive with the other techniques on industrial partial [weighted] max sat problems.
While reading Minisat 2.1 description, I noticed the interesting discussion on “blocking literals” that is used in that new version of Minisat to manage the cases where clauses are satisfied by one of the watched literal.
Since the very first versions of SAT4J, I commented out the code corresponding to the management of satisfied clauses in Minisat: it is often the case that the solver performs better if the other watched literal is updated.
How are you taking into account a satisfied watched literal in your solver?
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
Loading ...