An Efficient Hardware Implementation of a SAT Problem Solver on FPGA
Bibliographic record
Abstract
A hardware analyzer for the Boolean satisfiability problem using a complete algorithm was developed for an Alter a DE2-70 Cyclone II FPGA board. In one clock cycle, all implications are computed, variables are assigned and all clauses are evaluated in parallel. Backtracking is done by means of a hardware stack occupying minimal memory resources. No memory is required to hold the potentially gigantic problem specification as a VHDL package is used by the HDL compiler to simplify the circuit (by propagating constants). Run-time comparisons were made using instances from the DIMACS suite with MiniSAT, one of the most efficient software solvers, revealing accelerations of up to 6.66, as well as with other state-of-the-art hardware SAT solvers where accelerations of 2 orders of magnitude were observed. Our approach demonstrates a high level of flexibility and scalability as the generated circuits have a very small FPGA footprint. The largest problem tested has 317 variables, 1264 clauses for a total of 3670 literals and occupies 20.47% of the FPGA used. Projections regarding circuit frequency and FPGA footprint for larger problems are also deduced to show the scalability of the approach.
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
How this classification was reachedexpand
Full frame machine prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. The Gemma side is a direct model label for every work in the frame, read from the title-only record. The Codex side is a classifier learned from the 10,348 direct Codex labels and calibrated to design-weighted sample rates; fields without enough sample support carry no Codex call. Candidate is the union of the two sides; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels.
Distilled classifier scores by category (both heads)
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.000 | 0.001 |
| Meta-epidemiology (narrow) | 0.001 | 0.000 |
| Meta-epidemiology (broad) | 0.001 | 0.001 |
| Bibliometrics | 0.001 | 0.001 |
| Science and technology studies | 0.000 | 0.000 |
| Scholarly communication | 0.001 | 0.001 |
| Open science | 0.001 | 0.000 |
| Research integrity | 0.000 | 0.001 |
| Insufficient payload (model declined to judge) | 0.023 | 0.005 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from itClassification
machine, unvalidatedMachine predicted; a candidate call from one source (direct Gemma or distilled Codex), not a consensus.
How this classification was reached, model by model and score by score, is at the end of the page under "How this classification was reached".