SAT solver based on interpretation and truth table analysis

A method for determining if a Boolean formula is satisfiable, wherein the Boolean formula defined over a set of variables, the method comprising:

• receiving a Boolean formula defined over n variables;
• determining a hierarchy of Boolean formulas based on the Boolean formula by recursively rewriting the Boolean formula as another Boolean formula that is defined over a subset of variables and a set of new variables, wherein each new variable represents a respective Boolean formula;
• representing each new variable by a truth table;
• and
• determining, by a processor that performs Boolean operations on m-bit words, wherein in is less than n, if the Boolean formula is satisfiable by iteratively performing a set of operations on a processor, the set of operations comprising:
• (1) assigning a value to a variable or a truth table, (2) inferring values of variables when a truth table is assigned a value, (3) restricting other truth tables that depend on a variable that is assigned a value, and (4) detecting a conflict if inconsistent values are attempted to be assigned to a variable.

A non-transitory computer-readable storage medium storing instructions, which when executed by a processor, cause the processor to:

• define m-bit constants corresponding to distinct m-bit patterns, wherein the processor performs Boolean operations on m-bit words, wherein a Boolean formula is defined over n variables, and wherein n is greater than in;
• and
• iteratively perform a set of operations, comprising:
• selecting a distinct (n-m)-bit pattern,
• assigning values to variables by combining the m-bit constants with the distinct (n-m)-bit pattern,
• evaluating the Boolean formula by using the values assigned to the variables, and
• in response to determining that the Boolean formula evaluated to a TRUE value, determining that the Boolean formula is satisfiable.