This is a collection of reductions from FACT to SAT.
Todo: implement enforcing nontrivial factors (neither factor may be 1, i.e for a, force
!(!a0 ∧ !a1 ∧ ... ∧ !a[n-1] ∧ a[n])).
mk_array_multiplier. This would more-or-less mark the implementation of the simplest reduction.