Satisfiability problem solver implemented on spiking neural network embedded systems

Patent metadata

Field	Value
Publication number	US-12511522-B2
Application number	US-202016933994-A
Country	US
Kind code	B2
Filing date	Jul 20, 2020
Priority date	Jul 18, 2019
Publication date	Dec 30, 2025
Grant date	Dec 30, 2025

Abstract

A spiking neural network (SNN) system is disclosed having spiking neurons associated with clause values associated with a satisfiability (SAT) problem. Each spiking neuron generates a voltage spike when on input voltage applied to each spiking neuron is increased above a spiking voltage threshold. The input voltage that is increased above the spiking voltage threshold is indicative that the corresponding clause value is satisfied. A controller applies the clause grid that includes clause values to a literal grid that includes literal values. The controller generates the input voltage that is applied to each spiking neuron based on each corresponding clause value associated with each spiking neuron that is applied to the literal values. The controller determines that each clause value is satisfied when the corresponding spiking neuron generates the voltage spike and that each clause value is unsatisfied when the corresponding spiking neuron fails to generate the voltage spike.

First claim

What is claimed is:

1 . A spiking neural network (SNN) system that implements a plurality of spiking neurons to solve a satisfiability (SAT) problem, comprising:
a plurality of spiking neurons with each spiking neuron associated with a corresponding clause value from a plurality of clause values associated with the SAT problem and configured to generate a voltage spike when at least one input voltage applied to each spiking neuron is increased above a spiking voltage threshold, wherein the at least one input voltage applied to each spiking neuron that is increased above the spiking voltage threshold is indicative that the corresponding clause value associated with the spiking neuron is satisfied; and a controller configured to:
determine a literal grid that includes a plurality of literal values associated with the SAT problem, wherein each literal value is a fixed binary value,
determine a clause grid that includes the plurality of clause values associated with the SAT problem, wherein each clause value includes a corresponding subset of the literal values and corresponds to a constraint from a plurality of constraints associated with the SAT problem and each constraint is to be satisfied to solve the SAT problem,
apply the clause grid that includes the plurality of clause values to the literal grid that includes the plurality of literal values,
generate the at least one input voltage that is applied to each spiking neuron based on each corresponding clause value associated with each spiking neuron that is applied to the plurality of literal values,
determine that each clause value is satisfied when the corresponding spiking neuron generates the voltage spike and that each clause value is unsatisfied when the corresponding spiking neuron fails to generate the voltage spike,
continuously feedback each clause value that is unsatisfied following each iteration applying the clause grid to an updated revised literal grid that includes the corresponding literal value of each incorrect literal value previously generated when the clause grid is applied to the literal grid, and
continuously apply the clause grid to each updated revised literal grid when at least one spiking neuron fails to generate the voltage spike indicating that at least one clause value is unsatisfied.

2 . The SNN system of claim 1 , wherein the at least one input voltage applied to each spiking neuron that is increased above the spiking voltage threshold is indicative that the corresponding clause value associated with the spiking neuron is unsatisfied.

3 . The SNN system of claim 1 , wherein the controller is further configured to:
determine a plurality of correct literal values and a plurality of incorrect literal values after the clause grid is applied to the literal grid, wherein each correct literal value is included in a corresponding clause value that is satisfied and each incorrect literal value is included in a corresponding clause value that is unsatisfied; transition each incorrect literal value to a corresponding complemented literal value, wherein each corresponding complemented literal value is a complement of the incorrect literal value that is initially applied to the corresponding clause value that is unsatisfied.

4 . The SNN system of claim 3 , wherein the controller is further configured to:
apply the clause grid that includes the plurality of clause values to a revised literal grid that includes the corresponding complemented literal value of each incorrect literal value previously generated when the clause grid is applied to the literal grid; generate the at least one input voltage that is applied to each spiking neuron based on each corresponding clause value associated with each spiking neuron that is applied to each revised literal value included in the revised literal grid; and determine that each clause value is satisfied when the corresponding spiking neuron generates the voltage spike and each clause value is unsatisfied when the corresponding spiking neuron fails to generate the voltage spike.

5 . The SNN system of claim 4 , wherein the controller is further configured to:
determine when each spiking neuron generates the voltage spike indicating each clause value is satisfied; and generate a SAT answer value that includes each current value of each corresponding literal value after each spiking neuron generates the voltage spike indicating each clause value is satisfied, wherein the SAT answer value is an answer to the SAT problem.

6 . The SNN system of claim 5 , further comprising:
a noise generator that is configured to randomly select a first portion of incorrect literal values from the plurality of incorrect literal values to transition to the corresponding complemented literal value and a second portion of incorrect literal values to refrain from transitioning to the corresponding literal value to prevent the SNN system from locking up when transitioning each incorrect literal value to the corresponding complemented literal value.

7 . The system of claim 1 , wherein the controller is further configured to:
map each clause value that corresponds to each clause associated with a corresponding constraint of the SAT problem into each column of the clause grid; weight each clause value with a binary weight to associate an impact of each clause as corresponding to each constraint of the SAT problem, wherein each constraint that includes an increased impact on the SAT problem is associated with each corresponding clause with an increased binary weight to correspond to the increased impact of each clause relative to each other clause.

8 . The system of claim 1 , wherein the controller is further configured to:
generate a feedback loop that provides an updated vector matrix with a plurality of updated literal values to thereby apply the updated vector matrix to the clause grid for each iteration to determine each clause that is satisfied and each clause that is unsatisfied; apply during the feedback loop the clause grid to the plurality of clause values to generate the revised literal grid that includes each corresponding complemented literal value of each incorrect literal value previously generated when the clause grid is previously applied to the literal grid; and generate during the feedback loop at least one input voltage to each spiking neuron based on each corresponding clause value associated with each spiking neuron that is applied to each revised literal value included in the revised literal grid.

9 . The system of claim 8 , wherein the controller is further configured to:
continuously feedback each value that is unsatisfied following each iteration of applying the clause grid to an updated revised literal grid that includes the corresponding literal value of each incorrect literal value previously generated when the clause grid is applied to the literal grid; continuously apply the clause grid to each updated revised literal grid when at least one spiking neuron fails to generate the voltage spike indicating that at least one clause value is unsatisfied; and determine when each spiking neuron generates the voltage spike indicating each clause is satisfied to generate a SAT answer value that includes each current value of each corresponding literal value after each spiking neuron generates the voltage spike indicating each clause value is satisfied, wherein the SAT answer value is an answer to the SAT problem.

10 . A method for implementing a plurality of spiking neurons to solve a Satisfiability (SAT) problem with each spiking neuron associated with a corresponding clause value from a plurality of clause values associated with the SAT problem, comprising:
generating by eac

Assignees

• Univ Of Dayton

Inventors

• Yakopcic Chris
• Taha Tarek M

Classifications

• G06N3/065

  Analogue means · CPC title

• G06N3/049 Primary

  Temporal neural networks, e.g. delay elements, oscillating neurons or pulsed inputs · CPC title