Accelerate Boolean Constraint Propagation for Boolean Satisfiability Solvers with FPGA

Maxence CARON–LASNE

maxence.caron-lasne@lse.epita.fr

Satifiability problems and Boolean Constraint Propagation

Satisfiability problems

Find if a set of values satisfies a given Boolean equation.

Some examples:

Sorry, your browser does not support SVG.

Usecases

  • SMT solvers
  • Symbolic execution
  • Formal verification
  • Circuit synthesis

Conjunctive Normal Form

Sorry, your browser does not support SVG.

  • Clauses are composed of literals.
  • Literals are variables with a sign.
  • Clause size are not fix.
  • We tend to normalize the clause's size (3, 4, 16…).
  • 3-SAT, 4-SAT, k-SAT.

DPLL algorithm

Davis-Putman-Logemann-Loveland algorithm.

  • Backtracking-based.
def DPLL(CLAUSES):
        if CLAUSES is a consistant set of literals:
                return SAT

        if CLAUSES contains an empty clause:
                return UNSAT

        for every unit clause U in CLAUSES:
                CLAUSES = unit-propagate(U, CLAUSES)

        for every literal L that occurs pure in CLAUSES:
                CLAUSES = pure-literal-assign(L, CLAUSES)

        L = choose-literal(CLAUSES)

        return DPLL(CLAUSES and L) or DPLL(CLAUSES and not L)

DPLL example

dpll_example_2.png

By Tamkin04iut - asdfasf Previously published: asdfasf, CC BY-SA 3.0, https://commons.wikimedia.org/w/index.php?curid=25661587

DPLL example

dpll_example.png

By Tamkin04iut - asdfasf Previously published: asdfasf, CC BY-SA 3.0, https://commons.wikimedia.org/w/index.php?curid=25661587

Boolean Constraint Propagation

Also called unit-propagation.

In a clause, if all literals but one are assigned and false, the last literal must be assigned to true to satisfies the clause.

Sorry, your browser does not support SVG.

Cascade effect

BCP implies a variable value.

  • So, no choice to make.
  • Free implication.
  • Free infered variable.

So we can see "cascades" of propagation.

Example of cascade effect

Sorry, your browser does not support SVG.

We cannot imply anything for d and e.

Hardware acceleration?

Is BCP worth accelerating?

  • BCP is part of any software SAT solvers.
  • BCP is useful to prune branches.
  • BCP takes 80%-90% of CPU time because of cascades of implications.

This part of the algorithm is worth accelerating.

What is an FPGA?

Field Programmable Gate Array.

  • Array of programmable logic blocks (gate).
  • Logic blocks can be wired together.
  • User can implements complex logic function and synthetise it on FPGA.

FPGA is by nature highly parallel, so it can be faster for some tasks.

Why FPGA?

  • The DPLL algorithm is a branching algorithm.
  • The BCP is a simple operation executed many times.

Divide the work between two chips may be worth.

  • Branching algorithm: CPU
  • Little operation with many workers: FPGA

cpu_to_fpga.png

General BCP Algorithm

General BCP Algorithm

Deducts variable values from input values

io.png

Algorithm:

  1. Fetch list of clauses
  2. Fetch variable assignments
  3. Verify if the clause is an unit clause
  4. Update assignments

Many Inference Engines design

Many Inference Engines design

J. D. Davis, Zhangxi Tan, Fang Yu and Lintao Zhang, "A practical reconfigurable hardware accelerator for boolean satisfiability solvers"

total_project.png

Inference engine

infengine.png

Clause partitionning

Each Inference Engine has only one occurence of a single variable.

At each BCP, a single Inference Engine can only find a single inference.

So the Inference Engine find the inference in a fixed number of clock cycles.

Clause fetching

  • Naive solution: just an array.
Index Match Index Match
0000 No Match 1000 No Match
0001 CID: 1; PID: 1 1001 No Match
0010 No Match 1010 No Match
0011 No Match 1011 No Match
0100 No Match 1100 CID: 2; PID: 1
0101 No Match 1101 CID: 2; PID: 2
0110 No Match 1110 CID: 1; PID: 2
0111 No Match 1111 No Match
  • Problem: the array is too sparse.

Clause tree walking

clause_trie.png

Trie memory representation

The data is less sparse.

Index Match Index Match
0000 Base index: 0100 0110 No Match
0001 No Match 0111 No Match
0010 No Match 1000 CID: 2; PID: 1
0011 Base index: 1000 1001 CID: 2; PID: 2
0100 No Match 1010 CID: 1; PID: 2
0101 CID: 1; PID: 1 1011 No Match

Clause status fetching

  • A clause is identified with its CID.
  • Putting clause status in an array is OK.
Address CID: [status0][status1][status2]...[status(n-1)]

Status:
00: false
01: true
10: unassigned

Inference computation

00 00 00 00 10 00 00 00
___________    ________
  HI(i)      i   LO(i)

is_implication(i) = HI(i) == LO(i) == 0 and lit(i) == unassigned
for i in sizeof(clause_entry):
    ret[i] = clause[:i] == 0 and clause[i+1:] == 0 and clause[i] == UNASSIGN
  • It is a combinational operation, it is done in one clock cycle.

Results

250 MHz

SAT Instance Clause-Variable Ratio Number of clock cycles
miters-c3540 2.70 7
miters-c5315 2.96 9
miters-c880 5.08 12
bmc-galileo-8 5.08 5
bmc-ibm-12 4.67 6
crypto-md4 4.16 10
crypto-md5 4.17 11

Supports up to 64,000 variables and clauses.

x5 to x16 speedup relative to contemporary SAT Solvers.

Sequencial Clause Traversal design

Sequencial Clause Traversal design

J. Thong and N. Nicolici, "FPGA acceleration of enhanced boolean constraint propagation for SAT solvers"

Sorry, your browser does not support SVG.

Clauses fetching

Clauses are fetched by linked list traversal.

Sorry, your browser does not support SVG.

Implications fetching

Clauses are identified by their addresses.

Sorry, your browser does not support SVG.

K threads, N local links, M global links

Clause walking

Sorry, your browser does not support SVG.

Memory accesses

4 steps:

Sorry, your browser does not support SVG.

Memory is usualy dual-ported.

Clause visit: 2 clock cycles.

Results

250 MHz

Nbr of clauses Nbr of variables Max Clause Size Number of clock cycles
500 225 6 46.7
500 200 4 28.0
500 200 3 21.3

Supports up to 250,000 variables and clauses.

x2 speed up.

Conclusion

  • The two designs are efficient in terms of speed.
  • The two designs only works on little SAT instances.

Bibliography

J. D. Davis, Zhangxi Tan, Fang Yu and Lintao Zhang, "A practical reconfigurable hardware accelerator for boolean satisfiability solvers," 2008 45th ACM/IEEE Design Automation Conference, Anaheim, CA, 2008, pp. 780-785.

Davis J.D., Tan Z., Yu F., Zhang L. (2008) Designing an Efficient Hardware Implication Accelerator for SAT Solving. In: Kleine Büning H., Zhao X. (eds) Theory and Applications of Satisfiability Testing – SAT 2008. SAT 2008. Lecture Notes in Computer Science, vol 4996. Springer, Berlin, Heidelberg

J. Thong and N. Nicolici, "FPGA acceleration of enhanced boolean constraint propagation for SAT solvers," 2013 IEEE/ACM International Conference on Computer-Aided Design (ICCAD), San Jose, CA, 2013, pp. 234-241.

Questions?

Thank you!

Created by Maxence CARON--LASNE.