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=linear-us, 3=msu3, 4=wmsu3, 5=best) (default: 5)

-bmo, -no-bmo

 BMO search (default: on)

-incremental = {0,1,2,3}

 Incremental strategy (0=none, 1=blocking, 2=weakening, 3=iterative) (default: 3)

-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)


Input format and benchmarks:

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

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