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.
| Identifer | oai:union.ndltd.org:siu.edu/oai:opensiuc.lib.siu.edu:theses-3050 |
| Date | 01 December 2016 |
| Creators | Ahmadi, Ehsan |
| Publisher | OpenSIUC |
| Source Sets | Southern Illinois University Carbondale |
| Detected Language | English |
| Type | text |
| Format | application/pdf |
| Source | Theses |
Page generated in 0.0021 seconds