Patent ID: 8589327

Claim:
A computer program product comprising a non-transitory computer readable storage medium having a computer readable program stored therein, wherein the computer readable program, when executed on a computing device, causes the computing device to: determine whether a Boolean satisfiability (SAT) problem is satisfied without applying constraints in a list of constraints; responsive to the SAT problem being satisfied without applying the constraints in the list of constraints, fix a set of variable assignments determined in satisfying the SAT problem without applying the constraints in the list of constraints; for each constraint in the list of constraints, determine whether the set of variable assignments remain constant when applying the constraint to the SAT problem; responsive to the set of variable assignments remaining constant when applying the constraint to the SAT problem, add the constraint to a list of non-affecting constraints; return a satisfied result; and responsive to the set of variable assignments changing when applying the constraint to the SAT problem, add the constraint to a list of affecting constraints; unfix the set of variable assignments determined in satisfying the SAT problem without applying the constraints in the list of constraints; determine whether the SAT problem is satisfiable with the constraint being applied; responsive to the SAT problem being satisfied with the constraint, fix a new set of variable assignments determined in satisfying the SAT problem with the constraint being applied; for each remaining constraint in the list of constraints, continuing with determine whether the SAT problem with the constraint results in the new set of variable assignments remain constant, change, or are inconclusive.