to parallelize SAT solving through decomposition into smaller problems and composing solutions to those smaller problems.

Let S₁ and S₂ be a decomposed SAT problem with solutions φ₁ and φ₂ respectively. What we seek are representations for φ₁ and φ₂ and a function Φ such that Φ(φ₁,φ₂) is the solution of S₁ ∪ S₂ and the following properties hold for φ₁,φ₂, and Φ(φ₁,φ₂):

1. The size of the representation is as "compact" as possible (preferably polynomial space in the number of variables).
2. Enumeration of solutions is polynomial time on the size of the representation.
3. The number of redundant solutions in the representation is low (no solution is repeated more than C times for some reasonable C)
4. Two representations can be composed (their solution spaces intersected) efficiently (preferably in polynomial time).

The disjunctive normal form of a boolean formula is an enumeration of all the valid variable assignments which make the formula true. This representation may be exponential in space, requiring upto 2^N disjuncts where N is the number of variables needing assignment. Such an enumeration does not account for the structural regularity of similar solutions. Our goal is to find a representation which is compact and can efficiently be expanded to recover the DNF of the formula. To do this we are looking at a representation which employs data compression techniques, i.e. using shorter strings to describe a set of larger strings. We call this representation Solution Normal Form (SNF)

There is a strong homomorphism between regular expressions and SAT. Let the alphabet for our regular expression be the variables used in a given SAT problem. A variable assignment V, where the variable order is fixed, satisfies a boolean formula F if and only if the projection λ(V) is recognized by the regular expression λ(F)

λ(F) is defined as follows:

1. λ(True) → The set of all strings where each character occurs at most once and in the same order as the variable ordering
2. λ(False) → The empty set of strings
3. λ(Variable V) → All strings in λ(True) which contain the character representing variable V
4. λ(¬A) → λ(True) - λ(A)
5. λ(A∧B) → λ(A) ∩ λ(B)
6. λ(A∨B) → λ(A) ∪ λ(B)