Accelerating Boolean Constraint Propagation for Efficient SAT-Solving on FPGAs
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866917638719930368 |
|---|---|
| author | Govindasamy, Hariprasadh Esfandiari, Babak Garcia, Paulo |
| author_facet | Govindasamy, Hariprasadh Esfandiari, Babak Garcia, Paulo |
| contents | We present a hardware-accelerated SAT solver targeting processor/Field Programmable Gate Arrays (FPGA) SoCs. Our solution accelerates the most expensive subroutine of the Davis-Putnam-Logemann-Loveland (DPLL) algorithm, Boolean Constraint Propagation (BCP) through fine-grained FPGA parallelism. Unlike prior state-of-the-art solutions, our solver eliminates costly clause look-up operations by assigning clauses directly to clause processors on the FPGA and dividing large formulas into smaller partitions manageable by FPGA. Partitions are hot-swapped during runtime as required and the supported formula size is limited only by available external memory, not on-chip FPGA memory. We evaluate our solver on a Xilinx Zynq platform with results showing quicker execution time across various formula sizes, subject to formula partitioning strategy. Compared to prior state-of-the-art, we achieve 1.7x and 1.1x speed up on BCP for 2 representative benchmarks and up to 6x total speedup over software-only implementation. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_07429 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Accelerating Boolean Constraint Propagation for Efficient SAT-Solving on FPGAs Govindasamy, Hariprasadh Esfandiari, Babak Garcia, Paulo Hardware Architecture We present a hardware-accelerated SAT solver targeting processor/Field Programmable Gate Arrays (FPGA) SoCs. Our solution accelerates the most expensive subroutine of the Davis-Putnam-Logemann-Loveland (DPLL) algorithm, Boolean Constraint Propagation (BCP) through fine-grained FPGA parallelism. Unlike prior state-of-the-art solutions, our solver eliminates costly clause look-up operations by assigning clauses directly to clause processors on the FPGA and dividing large formulas into smaller partitions manageable by FPGA. Partitions are hot-swapped during runtime as required and the supported formula size is limited only by available external memory, not on-chip FPGA memory. We evaluate our solver on a Xilinx Zynq platform with results showing quicker execution time across various formula sizes, subject to formula partitioning strategy. Compared to prior state-of-the-art, we achieve 1.7x and 1.1x speed up on BCP for 2 representative benchmarks and up to 6x total speedup over software-only implementation. |
| title | Accelerating Boolean Constraint Propagation for Efficient SAT-Solving on FPGAs |
| topic | Hardware Architecture |
| url | https://arxiv.org/abs/2401.07429 |