Optimised constraint solving for real-world problems
Date
2019-12
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Stellenbosch : Stellenbosch University
Abstract
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.
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.
Description
Thesis (MSc)--Stellenbosch University, 2019.
Keywords
Factorization of operators, Constrained optimazition, Satisfiability Modulo Theories (SMT), Cache memory, Information storage and retrieval systems, UCTD