Add a SAT solver (behind a feature flag)

[koenichiwa]

To check if groups are valid, currently we're checking the superset of all initialization states, which is $O(2^g)$ where $g$ is the amount of "grouped" fields. Maybe a SAT solver could help us speed that up.