Universitat de Lleida
2022
We present an extension of the OptiLog Python framework. We fully redesign the solvers module to support the dynamic loading of incremental SAT solvers with support for external libraries. We introduce new modules for modelling problems into Non-CNF format with support for Pseudo Boolean constraints, for evaluating and parsing the results of applications, and we add support for constrained execution of blackbox programs and SAT-heritage integration. All these enhancements allow OptiLog to become a swiss knife for SAT-based applications in academic and industrial environments.
Supported by Grant PID2019-109137GB-C21 funded by MCIN/AEI/10.13039/501100011033, PANDEMIES 2020 by Agencia de Gestio d’Ajuts Universitaris i de Recerca (AGAUR), Departament d’Empresa i Coneixement de la Generalitat de Catalunya, FONDO SUPERA COVID-19 funded by Crue-CSIC-SANTANDER, and the MICNN FPU fellowship (FPU18/02929).
Object of conference
Published version
English
Kuldeep S. Meel and Ofer Strichman
info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2017-2020/PID2019-109137GB-C21/ES/SISTEMAS DE DEMOSTRACION PRACTICOS MAS ALLA DE RESOLUCION/
Reproducció del document publicat a https://doi.org/10.4230/LIPIcs.SAT.2022.25
In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), 2022, vol. 236, p. 25:1-25:16
cc-by (c) Josep Alòs et al., 2022
Attribution 4.0 International
http://creativecommons.org/licenses/by/4.0/
Documents de recerca [18403]
