English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

We present a hardware-accelerated SAT solver targeting processor/FieldProgrammable Gate Arrays (FPGA) SoCs. Our solution accelerates the mostexpensive 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 clauselook-up operations by assigning clauses directly to clause processors on theFPGA and dividing large formulas into smaller partitions manageable by FPGA.Partitions are hot-swapped during runtime as required and the supported formulasize is limited only by available external memory, not on-chip FPGA memory. Weevaluate our solver on a Xilinx Zynq platform with results showing quickerexecution time across various formula sizes, subject to formula partitioningstrategy. Compared to prior state-of-the-art, we achieve 1.7x and 1.1x speed upon BCP for 2 representative benchmarks and up to 6x total speedup oversoftware-only implementation.

Accelerating Boolean Constraint Propagation for Efficient SAT-Solving on FPGAs