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).
Satisfiability of propositional theories is checked by means of a pseudo-Boolean solver extending Glucose 4 (single thread).
In this version the parameter k depends on the size of the processed core. Roughly, k is in O(log n), where n is the size of the core. Disjoint cores are initially computed.