ALGOS Logo
PMSat

PMSat

PMSat is a parallel SAT-solver that uses MiniSAT as engine. MiniSAT was chose because is efficient and well documented. PMSat was implemented with MPI technology, the industry's de-facto standard and widely portable, to be executed in clusters or grids of computers. It was developed at INESC-ID, in the ALGOS group, as final year project by Luís Gil, a student of Computer Science at Instituto Superior Técnico / Technical University of Lisbon, under supervision of professors Paulo Flores, Luís Miguel Silveira and Jaime Ramos.

How it works ?

The idea to obtain parallelism is to make a domain decomposition to explore the different parts of the search space at the same time. The search space is the set of all assignments to the variables of the formula and can be arranged as a binary tree. The binary tree is decomposed in independent subtrees with the creation of assumptions (the assignment of values for the most popular variables). MiniSat is able to receive a set of variables with a fixed value and just search the value of the others. With this method, several subtrees of the assignments tree can be processed in parallel according to the number of processes created.

The main features of PMSat are the two different methods to create and four different modes to test the assumptions (called search modes). Is also possible to share and remove learnt clauses, eliminate assumptions with conflicts, perform an automatic calculation of the options and display activity statistics.

How fast is it ?

One must realise that a SAT-solver performs a search algorithm to get a solution. By this reason the program achieves different performances according to the Boolean formula, the partition of the search space and the options chose. Sometimes there is a slowdown, other times the time spent is the same, but most of the times interesting speedups (sometimes super-linear) are achieved. This happens because each partition of the search space takes a different time to be solved and some of them are explored very quickly.

Related publication

PMSat-JSAT08.pdf Luís Gil, Paulo Flores, Luís Miguel Silveira, PMSat: a parallel version of MiniSAT, in Journal on Satisfiability, Boolean Modeling and Computation, Volume 6, pages 71-98, November 2008.
PMSat-tfc.pdf Full report of the final year project by Luís Gil

Source code and documentation

Download the following files to install and start using the PMSat solver. PMSat is distributed under the MIT License (see below).

PMSat-src.zip Download the PMSat source code.
PMSat-user-manual.pdf PMSat user's manual.

License

Both programs are under MIT License:

PMSat -- Copyright (c) 2006-2007, Luís Gil
MiniSat -- Copyright (c) 2003-2005, Niklas Eén, Niklas Sörensson

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sub-license, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NON-INFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.