Factor the polynomials before processing

[lvella]

This is an idea for generalizing the approach of Picus for issue #7.

In issue number #7, instead of processing one huge polynomial, Picus tries to solve the problem with one factor at a time. Considering that a polynomial is a disjunction of factors, so that (f1 = 0) OR (f2 = 0) is equivalent to p = f2*f1 = 0, we can apply this idea to partition any polynomial that can be factored.

For instance, consider the following system:

f = 0
g = 0
h = 0

suppose that we can decompose each of the f, g, and h polynomials into:

f1*f2 = 0
g1*g2*g3 = 0
h = 0

Then we have that if any system in {[fi, gk, h] | i ∈ {1,2} and k ∈{1,2,3}} is satisfiable, the whole system is satisfiable. This can be used for parallelism, or, if we consider Picus experience were proving all combinations to be UNSAT is cheaper than proving the full system at once, this decomposition can be used for raw serial speedup.

We can also use this factorization decompose the system into a set of clauses and leverage the power of well studied SMT algorithms:

(f1 = 0 OR f2 = 0) AND (g1 = 0 OR g2 = 0 OR g3 = 0) AND (h)