Characteristic Subsets of SMT-LIB Benchmarks

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F21%3A00353737" target="_blank" >RIV/68407700:21730/21:00353737 - isvavai.cz</a>

Result on the web

<a href="http://sat.inesc-id.pt/~mikolas/smt-clustering.pdf" target="_blank" >http://sat.inesc-id.pt/~mikolas/smt-clustering.pdf</a>

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Characteristic Subsets of SMT-LIB Benchmarks

Original language description

A typical challenge faced when developing a parametrized solver is to evaluate a set of strategies over a set of benchmarking problems. When the set of strategies is large, the evaluation is often done with a restricted time limit and/or on a smaller subset of problems in order to estimate the quality of the strategies in a reasonable time. Firstly, considering the standard SMT-LIB benchmarks, we ask the question how much the time evaluation limit and benchmark size can be restricted to still obtain reasonable performance results. Furthermore, we propose a method to construct a benchmark characteristic subset which faithfully characterizes all benchmark problems. To achieve this, we collect problem performance statistics and employ clustering methods. We evaluate the quality of our benchmark characteristic subsets on the task of the best cover construction, and we compare the results with randomly selected benchmark subsets. We show that our method achieves smaller relative error than random problem selection

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/LL1902" target="_blank" >LL1902: Powering SMT Solvers by Machine Learning</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2021

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Proceedings of the 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification(CAV 2021)

ISBN

—

ISSN

1613-0073

e-ISSN

1613-0073

Number of pages

11

Pages from-to

53-63

Publisher name

CEUR Workshop Proceedings

Place of publication

Aachen

Event location

Los Angeles

Event date

Jul 18, 2021

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—