WBO - Weighted Boolean Optimization Solver

Weighted Boolean Optimization (WBO) is a formalism for problem solving that extends Weighted-Partial Max-SAT and Pseudo-Boolean Optimization.

A WBO formula is defined by a set of hard constraints and a set of weighted soft constraints. The objective is to find an assignment to problem variables such that all hard constraints are satisfied and the total weight of unsatisfied soft constraints is minimized.

In WBO, one can use pseudo-Boolean constraints as both soft and hard constraints. Hence, any Max-SAT or Pseudo-Boolean formula can be naturally encoded into the WBO formalism. In fact, our solver is able to solve any Boolean optimization formula in WBO, WCNF or OPB format.

We have also developed a multicore parallel Boolean optimization solver. For our parallel solver, please visit the pwbo homepage.

Usage

./wbo [options] <input-file>

Options

The following options are available in version 2.0 of WBO:

-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

-preprocessor = {no,yes} (default yes)

(Dis)enables preprocessing techniques for optimization formulas [MML10]

-search-mode = {normal,part-weight,part-graph,part-dyn} (default normal)

'normal' : uses the unsatisfiability-based algorithm proposed for Weighted Boolean Optimization [MMSP09]
'part-weight' : for weighted problems it uses a partition-based algorithm using the weight of the soft clauses [MML12]
'part-graph' : for weighted problems it uses a partition-based algorithm using a graph based approach [MML12]
'part-dyn' : dynamically chooses between 'normal', 'part-weight' and 'part- graph' based on the instance properties [MML12]

-part-graph = <num> (only for search mode 'part-graph' and 'part-dyn', default 16)

Number of partitions that are created when using the graph based approach

-amo = {pairwise, ladder, bitwise, commander, product, sequential, totalizer, sorters, pb} (default pb)

Encoding for the at-most-one cardinality constraints [MML11]

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

Time limit for finding the optimal solution

Download

You can download the solver.

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

[MML12] R. Martins, V. Manquinho, I. Lynce: On Partitioning for Maximum Satisfiability. ECAI 2012: 913-914 (bibtex)
[MML11] R. Martins, V. Manquinho, I. Lynce: Exploiting Cardinality Encodings in Parallel Maximum Satisfiability. ICTAI 2011: 313-320 (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, João Marques-Silva, Jordi Planes

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