ALGOS Logo
pmcSAT

pmcSAT

pmcSAT 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

satCompetition2013.pdf 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.
 
pmcSAT-flairs13.pdf 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).

pmcSAT-src.zip Download the pmcSAT source code.

License

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.