Find if a set of values satisfies a given Boolean equation.
Some examples:
Davis-Putman-Logemann-Loveland algorithm.
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)
By Tamkin04iut - asdfasf Previously published: asdfasf, CC BY-SA 3.0, https://commons.wikimedia.org/w/index.php?curid=25661587
By Tamkin04iut - asdfasf Previously published: asdfasf, CC BY-SA 3.0, https://commons.wikimedia.org/w/index.php?curid=25661587
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.
BCP implies a variable value.
So we can see "cascades" of propagation.
We cannot imply anything for d and e.
This part of the algorithm is worth accelerating.
Field Programmable Gate Array.
FPGA is by nature highly parallel, so it can be faster for some tasks.
Divide the work between two chips may be worth.
Deducts variable values from input values
Algorithm:
J. D. Davis, Zhangxi Tan, Fang Yu and Lintao Zhang, "A practical reconfigurable hardware accelerator for boolean satisfiability solvers"
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.
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 |
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 |
Address CID: [status0][status1][status2]...[status(n-1)] Status: 00: false 01: true 10: unassigned
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
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.
J. Thong and N. Nicolici, "FPGA acceleration of enhanced boolean constraint propagation for SAT solvers"
Clauses are fetched by linked list traversal.
Clauses are identified by their addresses.
K threads, N local links, M global links
4 steps:
Memory is usualy dual-ported.
Clause visit: 2 clock cycles.
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.
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.
Created by Maxence CARON--LASNE.