Efficiently grounding FOL using bit vectors
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866914913376534528 |
|---|---|
| author | Van Laer, Lucas Vandevelde, Simon Vennekens, Joost |
| author_facet | Van Laer, Lucas Vandevelde, Simon Vennekens, Joost |
| contents | Several paradigms for declarative problem solving start from a specification in a high-level language, which is then transformed to a low-level language, such as SAT or SMT. Often, this transformation includes a "grounding" step to remove first-order quantification. To reduce the time and size of the grounding, it can be useful to simplify formulas along the way, e.g., by already taking into account the interpretation of symbols that are already known. In this paper, we investigate the use of bit vectors to efficiently simplify formulas, thereby taking advantage of the fact that, on modern hardware, logical operations on bit vectors can be executed extremely fast. We conduct an experimental analysis, which shows that bit vectors are indeed fast for certain problems, but also have limitations. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_07980 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Efficiently grounding FOL using bit vectors Van Laer, Lucas Vandevelde, Simon Vennekens, Joost Logic in Computer Science Several paradigms for declarative problem solving start from a specification in a high-level language, which is then transformed to a low-level language, such as SAT or SMT. Often, this transformation includes a "grounding" step to remove first-order quantification. To reduce the time and size of the grounding, it can be useful to simplify formulas along the way, e.g., by already taking into account the interpretation of symbols that are already known. In this paper, we investigate the use of bit vectors to efficiently simplify formulas, thereby taking advantage of the fact that, on modern hardware, logical operations on bit vectors can be executed extremely fast. We conduct an experimental analysis, which shows that bit vectors are indeed fast for certain problems, but also have limitations. |
| title | Efficiently grounding FOL using bit vectors |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2408.07980 |