Browsing by Author "Taljaard, Johannes Hendrik"

Now showing 1 - 1 of 1
  • Thumbnail Image
    Item
    Optimised constraint solving for real-world problems
    (Stellenbosch : Stellenbosch University, 2019-12) Taljaard, Johannes Hendrik; Visser, Willem; Geldenhuys, Jaco; Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Division Computer Science.
    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.