Date of Award
12-1-2016
Degree Name
Master of Science
Department
Electrical and Computer Engineering
First Advisor
Tragoudas, Spyros
Abstract
Many problems in nature can be represented as some kind of a satisfiability problem. Several SAT solvers and SMT solvers have been developed in the last decade with the goal of checking the satisfiability of different SAT problems. An all-solution satisfiability modulo theories on top of the Z3 SMT solver is presented that uses the clause blocking algorithm to find all the solution sets of a SAT problem. Then, an incremental All-SMT solver has been presented based on the all-SMT solver which is able to find the satisfiable answers of an incremental SMT problem based on the solution set of the original problem.
Access
This thesis is only available for download to the SIUC community. Current SIUC affiliates may also access this paper off campus by searching Dissertations & Theses @ Southern Illinois University Carbondale from ProQuest. Others should contact the interlibrary loan department of your local library or contact ProQuest's Dissertation Express service.