1. A method, composing: receiving a formula comprising a set of clauses, each clause comprising a disjunction of literals; receiving a plurality of proof objective literals, each proof objective literal comprising a variable or a negation of the variable, wherein the variable or the negation of the variable occurs in the formula; performing operations on a satisfiability search space until no unresolved proof objective literal exists, the operations comprising; assigning an unresolved proof objective literal of the plurality of proof objective literals as a currently watched proof objective literal; performing Boolean constraint propagation on the formula; if a model is found during Boolean constraint propagation, designating proof objective literals that are assigned false by the model as falsifiable and un-assigning literals of the formula that are not globally true; and designating globally true proof objective literals as valid proof objective literals.