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 not computed, but large cores are initially cached. After 10 minutes, caching is disabled.