Skip to content
Home » Using Bio-Inspired Computing to Efficiently Solving SAT Problems

Using Bio-Inspired Computing to Efficiently Solving SAT Problems

With Moore’s law coming to an end, and, with it, the digital age, alternative novel computing systems have to be explored. Physical systems and processes, just like biological ones, can inspire the design of computer algorithms.

Early ideas

The ideas behind biological computing trace back to 1936 and the first description of an abstract computer, which is now known as a Turing machine. Turing firstly described the abstract construct using a biological specimen. Turing imagined a mathematician that has three important attributes. He always has a pencil with an eraser, an unlimited number of papers and a working set of eyes. The eyes allow the mathematician to see and perceive any symbols written on the paper while the pencil allows him to write and erase any symbols that he wants. Lastly, the unlimited paper allows him to store anything he wants memory. Using these ideas he was able to describe an abstraction of the modern digital computer. However Turing mentioned that anything that can perform these functions can be considered such a machine and he even said that even electricity should not be required to describe digital computation and machine thinking in general.

Recent development

In recent years, the research community has witnessed an explosion of literature dealing with the adaptation of behavioral patterns and social phenomena observed in nature towards efficiently solving complex computational tasks. This trend has been especially dramatic in what relates to optimization problems, mainly due to the unprecedented complexity of problem instances, arising from a diverse spectrum of domains such as transportationlogisticsenergyclimatesocial networkshealth and industry 4.0, among many others. Notwithstanding this upsurge of activity, research in this vibrant topic should be steered towards certain areas that, despite their eventual value and impact on the field of bio-inspired computation, still remain insufficiently explored to date. Some areas of study in biologically inspired computing, and their biological counterparts:

bio inspired computation ecosystem
Image: Applications of Bio-inspired Computation

One of the interesting areas we are discussing today is the simulation of Amoebas. Our simulation extracts the essence of spatiotemporal oscillatory dynamics of a singlecelled amoeboid organism, the true slime mold Physarum polycephalum, which is capable of searching for a solution to some optimization problems. When placed under our previously studied spatiotemporal control which applies aversive light stimuli locally and dynamically depending on the shape of the organism, the organism exhibits chaotic oscillatory dynamics and finds a solution to the traveling salesman problem by changing its shape into the optimal one for which the area of the body is maximized and the risk of being illuminated is minimized.

To fully leverage the advantages of the parallelism we have implemented the simulation in Verilog (FPGA)to run on a chip. In a recently published paper “A Circuit-Level Amoeba-Inspired SAT Solver” from N. Takeuchi, Member, IEEE, M. Aono, Y. Hara-Azumi, and C. L. Ayala, Member, IEEE, an implementation methodology is suggested which outperforms traditional SAT solvers:

iterations to find a solution to a sat problem

The proposed solver is a biologically-inspired stochastic local search (SLS) solver to explore solutions to the Boolean satisfiability problem (SAT). It updates multiple variables in parallel at every iteration step, and thus it can find solutions with a fewer number of iteration steps than some other conventional SLS solvers for a specific set of SAT instances. However, the parallelism of the solver is not compatible with general-purpose microprocessors in that many clock cycles are required to execute each iteration; thus, it requires special hardware that can exploit the parallelism to quickly find solutions.

In their paper, they propose a circuit model (hardware-friendly algorithm) that explores solutions to SAT, which they call circuit-level AmbSAT (CLAmbSAT). The authors conducted numerical simulation to evaluate the search performance of CL-AmbSAT for a set of randomly generated SAT instances that was designed to estimate the scalability of their approach. Simulation results showed that CLAmbSAT finds solutions with a fewer iteration number than a powerful SLS solver, ProbSAT, and outperforms even AmbSAT. Since CL-AmbSAT uses simple combinational logic to update variables, CL-AmbSAT can be easily implemented in various hardware.

Implementation

Assuming that the reader is already familiar with SAT problems, we jump right into the implementation. It consists of the core solving code as well as multiple variable cells for each clause of the SAT formulation to be solved. Given an N-variable formula, the SAT solver is defined as a discrete-time-state dynamical system consisting of 2 · N units, each of which is labeled with (i, v) ∈ I × {0, 1} and is an analogy of a pseudopod-like branch of the amoeboid organism.

The conversion from a CNF file to a “cell” is done with a simple Python script:

for lit in literals:
o = o + " assign c["+str(cnt)+"] = (";
for l in lit:
tmp = int(l);
if tmp>0:
o = o + "x["+str(abs(tmp))+'] |'
else:
o = o + "~x["+str(abs(tmp))+'] |'
o = o[0:-1];
o = o + ');\n';
text_file.write(o); o = '';
cnt = cnt + 1;
if cnt % 1000 == 0: print(cnt,'clause assigns generated...');

We basically iterate through each literal and generate an Amoeba functional “cell” which is generated as Verilog RTL code. For example, one clause becomes:

assign F1[1] = ~(x[11] |x[29]) | ~(~x[29] |~x[31]) ;    
assign F0[1] = (x[29] |~x[50]) & (x[2] |~x[8]) ;
assign CONTRA_NEXT[1] = ~ (~F1[1] | F0[1]) ;
assign CONTRA_IN[1] = CONTRA[11] |CONTRA[29] |CONTRA[31] |CONTRA[50] |CONTRA[2] |CONTRA[8] ;

The main solver code consists of a module which implements the parallel flipping logic of each variable:

INPUT:  A k-SAT formula F. 
OUTPUT: A satisfiable assignment or “not found”
BEGIN: Determine B (bounceback rules) of F
FOR (i, v) = (1, 0) to (N, 1)
Set Xi,v = 0, Ri,v = 0, and S i,v = 0;
Choose fi,v ∈ [0.0, 1.0] randomly;
END FOR
REPEAT:
Obtain an assignment x from X;
IF x satisfies F THEN RETURN x;
ELSE FOR (i, v) = (1, 0) to (N, 1)
Update Xi,v, Ri,v, fi,v, and S i,v
END FOR
END IF
UNTIL: Run out of time;
RETURN: “not found”;
END:

Only two files, AmoebaD.v and varcells.v are required to synthesize the code to run on your FPGA. We have tested the implementation on an entry-level Spartan-7 Development board but expect it to run on any regular FPGA environment. When running, the FPGA SAT Solver performs the Amoeba inspired iterations and shows the progress by enabling 4 status LEDs (5% / 25% / 50% and 75% of the clauses are unsatisfied).

We demonstrated that the solver exhibits its powerful search ability for solving the SAT in a concurrent fashion. It is a hybrid of chaotic oscillatory dynamics and spatiotemporal control dynamics.

The complete source-code of the implementation is available on our GitHub repository. More of our research and work into physics and bio inspired computing is also available on our page.