Overview

FACT->SAT reductions

This is a collection of reductions from FACT to SAT.

TODO

  • Todo: implement enforcing nontrivial factors (neither factor may be 1, i.e for a, force !(!a0 ∧ !a1 ∧ ... ∧ !a[n-1] ∧ a[n])).

  • Todo: implement mk_array_multiplier. This would more-or-less mark the implementation of the simplest reduction.