Patent ID: 8825572

Claim:
A method performed by a computing device comprised of memory and a processor cooperating to perform the method, the method performed by the computing device comprising: executing, by the processor, a quantified belief propagation (QBP) algorithm that receives as input, from the memory, an existentially quantified boolean formula comprised of existentially quantified boolean variables, universally quantified variables, and a boolean formula comprised of subformulas each comprising one or more boolean operators operating on one or more of the existentially quantified variables and/or one or more of the universally quantified variables; constructing, in the memory, a tripartite graph comprised of nodes comprising: (i) there-exists nodes that correspond to and represent the existentially quantified variables, respectively, (ii) for-all nodes that correspond to and represent the universally quantified variables, and (iii) sub-formula nodes that correspond to and represent the sub-formulas, respectively; finding a set of boolean values of the existentially quantified variables by (i) passing a first message from an arbitrary sub-formula node to an arbitrary for-all node, and (ii) in response, passing a second message from the arbitrary for-all node to the arbitrary sub-formula node; and storing the set of boolean values in the memory.