1. only convert to CNF once
2. group predicates that only appear in specific combinations to limit amount of variables provided to the sat solver
Number 2 above does technically slow down all cases a bit, but the optimization is really important when it matters. And cases that don't need this optimization still happen on the order microseconds anyway.
