|
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
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).
 |
Download the PMSat source code. |
 |
PMSat user's manual. |
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.
|
 |
|
|
