The source files of Open-WBO are the following:

Makefile - Compiles the source files - Script for easy cleaning of compiled files - Script for easy compilation with different SAT solvers - Main options for Open-WBO

Dimacs.h - MaxSAT parser

Soft.h - Soft clauses class

Hard.h - Hard clauses class

MaxTypes.h - Useful enumerators

Encoder.* - Interface for the different encodings

MaxSAT.* - Parent class for the different MaxSAT algorithms

algorithms/ - Subdirectory with MaxSAT algorithms

algorithms/Alg_* - Source files for MaxSAT algorithms

encodings/ - Subdirectory with MaxSAT encodings

encodings/Encodings.* - Parent class for the different encodings

encodings/Enc_* - Source files for encodings of linear constraints to CNF

solvers/ - Subdirectory with SAT solvers

solvers/X/ - Source files of SAT solver X

Open-WBO is compiled like MiniSAT. The option "s" statically compiles Open-WBO, and the option "r" compiles Open-WBO in release mode. For example:

make rs - compiles Open-WBO statically ("s") in release mode ("r")

make - compiles Open-WBO dynamically in debug mode

Any MiniSAT-like SAT solver may be used with Open-WBO. If you want to use a new SAT solver (e.g. "MiniSAT 2.0"), it is necessary to crease a subdirectory (e.g. "minisat2.0") inside the "solvers" directory and change the Makefile accordingly:

# VERSION = core or simp

# SATSOLVER = name of the SAT solver

# SOLVERDIR = subdirectory of the SAT solver

# NSPACE = namespace of the SAT solver


# e.g. MiniSAT 2.0 compilation with simp version:


VERSION = simp


SOLVERDIR = minisat2.0

NSPACE = Minisat


The following SAT solvers are included in this version of Open-WBO: (i) minisat2.0, (ii) minisat2.2, (iii) glucose2.3, (iv) glucose3.0, (v) zenn, (vi) sinn, (vii) glueminisat, (viii) gluh, (ix) glue_bit, (x) glucored. We would like to thank the authors of those solvers for making their source code publicly available. Further information regarding those solvers may be found in the following references.


SAT Solver References: