From MBQI to Enumerative Instantiation and Back
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866913993575104512 |
|---|---|
| author | Dančo, Marek Hozzová, Petra Janota, Mikoláš |
| author_facet | Dančo, Marek Hozzová, Petra Janota, Mikoláš |
| contents | This work investigates the relation between model-based quantifier instantiation (MBQI) and enumerative instantiation (EI) in Satisfiability Modulo Theories (SMT). MBQI operates at the semantic level and guarantees to find a counterexample to a given a non-model. However, it may lead to weak instantiations. In contrast, EI strives for completeness by systematically enumerating terms at the syntactic level. However, such terms may not be counter-examples. Here we investigate the relation between the two techniques and report on our initial experiments of the proposed algorithm that combines the two. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_22584 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | From MBQI to Enumerative Instantiation and Back Dančo, Marek Hozzová, Petra Janota, Mikoláš Logic in Computer Science This work investigates the relation between model-based quantifier instantiation (MBQI) and enumerative instantiation (EI) in Satisfiability Modulo Theories (SMT). MBQI operates at the semantic level and guarantees to find a counterexample to a given a non-model. However, it may lead to weak instantiations. In contrast, EI strives for completeness by systematically enumerating terms at the syntactic level. However, such terms may not be counter-examples. Here we investigate the relation between the two techniques and report on our initial experiments of the proposed algorithm that combines the two. |
| title | From MBQI to Enumerative Instantiation and Back |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2506.22584 |