Change search
ReferencesLink to record
Permanent link

Direct link
Normalization of SMT-LIB scripts
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
2016 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

Satisfiability modulo theories (SMT) is about determining the satisfiability of logical formulas over a range of one or more theories. SMT solvers are programs that are designed to determine the satisfiability of logical formulas and to find a satisfying model. Since the SMT problem is known to be NP-complete, the SMT initiative holds annual competitions to further advance and stimulate the techniques and tools used by the SMT community. To prevent unfair entries to the competition, a benchmark scrambler with a random seed is used to rename variables, randomly permutes arguments and hides benchmark names for each of the formulas. This paper is about researching the possibility of proving satisfiability of expressions that are semantically equal but not necessarily syntactical. The purpose of this project was to develop a computer program that is able to normalize benchmark scripts to a standard defined format such that by scrambling syntactically equal scripts would result in the same result when normalized. The implementation that was conceived is incomplete and inefficient for larger SMT scripts in terms of computational complexity due to time constraints however, the research of that was conceived during this thesis provides an interesting insight in the complexity of normalizing benchmark scripts and its relation to graph isomorphism.

Place, publisher, year, edition, pages
2016. , 50 p.
IT, 16003
National Category
Engineering and Technology
URN: urn:nbn:se:uu:diva-273787OAI: diva2:895083
Available from: 2016-01-18 Created: 2016-01-18 Last updated: 2016-01-18Bibliographically approved

Open Access in DiVA

fulltext(968 kB)34 downloads
File information
File name FULLTEXT01.pdfFile size 968 kBChecksum SHA-512
Type fulltextMimetype application/pdf

By organisation
Department of Information Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 34 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 47 hits
ReferencesLink to record
Permanent link

Direct link