Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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.
Series
IT, 16003
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:uu:diva-273787OAI: oai:DiVA.org:uu-273787DiVA: diva2:895083
Supervisors
Examiners
Available from: 2016-01-18 Created: 2016-01-18 Last updated: 2016-01-18Bibliographically approved

Open Access in DiVA

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

By organisation
Department of Information Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 115 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

urn-nbn

Altmetric score

urn-nbn
Total: 247 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf