2. The method as recited in claim 1 , further comprising creating relevancy propagation rules for tracking which truth assignments are relevant for determining satisfiability of the formula.
4. The method as recited in claim 2 , wherein the relevancy propagation rules include: rule 1: when φ is shorthand for φ i , if φ is assigned true and is marked as relevant, then the first child φ i that gets assigned true is marked relevant, while if φ is assigned false and is marked as relevant, then all children are marked relevant; rule 2: when φ is shorthand for (φ 1 φ 2 ), if φ is marked as relevant, then both φ 1 and φ 2 are marked as relevant; and rule 3: when φ is ite(φ 1 ,φ 2 ,φ 3 ) , if φ is marked as relevant, then φ 1 is marked as relevant, and if φ 1 is assigned to true(false), then φ 2 (φ 3 ) is marked as relevant, wherein ite represents an if-then-else constraint structure.