Compact k-sat verification with tcams

A method comprising:

• programming one or more clauses of a Boolean expression for a K-SAT problem written in negated disjunctive normal form (DNF) to a ternary-CAM (TCAM) array comprising columns and rows of TCAM cells, wherein each clause of the Boolean expression is programmed to a respective row of the TCAM array, and wherein each occurring variable of each clause is mapped to a respective TCAM cell of the row, and wherein each non-occurring variable is programmed as a don't care value;
• applying a first interpretation, comprising one or more binary variables expected to solve the Boolean expression, as an input along the columns to the TCAM array;
• returning a binary value for each clause;
• updating one or more variables within the first interpretation if at least one clause of the Boolean expression is not satisfied;
• and
• applying a second interpretation, comprising one or more updated binary variables expected to solve the Boolean expression, as an input along the columns to the TCAM array.

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

• program one or more clauses of a Boolean expression for a K-SAT problem written in negated disjunctive normal form (DNF) to a TCAM array comprising columns and rows of TCAM cells, wherein each clause of the Boolean expression is programmed to a respective cell of the row of the TCAM array, and wherein each occurring variable of each clause is mapped to a respective cell of a row, and wherein each non-occurring variable is programmed as a don't care value;
• apply an interpretation, comprising one or more binary variables expected to solve the Boolean expression, as input along the columns to the TCAM array;
• return a binary value for each clause;
• and
• update one or more variables within the interpretation if at least one clause is violated.

A circuit for solving a K-SAT problem comprising:

• a K-SAT verification circuit configured to:
• program one or more clauses of a Boolean expression for a K-SAT problem written in negated disjunctive normal form (DNF) to a TCAM array comprising columns and rows of TCAM cells, wherein each clause of the Boolean expression is programmed to a respective cell of a row of the TCAM array, and wherein each occurring variable of each clause is mapped to a respective cell of the row, and wherein each non-occurring variable is programmed as a don't care value;
• apply an interpretation comprising search data to one or more search lines of the TCAM array, wherein the search data includes one or more binary variables expected to solve the Boolean expression, and wherein the search data is applied as an input along the one or more search lines;
• and
• discharge a match line if a row does not include the search data;
• and
• a K-SAT optimizer, configured to:
• update the interpretation if at least one match line is not discharged.