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.

Share

COinS
 

Access

This thesis is only available for download to the SIUC community. Others should
contact the interlibrary loan department of your local library.