CN111159631B - Hardware SAT solver based on programmable logic - Google Patents
Hardware SAT solver based on programmable logic Download PDFInfo
- Publication number
- CN111159631B CN111159631B CN201911416673.4A CN201911416673A CN111159631B CN 111159631 B CN111159631 B CN 111159631B CN 201911416673 A CN201911416673 A CN 201911416673A CN 111159631 B CN111159631 B CN 111159631B
- Authority
- CN
- China
- Prior art keywords
- module
- argument
- clauses
- break
- probability
- Prior art date
- Legal status (The legal status is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the status listed.)
- Active
Links
Classifications
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING OR COUNTING
- G06F—ELECTRIC DIGITAL DATA PROCESSING
- G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
- G06F17/10—Complex mathematical operations
-
- Y—GENERAL TAGGING OF NEW TECHNOLOGICAL DEVELOPMENTS; GENERAL TAGGING OF CROSS-SECTIONAL TECHNOLOGIES SPANNING OVER SEVERAL SECTIONS OF THE IPC; TECHNICAL SUBJECTS COVERED BY FORMER USPC CROSS-REFERENCE ART COLLECTIONS [XRACs] AND DIGESTS
- Y02—TECHNOLOGIES OR APPLICATIONS FOR MITIGATION OR ADAPTATION AGAINST CLIMATE CHANGE
- Y02D—CLIMATE CHANGE MITIGATION TECHNOLOGIES IN INFORMATION AND COMMUNICATION TECHNOLOGIES [ICT], I.E. INFORMATION AND COMMUNICATION TECHNOLOGIES AIMING AT THE REDUCTION OF THEIR OWN ENERGY USE
- Y02D10/00—Energy efficient computing, e.g. low power processors, power management or thermal management
Landscapes
- Engineering & Computer Science (AREA)
- Physics & Mathematics (AREA)
- Theoretical Computer Science (AREA)
- Mathematical Physics (AREA)
- Data Mining & Analysis (AREA)
- General Physics & Mathematics (AREA)
- Mathematical Analysis (AREA)
- Mathematical Optimization (AREA)
- Computational Mathematics (AREA)
- Pure & Applied Mathematics (AREA)
- Databases & Information Systems (AREA)
- Software Systems (AREA)
- General Engineering & Computer Science (AREA)
- Algebra (AREA)
- Devices For Executing Special Programs (AREA)
Abstract
The invention provides a hardware SAT solver based on programmable logic, which comprises a preprocessing module and an FPGA module. According to the invention, the hardware SAT solver is established by utilizing the programmable logic, the initial assignment of the variable elements is preprocessed, the searching trend of the optimal true value assignment is guided in advance, and the variable elements are turned over by searching the probability corresponding to the pre-stored probability mapping table preferentially during solving, so that the technical problems of complex algorithm, low efficiency and low solving success rate of the existing software SAT solver are solved, the additional time expenditure is reduced, the solving process of the solver is further accelerated, and the SAT problem with relatively large scale can be solved more efficiently and conveniently.
Description
Technical Field
The invention belongs to the technical field of computers, and particularly relates to a SAT solver, in particular to a hardware SAT solver based on programmable logic.
Background
In the SAT problem (satisifiability problem, boolean satisfiability problem), a set of finite element sets x= { X is given 1 ,x 2 ,…,x n }，x n Can be assigned a value of true (1) Or false (0), literal l i Is the argument x i Or negation ofAnd hasClause C is formed by word disjunctive (meaning of OR) and conjunctive paradigm CNF (conjectured normal formula) formula ++>Is formed by combining multiple clauses, such as +.> I.e. a CNF formula consisting of 5 arguments and 4 clauses. Any text in the clause is assigned true, and the clause is true or satisfied; if all characters in the clause are assigned false at the same time, then the clause is assigned to be false, or the clause is not satisfied by the assignment, and the formula isIs satisfied if and only if all clauses are satisfied at the same time. The SAT problem refers to finding a set of assignments X' for all arguments on X, X→ {0,1}, such that +.>Is true. If such assignment is present, then +.>Is satisfactory; if no such assignment exists +.>Is not satisfactory.
The SAT problem was proven by steve-kuk (Steven Cook) in 1971 to be an NP-complete problem, which means that it can be solved very quickly in polynomial time, and all other problems of the NP class can be ascribed to SAT problems in polynomial time. The most straightforward, crude way to solve the SAT problem is by enumeration, i.e. trying to input all possible assignments of arguments, however, the solution time of such an algorithm grows exponentially with the number of arguments.
Algorithms that solve the SAT problem, also known as SAT solvers, have made tremendous progress over the past decades. Problems that were considered to be unsolvable more than ten years ago can now be solved in a few seconds with advanced SAT solvers. Modern SAT solvers may integrate more advanced solving techniques by which software solvers developed can solve even the difficult SAT problem of how many millions of arguments.
When the SAT solver attempts to solve a problem, it fully or partially initializes the argument (denoted by α and β, respectively). For formula (VI)The full assignment is to assign 0 or 1 to each argument in the formula, such as α= (x) 1 ＝1,x 2 ＝0,x 3 ＝1,x 4 ＝1,x 5 =1). Conversely, a partial assignment is a subset assignment to a set of formula arguments, such as β= (x) 1 ＝1,x 2 =0). The assignment to the formula should follow the rules of boolean logic. For example, if one or more words in a clause are true (i.e., have a value of 1), then the clause is satisfied and can be deleted from the formula. If the formula is empty (i.e., there are no more clauses to satisfy), the formula satisfies. Conversely, if the word in the clause is false, the word may be deleted from the clause. Thus, if a clause is empty, then the clause cannot be satisfied, and the simplified formula is not satisfied.
The traditional SAT solver is realized by software, the solving algorithm is divided into a complete algorithm and an incomplete algorithm, the complete algorithm searches the solution space of the SAT formula thoroughly, the satisfaction conclusion of a certain SAT formula can be obtained in theory, but the SAT problem belongs to the NP problem, the solution space of the SAT problem grows exponentially along with the variable number of the formula, so the algorithm has lower efficiency and is not suitable for solving the large-scale SAT problem. The incomplete algorithm does not search the whole solution space, but searches the partial solution space by adopting various methods, the solution speed is higher, but the satisfaction of judging the SAT problem can not be ensured. With the dramatic increase in the size of actual SAT problems, software solvers have not been able to quickly and efficiently determine the satisfiability of the SAT problem.
Disclosure of Invention
Aiming at the defects related to the background technology, the invention provides a hardware SAT solver based on programmable logic, which is used for solving the technical problems of complex algorithm, low efficiency and low solving success rate of a software SAT solver in the prior art.
In order to solve the technical problems, the invention adopts the following technical scheme:
a programmable logic-based hardware SAT solver, comprising: the device comprises a preprocessing module and an FPGA module. The preprocessing module is used for generating initial assignment of each argument of the CNF formula, clauses which cannot be met under the current assignment, clauses of the CNF formula and argument information, and sending the clauses and argument information to the FPGA module; the FPGA module is used for receiving the initial assignment of each argument of the CNF formula sent by the preprocessing module, failing to meet clauses, and turning the argument according to a certain probability within the designated times to judge whether the CNF formula can be met.
Further, the FPGA module includes a first memory module. Receiving clauses and argument information of a CNF formula sent by a preprocessing module, wherein the clauses and argument information comprise: and the FPGA module stores the clause and the argument information of the CNF formula sent by the preprocessing module in a first storage module.
Further, the FPGA module further comprises a first evaluation module, a second storage module, a counter module, an argument overturning module, a probability mapping table, a FIFO tree and a second evaluation module. The first evaluation module is used for storing the initial assignment of each argument of the CNF formula, calculating whether the clauses stored in the first storage module are satisfied, and storing the clauses which are not satisfied in the second storage module; the counter module is used for calculating the break-value of each argument in the second storage module after being overturned and sequencing the break-value; the probability mapping table is used for storing break-value values corresponding to different turning probabilities in advance; the argument overturning module is used for overturning the clause argument; the FIFO tree is used for storing clauses after the argument is turned over by the argument turning module; and the second evaluation module is used for reading the clause from the FIFO tree and judging whether the clause is satisfied.
Further, the FPGA module further comprises a cache module, a random number generation module and a circulation control module.
Further, the FPGA module turns over the argument according to pre-stored probability distribution data within the appointed times, and specifically comprises the following steps: the circulation control module circularly executes the following steps in the appointed times:
and reading the unsatisfiable clauses from the second storage module, and temporarily storing the unsatisfiable clauses to the cache module.
And turning words which cannot meet clauses in the cache module, calculating break-value values of the turned variable elements by the counter module, and sequencing the break-value values.
Comparing the break-value of each argument after sequencing with a probability mapping table, and if the break-value of the argument exists in the probability mapping table, generating a random number by a random number generation module, and selecting the argument corresponding to the break-value corresponding to the random number by an argument turning module to turn; if the break-value of the argument does not exist in the probability mapping table, the argument flipping module selects the argument corresponding to the minimum break-value to flip.
And storing the clauses with the inverted arguments into the FIFO tree.
The second evaluation module reads a clause from the FIFO tree and determines if the clause is satisfied.
And sending the unsatisfiable clause to the second storage module.
Further, the FPGA module further comprises an output module.
Further, the FPGA module determines whether the CNF is satisfied, specifically including:
after the circulation control module finishes executing the appointed times, the second storage module and the last stage FIFO of the FIFO tree are free from unsatisfiable clauses, the output module can output CNF, otherwise, the output module can output CNF unsatisfiable.
Further, the preprocessing module includes: the system comprises a full text word judging module, a text word assigning module, a negative text word assigning module and a probability assigning module.
Further, the preprocessing module generates initial assignment of each argument of the CNF formula, specifically including:
the full text judgment module judges whether each argument appears in the form of full text word or full negative text in the CNF formula; the text-word assignment module initially assigns 1 to the argument which appears in the form of all text words in the CNF formula; the negative text assignment module initially assigns 0 to the argument which appears in the form of the full negative text in the CNF formula; the probability assignment module generates an initial assignment to an argument in the CNF formula that does not appear in the form of all text words or all negative text words, according to the probability that the argument assumes a true value.
Preferably, the format of the CNF formula is a DIMACS format.
Further, the probability mapping table stores a plurality of corresponding groups of break-value values with highest occurrence probabilities in advance.
Preferably, the probability map stores in advance the corresponding 78 sets of break-value values having the highest occurrence probabilities.
Preferably, the FPGA module is a Xilinx Virtex-6 FPGA chip.
The invention has the following beneficial effects: the invention provides a hardware SAT solver based on programmable logic, which is established by utilizing the programmable logic, and the initial assignment of the argument is preprocessed, and the argument is turned over by searching the probability corresponding to a pre-stored probability mapping table preferentially during solving, so that the technical problems of complex algorithm, low efficiency and low solving success rate of the existing software SAT solver are solved, and the SAT problem with relatively large scale can be solved more efficiently and conveniently.
Drawings
FIG. 1 is a block diagram of one embodiment of a programmable logic based hardware SAT solver of the present invention;
FIG. 2 is a block diagram of an FPGA module of one embodiment of a programmable logic based hardware SAT solver of the present invention;
FIG. 3 is a block diagram of a preprocessing module of one embodiment of a programmable logic based hardware SAT solver of the present invention.
Detailed Description
The present invention will be described in further detail with reference to the accompanying drawings and examples. It should be understood that the specific embodiments described herein are for purposes of illustration only and are not intended to limit the scope of the invention.
The hardware SAT solver is realized by adopting a programmable logic (FPGA) -based technology, and the FPGA has been developed to a hundred million-level logic gate scale in recent years, so that the operation scale can cope with the solving of an actual SAT problem. The FPGA is used for developing the hardware SAT solver, so that the characteristics of a hardware processing speed block can be exerted, and the redesign of a hardware circuit can be avoided, and the hardware SAT solver is an efficient and practical SAT hardware solution.
In an alternative embodiment, the present invention provides a structure of a hardware SAT solver based on programmable logic, as shown in fig. 1, comprising a preprocessing module 1 and an FPGA module 2. The preprocessing module 1 is used for generating initial assignment of each argument of a CNF formula and sending the initial assignment to the FPGA module; the FPGA module 2 is used for receiving the initial assignment of each argument of the CNF formula sent by the preprocessing module, overturning the argument within the designated times according to the pre-stored probability distribution data, and judging whether the CNF formula can be met.
In this embodiment, a hardware SAT solver based on programmable logic is implemented, and the preprocessing module 1 is used to perform initial assignment on each argument of the CNF formula, extract clauses which cannot be satisfied under the current assignment, and clause and argument information of the CNF formula, and send the clause and argument information to the FPGA module 2. The preprocessing module 1 carries out certain constraint on the initial value assignment of each argument of the CNF formula, wherein the constraint comprises two aspects, namely, on one hand, the initial value of a specific argument is determined by using a pure text rule; on the other hand, for the argument which does not accord with the pure text rule, the probability that the value of the argument is true is calculated, so that the number of clauses which can be satisfied is increased as much as possible, and the occurrence of the situation that the algorithm falls into local optimum is reduced.
In this embodiment, the so-called plain text rule in the preprocessing module 1 is defined as that, in a conjunctive normal form CNF, if a proposition argument appears in the form of either all text characters or all negative text characters, then the text is called plain text. The rule that eliminates all clauses where the atomic formula appears positive or negative is called a plain text rule.
For example: CNF formula f=c 1 ∧c 2 ∧c 3 Wherein It is apparent that x 3 Is purely written, if x 3 The value is true, the satisfiability of the formula F is equivalent to +.>
Thus, given the conjunctive normal form formula F, the argument x i The initial assignment of (2) may be obtained by the following formula:
wherein p is i The probability that the argument is true is initially valued.
And after generating initial assignment of each argument of the CNF formula based on the pure text rule, the preprocessing module 1 sends the initial assignment to the FPGA module.
In the prior art, in the random local search type algorithm and other incomplete algorithms for solving the SAT problem, most of the incomplete algorithms are used for randomly generating a true value assignment as a searching starting point, so that the complexity of the problem can be greatly reduced by reasonable argument assignment, and the solving efficiency is improved. The SAT problem resembles a mathematical constraint problem, so the relationship between the arguments in the problem library and the solution space of the SAT problem can be analyzed first, and then the truth assignment of some of the arguments can be assigned. The constraint of initial assignment of all the arguments in the SAT example is adopted to guide the search trend of the assignment of the optimal true value in advance, so that the finding of the optimal solution is quickened, the turnover times in the search process are reduced, the solution space of the search is reduced, the extra time expenditure is reduced, and the solving process of the solver is quickened.
In this embodiment, a hardware SAT solver based on programmable logic is used for specifically executing and solving the SAT problem, that is, receiving initial assignment of each argument of the CNF formula sent by the preprocessing module, and turning over the argument according to pre-stored probability distribution data within a designated number of times, so as to determine whether the CNF formula can be satisfied.
In an alternative embodiment, the FPGA module 2 is shown in block diagram form in figure 2. In this embodiment, the FPGA module includes a first storage module 201, configured to store clauses and argument information of the CNF formula sent by the preprocessing module and received by the FPGA. That is, the FPGA module receives clauses and argument information of the CNF formula sent by the preprocessing module, and specifically includes: and the FPGA module stores the clause and the argument information of the CNF formula sent by the preprocessing module in the first storage module.
The FPGA module further comprises a first evaluation module 202, a second storage module 203, a counter module 204, an argument flipping module 207, a probability mapping table 205, a FIFO tree 208 and a second evaluation module 209.
In this embodiment, the first evaluation module 202 is configured to store the initial assignment of each argument of the CNF formula sent by the preprocessing module and received by the FPGA, calculate whether the clause stored in the first storage module 201 is satisfied, and store the clause that is not satisfied in the second storage module 203.
The counter module 204 is configured to calculate a break-value of each argument in the second storage module 203 after being flipped, and order the break-value.
The probability mapping table 205 is configured to store, in advance, break-value values corresponding to different flip probabilities. In the prior art, the break-value of an argument is defined as: given the CNF formula F, the value α and the argument x of all the arguments, when the argument x is flipped, the clauses originally satisfied before the flipping may become unsatisfiable, and the number of clauses that are truly spurious is the break-value of the argument x, and is denoted as break (x, F, α).
The argument flipping module 207 is configured to flip clause arguments.
FIFO tree 208 for storing clauses after the argument is flipped by argument flipping module 207.
A second evaluation module 209 is configured to read the clause from the FIFO tree 208 and determine whether the clause is satisfied.
The implementation of exponential or polynomial functions in FPGA can bring significant time and area overhead, so how to quickly and effectively select the most suitable argument in each argument flipping process is critical. In theory, it is possible to generate 7 for the random 3-SAT problem 3 The number of combinations is =343, but in practice, when 3 arguments have the same break-value, the probability of each argument flipping is equal, and is 0.33, such as (0, 0), (1, 1), and so on. Similarly, the probability of an argument having the same break-value being flipped is also fixed for different permutations of the same set of break-value values. E.g. c after flipping the argument 1 ＝(l 1 ,l 2 ,l 3 ) And c 2 ＝(l 4 ,l 5 ,l 6 ) The corresponding break-value values are (0, 1, 2) and (1,2,0), respectively, for word l 1 And l 6 Which is the same for the transition probabilities of the strain elements. Likewise, l 2 And l 4 ，l 3 And l 5 The flip probabilities of (2) are also equal. Based on the two principles, the random 3-SAT problem with the average maximum value of break-value of 6 is shared by the actually generated combination numbers The probability distribution for each combination is shown in the following table.
For the random 3-SAT problem, the probability of occurrence of the case that the value of break-value is more than or equal to 7 is extremely low, and even if the value of break-value is more than or equal to 7 after the argument is turned over, the probability of being selected is extremely low according to the probability distribution function, because more unsatisfiable clauses are generated when the argument is selected, and the situation that an algorithm needs to avoid as much as possible is solved. In contrast, for arguments with smaller break-value values, the probability of being selected is relatively greater and the search process is more likely to converge.
In order to optimize the probability data storage structure, before solving starts, the probability mapping table 205 stores a plurality of corresponding groups of break-value values with highest occurrence probability in advance, particularly, the break-value values corresponding to the argument in 78 probability distributions with highest occurrence probability in the above table are ordered, and then all data are sequentially downloaded to the on-chip memory of the FPGA, that is, the probability mapping table 205 stores the 78 corresponding groups of break-value values with highest occurrence probability in advance. The solving efficiency can be effectively improved by looking up a table instead of directly calculating the distribution function.
In this embodiment, the FPGA module further includes a buffer module 211, a random number generation module 206, and a loop control module 212.
When solving the SAT problem, the FPGA module turns over the argument according to pre-stored probability distribution data within the designated times, and specifically comprises the following steps:
the loop control module 212 loops the following steps within a specified number of times:
the clauses which cannot be satisfied are read from the second storage module 203 and temporarily stored in the buffer module 211, and the buffer module 211 is the RAM of the FPGA module.
The text that cannot satisfy the clause is flipped in the caching module 211, and the counter module 204 calculates the break-value after each argument is flipped and sorts the break-value.
Comparing the break-value of each argument after sorting with the probability mapping table 205, if the break-value of the argument exists in the probability mapping table 205, generating a random number by the random number generation module 206, and turning over the argument corresponding to the break-value corresponding to the random number by the argument turning module 207; if the break-value of the argument does not exist in the probability map, the argument rollover module 207 selects the argument corresponding to the minimum break-value for rollover.
The argument flipped clause is stored to FIFO tree 208. The unsatisfiable clauses caused by the argument inversion are subjected to data aggregation through the multi-stage FIFO, and the newly generated unsatisfiable clauses are stored in the last-stage FIFO for subsequent processing.
The second evaluation module 209 reads a clause from the FIFO tree 208 and determines whether the clause is satisfied, and sends an unsatisfiable clause to the second storage module 203. Specifically, the second evaluation module 209 reads a clause from the last FIFO of the FIFO tree 208, and when the read clause is unsatisfiable, the clause is sent to the second storage module 203 for the next cycle of processing.
The FPGA module completes one-time argument overturning process, and the FPGA module is controlled by the circulation control module 212 to perform circulation processing for preset designated times, so that the whole solving process is completed.
In an alternative embodiment, the FPGA module further includes an output module 210.
When solving the SAT problem, the FPGA module judges whether the CNF formula can be satisfied or not, and specifically comprises the following steps:
after the loop control module 212 finishes executing the specified times, the second storage module 203 and the last stage FIFO of the FIFO tree 208 have no unsatisfiable clauses, and if not, the output module 210 outputs the CNF formula to be satisfied, otherwise, the output module 210 outputs the CNF formula to be unsatisfiable.
From this point on, the FPGA module completes the solution of the SAT problem and outputs whether the CNF formula is or is not satisfied.
In an alternative embodiment, the block diagram of the preprocessing module of the programmable logic based hardware SAT solver is shown in fig. 3, and includes a full text word judgment module 101, a text word assignment module 102, a negative text word assignment module 103, and a probability assignment module 104.
In the prior art, in the random local search type algorithm and other incomplete algorithms for solving the SAT problem, most of the incomplete algorithms are used for randomly generating a true value assignment as a searching starting point, so that the complexity of the problem can be greatly reduced by reasonable argument assignment, and the solving efficiency is improved. The SAT problem resembles a mathematical constraint problem, so the relationship between the arguments in the problem library and the solution space of the SAT problem can be analyzed first, and then the truth assignment of some of the arguments can be assigned. The constraint of initial assignment of all the arguments in the SAT example is adopted to guide the search trend of the assignment of the optimal true value in advance, so that the finding of the optimal solution is quickened, the turnover times in the search process are reduced, the solution space of the search is reduced, the extra time expenditure is reduced, and the solving process of the solver is quickened.
In this embodiment, the full text judgment module 101 is configured to judge whether each argument in the CNF is in the form of a plain text according to a plain text rule, where the plain text rule is defined as that in a conjunctive normal form CNF, if a propositional argument is in the form of either a full text word or a full negative text, then the text is called a plain text. The rule that eliminates all clauses where the atomic formula appears positive or negative is called a plain text rule.
For example: CNF formula f=c 1 ∧c 2 ∧c 3 Wherein It is apparent that x 3 Is purely written, if x 3 The value is true, the satisfiability of the formula F is equivalent to +.>
Briefly, the full text judgment module 101 is configured to judge whether each argument appears as either a full text word or a full negative text in the CNF formula.
In this embodiment, the text-word assignment module 102 is configured to initially assign 1 to an argument that appears as an all-text word in the CNF formula. The negative text assignment module 103 is configured to initially assign 0 to an argument that appears as a full negative text in the CNF formula. And for the argument which does not meet the plain text rule, generating initial assignment for the argument which does not appear in the form of all text words or all negative text words in the CNF formula by utilizing a probability assignment module according to the probability that the value of the argument is true.
Therefore, in this embodiment, the preprocessing module of the hardware SAT solver based on programmable logic generates initial assignment of each argument of the CNF formula, which specifically includes:
the full text judgment module 101 judges whether each argument appears in the CNF formula in the form of either a full text word or a full negative text.
The text-word assignment module 102 initially assigns 1 to an argument that appears as an all-text word in the CNF formula.
The negative text assignment module 103 initially assigns 0 to the argument that appears as a full negative text in the CNF formula.
The probability assignment module 104 generates an initial assignment of an argument in the CNF formula that does not appear in the form of all text words or all negative text words, according to the probability that the value of the argument is true.
That is, given the conjunctive normal form formula F, the argument x i The initial assignment of (2) may be obtained by the following formula:
wherein p is i The probability that the argument is true is initially valued.
And after generating initial assignment of each argument of the CNF formula based on the pure text rule, the preprocessing module 1 sends the initial assignment to the FPGA module.
In an alternative embodiment, the format of the CNF formula is DIMACS format, which is a simple CNF text format, with annotation hang1 starting with "c" and the 1 st behavior run parameter of the non-annotated line, the format is:
P cnf NUM_OF_VARIABLES NUM_OF_CLAUSES。
wherein num_of_variables represents the number OF boolean VARIABLES and num_of_clauses represents the number OF CLAUSES.
Each clause of the CNF formula corresponds to a row, the variables of one clause are denoted by reference numerals, positive values denote the variables as original variables, negative values denote the variables as inverted variables, the middle is separated by spaces, and the end of one clause is denoted by 0 at the end of each row.
For example, for a certain CNF formula, f=c 1 ∧c 2 ∧c 3 Wherein The DIMACS format can be expressed as:
c this is the annotation line
p cnf 6 3
-1 2 3 0
1 3 4 -5 0
-6 2 0
In an alternative embodiment, the FPGA module is an Xilinx Virtex-6 FPGA chip. The embodiment provides that a hardware SAT solver is executed and evaluated based on an Xilinx Virtex-6 FPGA chip. The Virtex-6 FPGA is based on a 40nm fabrication process employing a third generation Xilinx advanced silicon module (Advanced Silicon Modular Block, ASMBL) architecture, which implements the concept of supporting multiple domain-specific application platforms by using a unique column-based architecture. The Virtex-6 series FPGA perfectly combines advanced hardware chip technology, innovative circuit design technology and architectural enhancement, and compared with the prior generation of Virtex devices and competing FPGA products, the internal core voltage is only 1.0v, so that the power consumption is greatly reduced, the performance is higher and the cost is lower. XC6VHX565T is logically resource rich, contains up to 88k slots, each consisting of 4 look-up tables and 8 flip-flops, and 32kb on-chip ROM.
In this embodiment, an FPGA module in a hardware SAT solver based on programmable logic is implemented using an Xilinx Virtex-6 FPGA chip, and a preprocessing module compiles and executes in an Intel (R) Core (TM) i 5-64-bit 2.3GHz CPU 4.0GB RAM Linux Ubuntu-14.04 environment, and the hardware SAT solver based on programmable logic compiles and downloads the same to the Xilinx Virtex-6 FPGA chip, so as to solve the SAT problem.
In order to verify the performance of the hardware SAT solver based on programmable logic, 10 test cases with medium-sized random set are randomly selected from a test benchmark library of 2011 SAT competition, the problem scale is 350 variators, 1491 clauses to 800 variators and 3408 clauses, and the evaluation result shows that the hardware SAT solver has lower time complexity and better time performance and reaches the performance of an advanced software solver on the solving success rate.
The embodiment of the invention provides a hardware SAT solver based on programmable logic, which is established by utilizing the programmable logic, and is capable of pre-processing the initial assignment of the variable elements, guiding the searching trend of the optimal true value assignment in advance by pre-processing the constraint of the initial assignment of all the variable elements in the SAT instance, and solving the problem that the existing software SAT solver is complex in algorithm, low in efficiency and low in solving success rate, reducing additional time cost, accelerating the solving process of the solver, and solving the SAT problem of relatively large scale more efficiently and conveniently by searching the probability corresponding to a pre-stored probability mapping table to turn over the variable elements in solution instead of directly calculating a distribution function.
Although the preferred embodiments of the present invention have been disclosed for illustrative purposes, those skilled in the art will appreciate that various modifications, additions and substitutions are possible, and accordingly the scope of the invention is not limited to the embodiments described above. It will be apparent to those skilled in the art that modifications may be made without departing from the principles of the invention, and such modifications are intended to be within the scope of the invention.
Claims (7)
1. A hardware SAT solver based on programmable logic, the hardware SAT solver comprising: the device comprises a preprocessing module and an FPGA module;
the preprocessing module is used for generating initial assignment of each argument of a CNF formula, unsatisfiable clauses under current assignment, and clauses and argument information of the CNF formula, and sending the initial assignment, the unsatisfiable clauses and the argument information to the FPGA module;
wherein, the preprocessing module includes: the text word evaluation module, the text word assignment module, the negative text word assignment module and the probability assignment module;
the initial assignment of each argument of the CNF formula specifically comprises the following steps:
the full text judgment module judges whether each argument appears in the form of full text or full negative text in the CNF formula;
the text-word assignment module initially assigns 1 to an argument which appears in the form of all text words in a CNF formula;
the negative text assignment module initially assigns 0 to the argument which appears in the form of the negative text in the CNF formula;
the probability assignment module generates initial assignment to the argument which does not appear in the form of all text words or all negative words in the CNF formula according to the probability that the value of the argument is true;
the FPGA module is used for receiving the initial assignment of each argument of the CNF formula and unsatisfiable clauses sent by the preprocessing module, overturning the argument according to pre-stored probability distribution data within the designated times and judging whether the CNF formula can be satisfied;
the FPGA module comprises a first storage module;
the receiving the clause and the argument information of the CNF formula sent by the preprocessing module specifically comprises the following steps:
the FPGA module stores the clause and the argument information of the CNF formula sent by the preprocessing module in the first storage module;
the FPGA module further comprises a first evaluation module, a second storage module, a counter module, an argument overturning module, a probability mapping table, a FIFO tree and a second evaluation module;
the first evaluation module is used for storing initial assignment of each argument, calculating whether clauses stored in the first storage module are met or not, and storing the clauses which are not met in the second storage module;
the counter module is used for calculating the break-value of each argument in the second storage module after being turned over and sequencing the break-value;
the probability mapping table is used for storing break-value values corresponding to different turning probabilities in advance;
the argument overturning module is used for overturning the clause argument;
the FIFO tree is used for storing clauses after the argument is turned over by the argument turning module;
the second evaluation module is used for reading clauses from the FIFO tree and judging whether the clauses are satisfied.
2. The programmable logic-based hardware SAT solver of claim 1, wherein the FPGA module further comprises a cache module, a random number generation module, and a loop control module;
the FPGA module turns over the argument according to pre-stored probability distribution data within the appointed times, and specifically comprises the following steps:
the circulation control module circularly executes the following steps in the appointed times:
reading the unsatisfiable clauses from the second storage module and temporarily storing the unsatisfiable clauses to the cache module;
the characters which cannot meet the clauses are overturned in the cache module, and the counter module calculates the break-value of each overturned argument and sorts the break-value;
comparing the break-value values of the ordered variables with the probability mapping table, and if the break-value values of the variables exist in the probability mapping table, generating random numbers by the random number generation module, and turning the variables corresponding to the break-value values corresponding to the random numbers by the variable turning module; if the break-value of the argument does not exist in the probability mapping table, the argument overturning module selects the argument corresponding to the minimum break-value to overturn;
storing the clauses with the inverted argument into a FIFO tree;
the second evaluation module reads clauses from the FIFO tree and judges whether the clauses are satisfied;
and sending the unsatisfiable clause to the second storage module.
3. The programmable logic based hardware SAT solver of claim 2, wherein the FPGA module further comprises an output module;
the judging whether the CNF formula can be satisfied specifically includes:
after the circulation control module finishes executing the appointed times, the second storage module and the last stage FIFO of the FIFO tree can not meet clauses, the output module outputs the CNF formula to meet, otherwise, the output module outputs the CNF formula to meet.
4. The programmable logic based hardware SAT solver of claim 1, wherein the format of the CNF formula is a DIMACS format.
5. The programmable logic based hardware SAT solver of claim 1, wherein the probability map table pre-stores corresponding sets of break-value values with highest probability of occurrence.
6. The programmable logic based hardware SAT solver of claim 5, wherein the probability map table pre-stores the corresponding 78 sets of break-value values with highest probability of occurrence.
7. The programmable logic based hardware SAT solver of claim 1, wherein the FPGA module is an Xilinx Virtex-6 FPGA chip.
Priority Applications (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| CN201911416673.4A CN111159631B (en) | 2019-12-31 | 2019-12-31 | Hardware SAT solver based on programmable logic |
Applications Claiming Priority (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| CN201911416673.4A CN111159631B (en) | 2019-12-31 | 2019-12-31 | Hardware SAT solver based on programmable logic |
Publications (2)
| Publication Number | Publication Date |
|---|---|
| CN111159631A CN111159631A (en) | 2020-05-15 |
| CN111159631B true CN111159631B (en) | 2023-08-11 |
Family
ID=70560211
Family Applications (1)
| Application Number | Title | Priority Date | Filing Date |
|---|---|---|---|
| CN201911416673.4A Active CN111159631B (en) | 2019-12-31 | 2019-12-31 | Hardware SAT solver based on programmable logic |
Country Status (1)
| Country | Link |
|---|---|
| CN (1) | CN111159631B (en) |
Families Citing this family (2)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| CN112507656B (en) * | 2020-12-21 | 2024-07-16 | 深圳国微芯科技有限公司 | Boolean satisfiability verification method and system for chip logic design |
| CN112487740B (en) * | 2020-12-23 | 2024-06-18 | 深圳国微芯科技有限公司 | Boolean satisfiability problem solving method and system |
Citations (3)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| CN105745618A (en) * | 2014-03-25 | 2016-07-06 | 克莱顿·吉莱斯皮 | Solving NP-complete problem without hyper-polynomial cost |
| CN107609325A (en) * | 2017-10-18 | 2018-01-19 | 中国航空无线电电子研究所 | The method that fault tree based on SAT solves minimal cut set |
| CN109726362A (en) * | 2017-10-30 | 2019-05-07 | 中国科学院计算技术研究所 | Solve the local search method for solving and system for weighting maximum satisfiability problem |
-
2019
- 2019-12-31 CN CN201911416673.4A patent/CN111159631B/en active Active
Patent Citations (3)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| CN105745618A (en) * | 2014-03-25 | 2016-07-06 | 克莱顿·吉莱斯皮 | Solving NP-complete problem without hyper-polynomial cost |
| CN107609325A (en) * | 2017-10-18 | 2018-01-19 | 中国航空无线电电子研究所 | The method that fault tree based on SAT solves minimal cut set |
| CN109726362A (en) * | 2017-10-30 | 2019-05-07 | 中国科学院计算技术研究所 | Solve the local search method for solving and system for weighting maximum satisfiability problem |
Non-Patent Citations (1)
| Title |
|---|
| Kenji Kanazawa.An Approach for Solving Large SAT Problems on FPGA.《ACM Transactions on Reconfigurable Technology and Systems》.2010,第 第4卷卷(第第1期期),1-21页. * |
Also Published As
| Publication number | Publication date |
|---|---|
| CN111159631A (en) | 2020-05-15 |
Similar Documents
| Publication | Publication Date | Title |
|---|---|---|
| Friedmann et al. | Subexponential lower bounds for randomized pivoting rules for the simplex algorithm | |
| Tabuada et al. | Robust linear temporal logic | |
| Aloul et al. | Faster SAT and smaller BDDs via common function structure | |
| US20050171747A1 (en) | Method and system for non-linear state based satisfiability | |
| CN111159631B (en) | Hardware SAT solver based on programmable logic | |
| US4951225A (en) | Updating pattern-matching networks | |
| Charikar et al. | Fully dynamic almost-maximal matching: Breaking the polynomial worst-case time barrier | |
| Davis et al. | A practical reconfigurable hardware accelerator for Boolean satisfiability solvers | |
| Kondratyev et al. | Hazard-free implementation of speed-independent circuits | |
| Harris et al. | A comparison of genetic programming variants for hyper-heuristics | |
| CN111159628B (en) | Hardware SAT solver for multi-thread parallel execution | |
| CN111142944A (en) | Hardware SAT solver based on pipeline execution strategy | |
| Van Gelder | Generalized conflict-clause strengthening for satisfiability solvers | |
| Ali et al. | Parallelization of unit propagation algorithm for SAT-based ATPG of digital circuits | |
| Fiser et al. | On using permutation of variables to improve the iterative power of resynthesis | |
| Lange | Solving parity games by a reduction to SAT | |
| US11200056B2 (en) | Parallel union control device, parallel union control method, and storage medium | |
| Mrena et al. | Comparison of left fold and tree fold strategies in creation of binary decision diagrams | |
| CN116976248A (en) | Circuit design adjustment using redundant nodes | |
| Muhammad et al. | A stochastic non-CNF SAT solver | |
| Tiejun et al. | An Parallel FPGA SAT Solver Based on Multi‐Thread and Pipeline | |
| CN109684761B (en) | Wide exclusive nor circuit optimization method | |
| Shabana et al. | Using Sat solvers for synchronization issues in non-deterministic automata | |
| Siládi et al. | Adapted parallel Quine-McCluskey algorithm using GPGPU | |
| CN113435149B (en) | Test case automatic generation method for optimizing FPGA comprehensive effect |
Legal Events
| Date | Code | Title | Description |
|---|---|---|---|
| PB01 | Publication | ||
| PB01 | Publication | ||
| SE01 | Entry into force of request for substantive examination | ||
| SE01 | Entry into force of request for substantive examination | ||
| GR01 | Patent grant | ||
| GR01 | Patent grant |