Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


44238.pdf (1.75 MB)

ETD Abstract Container

Abstract Header

FPGA Based Complete SAT Solver

Kannan, Sai Surya
http://rave.ohiolink.edu/etdc/view?acc_num=ucin1668636428692387

Abstract Details

2022, MS, University of Cincinnati, Engineering and Applied Science: Electrical Engineering.
Boolean Satisfiability (SAT) is an NP-complete problem. It is used in several VLSI design applications such as design automation, design verification and automatic test pattern generation. A SAT solver is an algorithm which checks whether a given SAT problem is satisfiable. There are two kinds of SAT solvers, incomplete and complete solvers. Incomplete solvers are based on iterative stochastic local search (SLS) algorithms, which attempt to solve a set of clauses using randomized variable assignments. These solvers are effective for large problems and use various heuristics to determine the solution. The disadvantage with these types of solvers is that the algorithm usually cannot determine whether the problem is UNSAT and these types of solvers doesn’t guarantee to find a solution. Complete solvers use a systematic approach toward exploration. Conflict Driven Clause Learning (CDCL) algorithm is an improved version of the Davis–Putnam–Logemann–Loveland (DPLL) method in which the algorithm learns a new clause from a conflict and performs non-chronological backtracking to the root of the conflict. With this new clause, the algorithm will prevent this branch from being explored again. Over the past few years, Field Programmable Gate Array (FPGA) has been used to solve complex problems due to their superior computational capability. With FPGA’s parallel and pipeline processing power and its memory resources, it is an excellent platform to build and run SAT algorithms. This thesis presents a CDCL solver on the Xilinx Alveo U280 Accelerator card, using Vitis HLS. This solver incorporates some of the effective techniques and heuristics used in the modern SAT solvers such as Literal Block Distance (LBD) used for clause pruning, Variable State Independent Decaying Sum (VSIDS) for variable selection heuristics, Phase Saving, Watched Literals, Rapid Restarts (Luby Sequence) and Restart Skips. The FPGA solver is implemented in three different versions with changes in the post-processing steps, where the hardware kernel code remains the same. The solver can handle k-SAT problems. SAT competition benchmarks and randomly generated SAT problems are solved with up to 786 variables and 6094 clauses. The performance of this FPGA solver is compared with a state-of-the-art complete solver executing on a CPU.
Ranganadha Vemuri, Ph.D. (Committee Member)
Wen-Ben Jone, Ph.D. (Committee Member)
John Emmert, Ph.D. (Committee Member)
106 p.
Electrical Engineering
Boolean Satisfiability; Complete Solvers; FPGA; CDCL; Heterogeneous Computing; SAT Solvers

Recommended Citations

Citations

  • Kannan, S. S. (2022). FPGA Based Complete SAT Solver [Master's thesis, University of Cincinnati]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1668636428692387

    APA Style (7th edition)

  • Kannan, Sai Surya. FPGA Based Complete SAT Solver. 2022. University of Cincinnati, Master's thesis. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=ucin1668636428692387.

    MLA Style (8th edition)

  • Kannan, Sai Surya. "FPGA Based Complete SAT Solver." Master's thesis, University of Cincinnati, 2022. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1668636428692387

    Chicago Manual of Style (17th edition)

ucin1668636428692387
44
© 2022, all rights reserved.
This open access ETD is published by University of Cincinnati and OhioLINK.