# US 2023/0410902 A1 · Compact k-sat verification with tcams

> Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt

- Number: US 2023/0410902 A1
- Document ID: US20230410902A1
- Status: Published application
- Kind: A1
- Application number: 17/841,532
- Filed: 2022-06-15
- Published: 2023-12-21
- Earliest claimed: 2022-06-15
- Assignees: Hewlett Packard Enterprise Development LP
- Applicants: Hewlett Packard Enterprise Development LP
- Inventors: Giacomo Pedretti; Tobias Frederic Ziegler; Thomas Van Vaerenbergh; Catherine Graves
- Web page: https://patentgrep.com/patent/US20230410902A1

## CPC

- G11C 15/046: {using non-volatile storage elements}
- G11C 15/04: using semiconductor elements
- H03K 19/20: characterised by logic function, e.g. AND, OR, NOR, NOT circuits (H03K19/003 - H03K19/01 take precedence)
- G11C: STATIC STORES (semiconductor memory devices H10B)
- H03K: PULSE TECHNIQUE (measuring pulse characteristics G01R; modulating sinusoidal oscillations with pulses H03C; transmission of digital information H04L; discriminator circuits detecting phase difference between two signals by counting or integrating cycles of oscillation H03D3/04; automatic control, starting, synchronisation or stabilisation of generators of electronic oscillations or pulses where the type of generator is irrelevant or unspecified H03L; coding, decoding or code conversion, in general H03M)

## Abstract

The disclosure generally provides for a method of solving a K-SAT problem. The method comprises 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, applying an 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 and updating one or more variables within the interpretation if at least one clause is violated.

## Claims

### Claim 1

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 an 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; and
updating one or more variables within the interpretation if at least one clause is violated.

### Claim 2 (depends on 1)

The method of claim 1, wherein programming each clause of the Boolean expression for the K-SAT problem written in negated disjunctive normal form (DNF) includes programming a bit value that includes a 0, 1, or X to each cell within each TCAM array, wherein the X represents a don't care value.

### Claim 3 (depends on 2)

The method of claim 2, wherein each negation of each literal in each clause is assigned a bit value of 0, each non-negation of each literal in each clause is assigned a bit value of 1, and each absent variable in each clause is assigned a bit value of X.

### Claim 4 (depends on 1)

The method of claim 1, wherein each match line returns a high bit value if the interpretation violates the clause stored in a corresponding row of the TCAM array, and wherein each match line returns a low bit value if the interpretation satisfies the clause stored in the corresponding row of the TCAM array.

### Claim 5 (depends on 1)

The method of claim 1, further comprising: generating an updated interpretation comprising one or more updated variables.

### Claim 6 (depends on 1)

The method of claim 1, wherein each match line is pre-charged to a high voltage.

### Claim 7

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.

### Claim 8 (depends on 7)

The method of claim 7, wherein programming each clause of the Boolean expression for the K-SAT problem written in negated disjunctive normal form (DNF) includes programming a bit value that includes a 0, 1, or X to each cell within each TCAM array, wherein the X represents a don't care value.

### Claim 9 (depends on 8)

The method of claim 8, wherein each negation of each literal in each clause is assigned a bit value of 0, each non-negation of each literal in each clause is assigned a bit value of 1, and each absent variable in each clause is assigned a bit value of X.

### Claim 10 (depends on 7)

The method of claim 7, wherein each match line returns a high bit value if the interpretation violates the clause stored in a corresponding row of the TCAM array, and wherein each match line returns a low bit value if the interpretation satisfies the clause stored in the corresponding row of the TCAM array.

### Claim 11 (depends on 7)

The method of claim 7, further comprising: generating a new interpretation comprising one or more updated variables.

### Claim 12 (depends on 7)

The method of claim 7, wherein each variable 1, 0, and X corresponds to a different voltage applied to each search line of the TCAM array.

### Claim 13

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.

### Claim 14 (depends on 13)

The non-transitory computer readable storage medium of claim 13 storing instructions that when executed cause the processor to further:
program a bit value that includes a 0, 1, or X to each cell within each TCAM array.

### Claim 15 (depends on 14)

The non-transitory computer readable storage medium of claim 14 storing instructions that when executed cause the processor to further:
assign a bit value of 0 for each negation of each literal in each clause;
assign a bit value of 1 for each non-negation of each literal in each clause; and
assign a bit value of X for each absent variable in each clause.

### Claim 16 (depends on 13)

The non-transitory computer readable storage medium of claim 13 storing instruction that when executed cause the processor to further:
apply an updated interpretation, comprising one or more updated binary variables expected to solve the Boolean expression, as input along the columns to the TCAM array.

### Claim 17

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.

### Claim 18 (depends on 17)

The circuit of claim 17 wherein, the search data includes a bit value that includes a 0, 1, or X to each cell within each TCAM array, wherein the X represents a don't care value.

### Claim 19 (depends on 18)

The circuit of claim 18 wherein, each negation of each literal in each clause is assigned a bit value of 0, each non-negation of each literal in each clause is assigned a bit value of 1, and each absent variable in each clause is assigned a bit value of X.

### Claim 20 (depends on 17)

The circuit of claim 17, wherein the K-SAT verification circuit is further configured to apply an updated interpretation comprising updated search data.