Description

MTSS is a Multi-Threaded SAT Solver. It is designed for shared memory computers. The most interesting feature for the SAT community is the parallelization of existing SAT solvers. It introduces the rich / poor approach which is a general framework in which one a lot of SAT implementations can be parallelized. And MTSS introduces also the new parallel object called the guiding tree, which is an object used in parallel to distribute and balance the workload in the system.

Acknowledgements

ROMEO II, Centre de Calcul de Champagne-Ardenne. We ran benchmarks on this multi-threaded super computer, hosted in the University of Reims Champagne-Ardenne. All details on this computer are available here www.romeo2.fr (in french), technical details are here (in english).

User Guide

Available options for MTSS:
'-t n': launches n threads (by default, MTSS uses as many threads as many cores)
'-p n': launches n poor threads
'-l n': beyond this limit (in % of #vars), poor threads don't work (default: n=5% of #vars)
'-to s': time out, stops MTSS after s seconds (real time)
'-fh': forces the heuristic used (known heuristics: bsh_3sat, bsh_ksat, moms)
'-es config_file': poor and rich threads will launch an external solver according to a configuration file
'-ktf': keep temp files (option 'es' uses such files when no sharing, by default, MTSS remove them
'-h' or '--help': displays this help

Explanations about the 'es' option.
The configuration file must contain lines with a keyword and a value. The minimum keyword needed is the solver. You must write the keyword 'solver', space, then the absolute path to the external solver. For clause sharing, the keyword is 'share' and the values are 'ON' or 'OFF' and (option if you want to share clauses between external runs thanks to MTSS).
'#' at the beginning of a line is interpreted as a comment.


Examples:
Minisat launched by MTSS and clause sharing is activated (the '-mtss' option is required by minisat):
solver /home/vander/minisat/core/minisat_static
share ON

Kcnfs is launched by MTSS and clause sharing is not activated (by default the value 'OFF' is used for the keyword 'share'):
solver /home/vander/kcnfs/kcnfs

Links

This is the binary of MTSS compiled with gcc for an Intel Core i3 processor on a 64-bits GNU/Linux OS (Ubuntu 11.10). If you require an other version, please contact us (see contact page): MTSS

This is now the library you can use to easily share clauses between runs of a sequential SAT solver: mtss_share.c and mtss_share.h
An example of the use of this library is given in this version of Minisat: minisat_for_mtss.tar.gz

You can see changes we made in this version of Minisat by searching "MTSS - begin" in files. We also added mtss_share.c and mtss_share.h in "core" and "simp" directories (to compile, we had to add mtss_share.C as a symbolic link to mtss_share.c).

As a quick summary, the changes you have to do are these ones:
1 - Add an option to your SAT solver to understand if it is launched by MTSS or not
2 - Receive a guiding path from MTSS
3 - At each restart of the solver, before working on the search-tree, you have to propagate the literals in the guiding path (you can not see this modification in Minisat because we put the guiding path in the "assumptions" vector, which is designed for this task)
4 - Before each restart, you send learnt clauses to MTSS, then you receive shared clauses from MTSS