PWBO - Parallel Weighted Boolean Optimization Solver

PWBO is a parallel solver for Weighted Boolean Optimization. Using two threads, an unsatisfiability-based algorithm is used to search on the lower bound of the optimal solution, while at the same time a linear search is performed on the upper bound of the optimal solution. Moreover, learned clauses are shared between threads during the search [MML12a, MML12b].

For a larger number of threads two different strategies may be used. The first strategy performs a portfolio approach by searching on the lower and upper bound values of the optimal solution using different encodings of cardinality constraints for each thread. The second strategy splits the search space considering different upper bound values of the optimal solution for each thread.

There are some strategies, such as partitioning, that have only been incorportated into our sequential solver. For that, please visit the wbo homepage.

We have also developed a parallel deterministic version of pwbo [MML12c]. That version will soon be released for download.

Usage

./pwbo [options] <input-file>

Options

The following options are available in version 2.2 of PWBO:

-file-format = {cnf,wcnf,opb,wbo} (default wcnf)

'cnf' : takes as input file an unweighted MaxSAT instance
'wcnf' : takes as input file a partial or weighted MaxSAT instance
'opb' : takes as input file a Pseudo-Boolean instance
'wbo' : takes as input file a Weighted Boolean Optimization instance

-thread = {1,2,4,8} (default 2)

Number of threads to be used by the parallel solver

-search-mode = {lb,ub,split,portfolio} (default portfolio)

'lb' : uses the unsatisfiability-based algorithm proposed for Weighted Boolean Optimization [MMSP09, MML10]
'ub' : performs a linear search on the upper bound of the optimal solution using a dynamic heuristic that determines which encoding should be used to represent the objective function [MML11b, MML12b]
'split' : the search space is split considering different upper bounds of the optimal solution for each thread [MML11a, MML12b]
'portfolio' : performs a portfolio search on the lower and upper bound values of the optimal solution [MML11b, MML12b]

-time-limit = <num> (default 1800 sec.)

Time limit for finding the optimal solution

-verbosity = {0,1} (default 1)

Controls the verbosity level of the solver

Download

You can download the pwbo 2.2 solver.

A two thread specific version is also available for download.

Input Format and Benchmarks

Benchmarks and description of solver input files are available at the webpages of solver evaluations.

MaxSAT evaluation 2012: http://www.maxsat.udl.cat/12/

Pseudo-Boolean and Weighted Boolean Optimization evaluation 2012: http://www.cril.univ-artois.fr/PB12/

References

[MML12c] R. Martins, V. Manquinho, I. Lynce: Clause Sharing in Deterministic Parallel Maximum Satisfiability.RCRA 2012 (bibtex)
[MML12b] R. Martins, V. Manquinho, I. Lynce: Parallel Search for Maximum Satisfiability. AI Communications 25(2): 75-95 (2012) (bibtex)
[MML12a] R. Martins, V. Manquinho, I. Lynce: Clause Sharing in Parallel MaxSAT LION 2012: 455-460 (bibtex)
[MML11b] R. Martins, V. Manquinho, I. Lynce: Exploiting Cardinality Encodings in Parallel Maximum Satisfiability. ICTAI 2011: 313-320 (bibtex)
[MML11a] R. Martins, V. Manquinho, I. Lynce: Parallel Search for Boolean Optimization. RCRA 2011 (bibtex)
[MML10] V. Manquinho, R. Martins, I. Lynce: Improving Unsatisfiability-Based Algorithms for Boolean Optimization. SAT 2010: 181-193 (bibtex)
[MMSP09] V. Manquinho, J. Marques-Silva, J. Planes: Algorithms for Weighted Boolean Optimization. SAT 2009: 495-508 (bibtex)

Contact

Contributors: Vasco Manquinho, Ruben Martins, Inês Lynce

The software packages are made available solely for research and educational purposes. If you wish to use it for other purposes, you must contact the authors for permission.

To contact the authors please send an email to:

Last Update: November 2012