 # 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``````