Add implementation of two new types of reduction using solvers. The
basic idea was the possibility of using solvers for reduction and
whether it is possible to create minimal nondeterministic automata.

The solvers work with an automata representation using the CNF
formula with variables representing its transitions, initial and final
states. The solver then tries to find a solution that satisfies the given
clause. The sets are updated until an equivalent automaton is found. The
number of states is increasing from the default value making sure that
the found automaton is minimal.

The reductions are working with structs SatStats and QbfStats, both
inheriting from the base stat AutStats, which defines the number of
states and symbols of the automaton, the two sets of words, and an output
stream. Declarations can be found in include/mata/nfa/types.hh.

The reductions are working with the same interface as the other possible
reduction algorithms which are parametrized using the ParameterMap.