Integrating cardinality constraints into constraint logic programming with sets

Formal reasoning about finite sets and cardinality is important for many applications, including software verification, where very often one needs to reason about the size of a given data structure. The Constraint Logic Programming tool {log} (‘setlog’) provides a decision procedure for deciding the...

Descripción completa

Detalles Bibliográficos
Autores principales: Cristía, Maximiliano, Rossi, Gianfranco
Formato: Objeto de conferencia Resumen
Lenguaje:Inglés
Publicado: 2022
Materias:
Ciencias Informáticas
Constraint Logic Programming tool
Theory of finite sets
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/151644
https://publicaciones.sadio.org.ar/index.php/JAIIO/article/download/302/251
Aporte de:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-151644
record_format dspace
spelling I19-R120-10915-1516442023-05-03T20:04:19Z http://sedici.unlp.edu.ar/handle/10915/151644 https://publicaciones.sadio.org.ar/index.php/JAIIO/article/download/302/251 issn:2451-7496 Integrating cardinality constraints into constraint logic programming with sets Cristía, Maximiliano Rossi, Gianfranco 2022-10 2022 2023-04-18T15:31:32Z en Ciencias Informáticas Constraint Logic Programming tool Theory of finite sets Formal reasoning about finite sets and cardinality is important for many applications, including software verification, where very often one needs to reason about the size of a given data structure. The Constraint Logic Programming tool {log} (‘setlog’) provides a decision procedure for deciding the satisfiability of formulas involving very general forms of finite sets, although it does not provide cardinality constraints. In this paper we adapt and integrate a decision procedure for a theory of finite sets with cardinality into {log}. The proposed solver is proved to be a decision procedure for its formulas. Besides, the new CLP instance is implemented as part of the {log} tool. In turn, the implementation uses Howe and King’s Prolog SAT solver and Prolog’s CLP(Q) library, as an integer linear programming solver. The empirical evaluation of this implementation based on +250 real verification conditions shows that it can be useful in practice. Sociedad Argentina de Informática e Investigación Operativa Objeto de conferencia Resumen http://creativecommons.org/licenses/by-nc-sa/4.0/ Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International (CC BY-NC-SA 4.0) application/pdf 70-70
institution Universidad Nacional de La Plata
institution_str I-19
repository_str R-120
collection SEDICI (UNLP)
language Inglés
topic Ciencias Informáticas
Constraint Logic Programming tool
Theory of finite sets
spellingShingle Ciencias Informáticas
Constraint Logic Programming tool
Theory of finite sets
Cristía, Maximiliano
Rossi, Gianfranco
Integrating cardinality constraints into constraint logic programming with sets
topic_facet Ciencias Informáticas
Constraint Logic Programming tool
Theory of finite sets
description Formal reasoning about finite sets and cardinality is important for many applications, including software verification, where very often one needs to reason about the size of a given data structure. The Constraint Logic Programming tool {log} (‘setlog’) provides a decision procedure for deciding the satisfiability of formulas involving very general forms of finite sets, although it does not provide cardinality constraints. In this paper we adapt and integrate a decision procedure for a theory of finite sets with cardinality into {log}. The proposed solver is proved to be a decision procedure for its formulas. Besides, the new CLP instance is implemented as part of the {log} tool. In turn, the implementation uses Howe and King’s Prolog SAT solver and Prolog’s CLP(Q) library, as an integer linear programming solver. The empirical evaluation of this implementation based on +250 real verification conditions shows that it can be useful in practice.
format Objeto de conferencia
Resumen
author Cristía, Maximiliano
Rossi, Gianfranco
author_facet Cristía, Maximiliano
Rossi, Gianfranco
author_sort Cristía, Maximiliano
title Integrating cardinality constraints into constraint logic programming with sets
title_short Integrating cardinality constraints into constraint logic programming with sets
title_full Integrating cardinality constraints into constraint logic programming with sets
title_fullStr Integrating cardinality constraints into constraint logic programming with sets
title_full_unstemmed Integrating cardinality constraints into constraint logic programming with sets
title_sort integrating cardinality constraints into constraint logic programming with sets
publishDate 2022
url http://sedici.unlp.edu.ar/handle/10915/151644
https://publicaciones.sadio.org.ar/index.php/JAIIO/article/download/302/251
work_keys_str_mv AT cristiamaximiliano integratingcardinalityconstraintsintoconstraintlogicprogrammingwithsets
AT rossigianfranco integratingcardinalityconstraintsintoconstraintlogicprogrammingwithsets
_version_ 1765659994938671104

Ejemplares similares