Hardware SAT solver for multi-thread parallel execution

Abstract

The invention provides a hardware SAT solver for multi-thread parallel execution. The hardware SAT solver comprises a first register module, a first evaluation module group, a buffer module group, a counter module, a variable element overturning module, a probability mapping table, an FIFO tree group, a second register module group, a second evaluation module and a third register module. All the data is stored in an on-chip memory of an FPGA; time expenditure caused by reading off-chip data is avoided. Meanwhile, a multi-thread strategy is utilized; different threads interact with the same address mapping table and clause mapping table. Compared with the prior art, the invention has the advantages that the resource overhead of the on-chip memory is greatly reduced, the total flipping amount per second is multiplied due to the use of a multi-thread strategy, the solution of the problem is more likely to be found in the specified time, and the relatively large-scale SAT problem can be solved more efficiently and conveniently.

Description

technical field [0001] The invention belongs to the technical field of computers, and in particular relates to a SAT solver, in particular to a hardware SAT solver for multi-thread parallel execution. Background technique [0002] In the SAT problem (satisifiability problem, Boolean satisfiability problem), given a set of finite variable set X={x 1 ,x 2 ,...,x n}, x n Can be assigned true (1) or false (0), the literal l i is the variable x i or its negation and have Clause C is formed by text disjunction (meaning "or"), and the conjunction normal form CNF (conjectured normal formula) formula Formed by the conjunction of several clauses, such as That is, a CNF formula consisting of 5 variables and 4 clauses. If any word in a clause is assigned a value of true, then the clause is true or satisfied; if all the words in a clause are assigned a value of false at the same time, it is said that the specified assignment makes the clause false, or the specified assignm...

AI Technical Summary

Problems solved by technology

[0011] For hardware solvers based on full algorithms, the lack of sufficient fast memory is the main reason why previous work did not try multi-threaded BCP in hardware

For SRAM-based BCP accelerators, memory capacity is the limiting factor

Copying assignments of arguments (and possibly watched literal lists) is too expensive

Images