Open-WBO MaxSAT Solver

Usage of the solver:

./open-wbo [options] <input-file>

The following options are available in Open-WBO:

-verbosity = {0,1}

Verbosity level (0=minimal, 1=more) (default: 1)

-algorithm = {0,1,2,3,4,5}

Algorithm strategy (0=wbo,1=linear-su,2=msu3,3=part-msu3,4=oll,5=best) (default: 5)

-bmo, -no-bmo

BMO search (default: on)

-pb = {0,1}

Pseudo-Boolean encodings (0=SWC,1=GTE) (default: 1)

-amo = {0}

At-most-one encodings (0=ladder) (default: 0)

-cardinality = {0,1,2}

Cardinality encodings (0=cardinality networks, 1=totalizer, 2=modulo totalizer) (default: 1)

The following options are available when using the wbo algorithm:

-weight-strategy = {0,1,2}

Weight strategy (0=none, 1=weight-based, 2=diversity-based) (default: 2)

-symmetry, -no-symmetry

Symmetry breaking (default: on)

-symmetry-limit = <num>

Limit on the number of symmetry breaking clauses (default: 500000)

The following options are available when using the PartMSU3 algorithm:

-graph-type = {0,1,2}

Graph type (0=vig, 1=cvig, 2=res) (default: 2)

-partition-strategy = {0,1,2}

Partition strategy (0=sequential, 1=sequential-sorted, 2=binary) (default: 2)

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

Options