1. A method for determining satisfying variable assignments of a Boolean formula, or for determining that no satisfying variable assignments exist, the method comprising the steps of: a. assigning a variable to zero or one; b. generating implications resulting from the assignment using Boolean Constraint Propagation, wherein implications are generated by watching two literals, the two literals watched being randomly selected from variables not assigned to zero; and c. continuing steps (a) and (b) until reaching a conflict or until all variables are assigned, wherein upon reaching a conflict the assignment of at least one variable is changed, implications resulting from the changed assignment are generated and steps (a) and (b) continue until determining a satisfying variable assignment, or until determining that no satisfying variable assignment exists.