Maxino

Maxino is a solver for MaxSAT, the optimization variant of the satisfiability problem for propositional formulas. Maxino is based on the k-ProcessCore algorithm described in the following paper:

Mario Alviano, Carmine Dodaro, and Francesco Ricca.
A MaxSAT Algorithm Using Cardinality Constraints of Bounded Size.
Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI 2015).
Online appendix: [PDF]

Binaries sent at 2015 MaxSAT Evaluation (Linux 64-bits): [maxino-k16], [maxino-kdyn].
Source code: [GitHub (aspino project)].

The binaries above implement algorithm K and can be run as follows:

$ ./maxino-k16  <input-file>
$ ./maxino-kdyn <input-file>

where

  • input-file is the path to the input instance; if omitted, the input is read from STDIN.

For example, to run maxino on an instance example.cnf, one of the following command lines can be used:

$ ./maxino-k16  example.cnf 
$ ./maxino-kdyn example.cnf 

where the first uses algorithm K bounding the size of cardinality constraints to 16 literals, and the second uses algorithm K with a dynamic selection of the bound depending on the size of the processed core.

If example.cnf contains the following simple instance (essentially, the formula in Example 1 of the IJCAI paper):

p wcnf 4 16 100
100 -1 -2 -3 0
100 -1 -2 -4 0
100 -1 -3 -2 0
100 -1 -3 -4 0
100 -1 -4 -2 0
100 -1 -4 -3 0
100 -2 -3 -1 0
100 -2 -3 -4 0
100 -2 -4 -1 0
100 -2 -4 -3 0
100 -3 -4 -1 0
100 -3 -4 -2 0
1 1 0
1 2 0
2 3 0
2 4 0

the output of maxino will be the following:

o 0
c ub 2
o 1
o 2
s OPTIMUM FOUND
v -1 -2 3 4

Compared Solvers