Add reduction using SAT and QBF solvers

[notValord]

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.

The tests will be added shortly in future commits together with some small fixes. I was not sure with the proper location for the reduction implementation and its structures, as it is an another type of reduction the src/nfa/operations.cc seemed appropriate and the used structures were put into include/mata/nfa/types.hh but can be moved if necessary.

[ondrik]

We discussed with @notValord to remove the linux binaries of SAT/QBF solvers and add them as requirements.

[Adda0]

Hello. Thank you for the PR. One MacOS test seems to be failing. Otherwise, let me know when you finish with the changes so that the PR can be reviewed. In general, the implementation looks great to me after a quick glance.

as it is an another type of reduction the src/nfa/operations.cc seemed appropriate and the used structures were put into include/mata/nfa/types.hh but can be moved if necessary.

types.hh should be only for the general data types used by the user of Nfa. If the data structures are to be used only by the implementation of some algorithm, ideally the types should go as close to the place where they are to be used as possible. Such as in an anonymous namespace inside the source file with the algorithm. Or, if it is too much code, maybe creating some header files with internal namespaces such as plumbing, or internal might be appropriate. In this case, unless you plan on using these types elsewhere, I would just place everything in the anonymous namespace. Where do you think these types will be applicable / plan to use them?

[Adda0]

We discussed with @notValord to remove the linux binaries of SAT/QBF solvers and add them as requirements.

Sounds good to me. However, I would go with optional requirements, ideally. However, we do not currently have a way to specify optional requirements. Maybe for now only a note in the comment when selecting the specific algorithm would be enough? That way, everyone can add complex algorithms with dependencies, but the main Mata implementation will remain as small and clean as possible. What do you and anyone else think about this?

[ondrik]

Sounds good to me. However, I would go with optional requirements, ideally. However, we do not currently have a way to specify optional requirements. Maybe for now only a note in the comment when selecting the specific algorithm would be enough? That way, everyone can add complex algorithms with dependencies, but the main Mata implementation will remain as small and clean as possible. What do you and anyone else think about this?

I agree with optional requirements and tests (maybe generating a warning instead of a failed test).