Compact k-XOR-SAT filtering with cams
Examples of the presently disclosed technology provide CAM-based circuits specially constructed to implement Boolean satisfiability problems involving k-XOR-SAT clauses. With the strategic addition of auxiliary counting and logic circuits that evaluate match line voltage outputs of a CAM at k discrete times in order to determine whether a counted number of matches returned by a match line satisfies a pre-determine parity condition—where k represents a number of literals of a k-XOR-SAT clause of a Boolean satisfiability problem—a circuit of the present technology can leverage a common CAM (i.e., the same CAM) to implement the k-XOR-SAT clause and k-SAT clauses. Accordingly, this extremely versatile circuit can be used to implement k-XOR-SAT and k-SAT-k-XOR-SAT hybrid problems in less time, and with less hardware and power consumption than existing hardware accelerators.
1. A circuit comprising:
a row of content addressable memory (CAM) cells programmed to store a k-exclusive OR-satisfaction (k-XOR-SAT) clause of a Boolean satisfiability problem;
a sense amplifier that, in response to an input vector being applied to the row of CAM cells:
compares, at k discrete times, voltage output of a match line associated with the row of CAM cells to a threshold voltage, wherein k represents a number of literals of the k-XOR-SAT clause;
a counter circuit that counts a number of matches returned by the match line based on the k voltage comparisons of the sense amplifier; and
a logic circuit that outputs a signal indicating the input vector satisfies the k-XOR-SAT clause based on the counted number of matches satisfying a pre-determined parity condition.
2. The circuit of claim 1 , wherein:
the row of CAM cells comprises k literal-representing CAM cells; and
a literal-representing CAM cell of the k literal-representing CAM cells is programmed to store a literal of the k-XOR-SAT clause.
3. The circuit of claim 1 , wherein the counted number of matches corresponds with a number of the k voltage comparisons where the voltage output of the match line exceeded the threshold voltage.
4. The circuit of claim 1 , wherein the pre-determined parity condition comprises an odd number of matches.
5. The circuit of claim 2 , wherein programming the literal-representing CAM cell to store the literal of the k-XOR-SAT clause comprises:
programming the literal-representing CAM cell to store a first value when the literal is negated in the k-XOR-SAT clause; and
programming the literal-representing CAM cell to store a second value when the literal is not negated in the k-XOR-SAT clause.
6. The circuit of claim 5 , wherein:
the row of CAM cells further comprises a non-literal-representing CAM cell programmed to store a wildcard value.
7. The circuit of claim 2 , wherein programming the literal-representing CAM cell to store the literal of the k-XOR-SAT clause comprises:
programming conductance of a memristor included in the literal-representing CAM cell.
8. The circuit of claim 1 , further comprising:
a second row of CAM cells programmed to store a second k-XOR-SAT clause of the Boolean satisfiability problem;
a second sense amplifier that, in response to the input vector being applied to the second row of CAM cells:
compares, at the k discrete times, voltage output of a second match line associated with the second row of aCAM cells to the threshold voltage;
a second counter circuit that counts a number of matches returned by the second match line based on the k voltage comparisons of the second sense amplifier; and
a second logic circuit that outputs a signal indicating the input vector satisfies the second k-XOR-SAT clause based on the counted number of matches satisfying the pre-determined parity condition.
9. The circuit of claim 8 , further comprising a processor, that in response to receiving the signal from the first logic circuit and the signal from the second logic circuit:
determines the input vector satisfies the Boolean satisfiability problem.
10. A method of solving a Boolean satisfiability problem using a CAM-based circuit, the method comprising:
comparing, at k discrete times, voltage output of a match line associated with a row of CAM cells to a threshold voltage, wherein:
the CAM-based circuit comprises the row of CAM cells,
the row of CAM cells is programmed to store a k-XOR-SAT clause of the Boolean satisfiability problem, and
k represents a number of literals of the k-XOR-SAT clause;
counting a number of matches returned by the match line based on the k voltage comparisons; and
determining the input vector satisfies the k-XOR-SAT clause based on the counted number of matches satisfying a pre-determined parity condition.
11. The method of claim 10 , further comprising:
comparing, at the k discrete times, voltage output of a second match line associated with a second row of CAM cells to the threshold voltage, wherein:
the CAM-based circuit comprises the second row of CAM cells,
the second row of CAM cells is programmed to store a second k-XOR-SAT clause of the Boolean satisfiability problem,
counting a number of matches returned by the second match line based on the k voltage comparisons associated with the voltage output of the second match line; and
determining the input vector satisfies the second k-XOR-SAT clause based on the counted number of matches returned by the second match line satisfying the pre-determined parity condition.
12. The method of claim 10 , further comprising:
comparing, at the k discrete times, voltage output of a second match line associated with a second row of CAM cells to the threshold voltage, wherein:
the CAM-based circuit comprises the second row of CAM cells,
the second row of CAM cells is programmed to store a second k-XOR-SAT clause of the Boolean satisfiability problem,
counting a number of matches returned by the second match line based on the k voltage comparisons associated with the voltage output of the second match line; and
determining the input vector violates the second k-XOR-SAT clause based on the counted number of matches returned by the second match line violating the pre-determined parity condition.
13. The method of claim 11 , further comprising:
determining the input vector satisfies the Boolean satisfiability problem.
14. The method of claim 12 , further comprising:
determining the input vector violates the Boolean satisfiability problem.
15. The method of claim 10 , wherein:
the row of CAM cells comprises k literal-representing CAM cells; and
a literal-representing CAM cell of the k literal-representing CAM cells is programmed to store a literal of the k-XOR-SAT clause.
16. The method of claim 15 , further comprising:
programming the literal-representing CAM cell to store a first value when the literal is negated in the k-XOR-SAT clause; and
programming the CAM cell to store a second value when the literal is not negated in the k-XOR-SAT clause.
17. The method of claim 15 , further comprising programming the literal-representing CAM cell to store the literal of the k-XOR-SAT clause by programming conductance of a memristor included in the literal-representing CAM cell.
18. A CAM-based circuit comprising:
a row of CAM cells programmed to store a k-XOR-SAT clause of a Boolean satisfiability problem, wherein:
k represents a number of literals of the k-XOR-SAT clause,
the row of CAM cells comprises k literal-representing CAM cells, and
a literal-representing CAM cell of the k literal-representing CAM cells is programmed to store a literal of the k-XOR-SAT clause;
a sense amplifier that, in response to an input vector being applied to the row of CAM cells:
compares, at k discrete times, voltage output of a match line associated with the row of CAM cells to a threshold voltage;
a counter circuit that counts a number of matches returned by the match line based on the k voltage comparisons of the sense amplifier; and
a logic circuit that outputs a signal indicating the input vector satisfies the k-XOR-SAT clause based on the counted number of matches satisfying a pre-determined parity condition.
19. The CAM-based circuit of claim 18 , wherein the counted number of matches corresponds with a number of the k voltage comparisons where the voltage output of the match line exceeded the threshold voltage.
20. The CAM-based circuit of claim 18 , wherein programming the literal-representing CAM cell to store the literal of the k-XOR-SAT clause comprises:
programming the literal-representing CAM cell to store a first value when the literal is negated in the k-XOR-SAT clause; and
programming the literal-representing CAM cell to store a second value when the literal is not negated in the k-XOR-SAT clause.