|
pmcSAT
pmcSATpmcSAT is a portfolio-based multi-threaded,
multi-core SAT solver, built on top of MiniSAT. The general strategy pursued in this
solver is to launch multiple instances of the same solver, with different
parameter configurations, which cooperate to a certain degree by sharing
relevant information when searching for a solution. This approach has the
advantage of minimizing the dependence of current SAT solvers on specific
parameter configurations chosen to regulate their heuristic behavior,
namely the decision process on the choice of variables, on when and how to
restart, on how to backtrack, etc. This solver was developed at INESC-ID, in the ALGOS group, under the ParSAT research project
(PTDC/EIA-EIA/103532/2008) by Ricardo Marques, a student of Electrical and
Computer Engineering at Instituto Superior
Técnico / Technical University of
Lisbon, under supervision of professors Luís G. Silva, Paulo Flores, and Luís Miguel Silveira.
How it works ?
The solver uses multiple threads (eight currently) that explore the search
space independently, following different paths, due to the way each thread is
configured. In order to ensure that each thread follows divergent search
paths, we defined distinct priority assignment schemes, one for each thread
of pmcSAT.
Although each pmcSAT thread exploiting independently the search
space, this is not just a purely competitive solver. The threads cooperate by
sharing the learnt clauses resulting from conflict analysis, leading to a
larger pruning of the search space
Related publication
 |
SAT Competition
2013
Ricardo Marques, Luís Guerra e Silva, Paulo Flores, Luís
Miguel Silveira,
pmcSAT,
Participation in the SAT Competition 2013, May 2013.
|
 |
Ricardo Marques, Luís Guerra e Silva, Paulo Flores, Luís Miguel
Silveira, Improving
SAT Solver Efficiency using a Multi-core Approach, in
International FLAIRS Conference, May 22 - 24, 2013 (accepted). |
Source code and documentation
Download the following files to install and start using the
pmcSAT solver. pmcSAT is distributed under the MIT License
(see below).
Both programs are under
MIT License:
pmcSAT -- Copyright (c) 2006-2007, Ricardo Marques
MiniSat -- Copyright (c) 2003-2005, Niklas Eén, Niklas Sorensson
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.
|
 |
|
|
