Full Text Available
Note: Clicking the button above will open the full text document at the original institutional repository in a new window.
Optimised constraint solving for real-world problems
Thesis (MSc)--Stellenbosch University, 2019.
Saved in:
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | en_ZA |
| Published: |
Stellenbosch : Stellenbosch University
2019
|
| Subjects: | |
| Tags: |
No Tags, Be the first to tag this record!
|
| _version_ | 1867613886477238272 |
|---|---|
| access_status_str | Open Access |
| author | Taljaard, Johannes Hendrik |
| author2 | Visser, Willem |
| author_browse | Taljaard, Johannes Hendrik Visser, Willem |
| author_facet | Visser, Willem Taljaard, Johannes Hendrik |
| author_sort | Taljaard, Johannes Hendrik |
| collection | Thesis |
| dc_rights_str_mv | Stellenbosch University |
| description | Thesis (MSc)--Stellenbosch University, 2019. |
| format | Thesis |
| id | oai:scholar.sun.ac.za:10019.1/107292 |
| institution | Stellenbosch University (South Africa) |
| language | en_ZA |
| last_indexed | 2026-06-10T12:43:15.981Z |
| license_str | Other — see source repository |
| provenance_str_mv | Harvested via OAI-PMH from SUNScholar — Stellenbosch University Repository |
| publishDate | 2019 |
| publishDateRange | 2019 |
| publishDateSort | 2019 |
| publisher | Stellenbosch : Stellenbosch University |
| publisherStr | Stellenbosch : Stellenbosch University |
| record_format | dspace |
| source_str | SUNScholar — Stellenbosch University Repository |
| spelling | oai:scholar.sun.ac.za:10019.1/107292 Optimised constraint solving for real-world problems Taljaard, Johannes Hendrik Visser, Willem Geldenhuys, Jaco Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Division Computer Science. Factorization of operators Constrained optimazition Satisfiability Modulo Theories (SMT) Cache memory Information storage and retrieval systems UCTD Thesis (MSc)--Stellenbosch University, 2019. ENGLISH ABSTRACT: Although significant advances in constraint solving technologies have been made during the past decade, Satisfiability Modulo Theories (SMT) solvers are still a significant bottleneck in verifying program properties. To overcome the performance issue, different caching strategies have been developed for constraint solution reuse. One of the first general frameworks for doing such caching was implemented in a tool called Green. Green allows extensive customisation, but in its basic form it splits a constraint to be checked into its independent parts (called factorisation), performs a canonisation step (including renaming and reordering of variables) and looks up results in a cache. More recently an alternative approach was suggested: rather than looking up sat or unsat results in a cache, it stores models (in the satisfiable case) and unsatisfiable cores (in the unsatisfiable case), and re uses these objects to establish the result of new constraints. This model reuse approach is re-implemented in Green and investigated further with an extensive evaluation against various Green configurations as well as incremental sat solving. The core findings highlight that the factorisation step is the crux of the different aching strategies.The results shed new light on the true benefits and weaknesses of the respective approaches. AFRIKAANSE OPSOMMING: Alhoewel daar die afgelope dekade aansienlike vordering met beperking-oplos tegnologieë gemaak is, is Bevredigbare Modulo Teorieë (BMT) oplossers steeds ’n belangrike knelpunt in die verifiëring van programme se eienskappe. Deur die werkverrigting kwessie te oorkom, is verskillende stoorstrategieë ontwikkel vir die hergebruik van beperkinge se oplossings. Een van die eerste algemene raamwerke om sulke stoorwerk te doen, is geïmplementeer in ’n program genaamd Green. Green laat uitgebreide aanpassing toe, maar in sy basiese vorm verdeel dit ’n beperking in sy onafhanklike dele (genaamd faktorisering), voer ’n kanoniseringsstap uit (insluitend die hernoem en herrangskik van veranderlikes) en soek resultate in ’n kasgeheue. Meer onlangs is ’n alternatiewe benadering voorgestel: waar in plaas van bevredigend of onbevredigend waardes in ’n kasgeheue op te soek, dit modelle (in die bevredigende geval) en onbevredigende kerns (in die onbevredigende geval) stoor, word hierdie voorwerpe hergebruik as die resultaat van nuwe beperkinge. Hierdie nuwe modelhergebruik-benadering word geïmplementeer in Green en word verder ondersoek met ’n uitgebreide evaluering teen verskillende Green-konfigurasies sowel as inkrementele bevredigbare-oplossing. Die kernbevindinge beklemtoon dat die faktoriseringstap die kern van die verskillende stoorstrategieë is. Die resultate werp nuwe lig op die werklike voordele en swakhede van die onderskeie benaderings. Masters 2019-11-25T13:36:33Z 2019-12-11T06:57:18Z 2019-11-25T13:36:33Z 2019-12-11T06:57:18Z 2019-12 Thesis http://hdl.handle.net/10019.1/107292 en_ZA Stellenbosch University x, 80 pages application/pdf Stellenbosch : Stellenbosch University |
| spellingShingle | Factorization of operators Constrained optimazition Satisfiability Modulo Theories (SMT) Cache memory Information storage and retrieval systems UCTD Taljaard, Johannes Hendrik Optimised constraint solving for real-world problems |
| title | Optimised constraint solving for real-world problems |
| title_full | Optimised constraint solving for real-world problems |
| title_fullStr | Optimised constraint solving for real-world problems |
| title_full_unstemmed | Optimised constraint solving for real-world problems |
| title_short | Optimised constraint solving for real-world problems |
| title_sort | optimised constraint solving for real world problems |
| topic | Factorization of operators Constrained optimazition Satisfiability Modulo Theories (SMT) Cache memory Information storage and retrieval systems UCTD |
| url | http://hdl.handle.net/10019.1/107292 |
| work_keys_str_mv | AT taljaardjohanneshendrik optimisedconstraintsolvingforrealworldproblems |