3 Search Results for "Salvia, Josep M."

Document

DOI: 10.4230/LIPIcs.SAT.2024.16

Towards Universally Accessible SAT Technology

Authors: Alexey Ignatiev, Zi Li Tan, and Christos Karamanos

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract

Boolean satisfiability (SAT) solvers are a family of highly efficient reasoning engines, which are frequently used for solving a large and diverse variety of practical challenges. This applies to multidisciplinary problems belonging to the class NP but also those arising at higher levels of the polynomial hierarchy. Unfortunately, encoding a problem of user’s interest to a (series of) propositional formula(s) in conjunctive normal form (CNF), let alone dealing with a SAT solver, is rarely a simple task even for an experienced SAT practitioner. This situation gets aggravated further when the user has little to no knowledge on the operation of the modern SAT solving technology. In 2018, the PySAT framework was proposed to address the issue of fast and "painless" prototyping with SAT solvers in Python allowing researchers to get SAT-based solutions to their problems without investing substantial time in the development process and yet sacrificing only a little in terms of performance. Since then, PySAT has proved a useful instrument for solving a wide range of practical problems and is now a critical package for the PyPI infrastructure. In the meantime, there have been advances in SAT solving and enhancements to PySAT functionality to extend its modelling and solving capabilities in order to make modern SAT technology accessible and deployable on a massive scale. This paper provides a high-level overview of the current architecture of PySAT and some of its capabilities including arbitrary Boolean formula manipulation, CNF preprocessing, and support for external user-defined propagators.

Cite as

Alexey Ignatiev, Zi Li Tan, and Christos Karamanos. Towards Universally Accessible SAT Technology. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 16:1-16:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ignatiev_et_al:LIPIcs.SAT.2024.16,
  author =	{Ignatiev, Alexey and Tan, Zi Li and Karamanos, Christos},
  title =	{{Towards Universally Accessible SAT Technology}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{16:1--16:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.16},
  URN =		{urn:nbn:de:0030-drops-205382},
  doi =		{10.4230/LIPIcs.SAT.2024.16},
  annote =	{Keywords: PySAT, Python, Prototyping, Practical Applicability}
}

Document

DOI: 10.4230/LIPIcs.CP.2023.7

Exploiting Configurations of MaxSAT Solvers

Authors: Josep Alòs, Carlos Ansótegui, Josep M. Salvia, and Eduard Torres

Published in: LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)

Abstract

In this paper, we describe how we can effectively exploit alternative parameter configurations to a MaxSAT solver. We describe how these configurations can be computed in the context of MaxSAT. In particular, we experimentally show how to easily combine configurations of a non-competitive solver to obtain a better solving approach.

Cite as

Josep Alòs, Carlos Ansótegui, Josep M. Salvia, and Eduard Torres. Exploiting Configurations of MaxSAT Solvers. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 7:1-7:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{alos_et_al:LIPIcs.CP.2023.7,
  author =	{Al\`{o}s, Josep and Ans\'{o}tegui, Carlos and Salvia, Josep M. and Torres, Eduard},
  title =	{{Exploiting Configurations of MaxSAT Solvers}},
  booktitle =	{29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
  pages =	{7:1--7:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-300-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{280},
  editor =	{Yap, Roland H. C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.7},
  URN =		{urn:nbn:de:0030-drops-190443},
  doi =		{10.4230/LIPIcs.CP.2023.7},
  annote =	{Keywords: maximum satisfiability, maxsat evaluation, automatic configuration}
}

Document

DOI: 10.4230/LIPIcs.SAT.2022.25

OptiLog V2: Model, Solve, Tune and Run

Authors: Josep Alòs, Carlos Ansótegui, Josep M. Salvia, and Eduard Torres

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract

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.

Cite as

Josep Alòs, Carlos Ansótegui, Josep M. Salvia, and Eduard Torres. OptiLog V2: Model, Solve, Tune and Run. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{alos_et_al:LIPIcs.SAT.2022.25,
  author =	{Al\`{o}s, Josep and Ans\'{o}tegui, Carlos and Salvia, Josep M. and Torres, Eduard},
  title =	{{OptiLog V2: Model, Solve, Tune and Run}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{25:1--25:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.25},
  URN =		{urn:nbn:de:0030-drops-166996},
  doi =		{10.4230/LIPIcs.SAT.2022.25},
  annote =	{Keywords: Tool framework, Satisfiability, Modelling, Solving}
}

Refine by Author
2 Alòs, Josep
2 Ansótegui, Carlos
2 Salvia, Josep M.
2 Torres, Eduard
1 Ignatiev, Alexey
Show More...

Refine by Classification
3 Theory of computation → Constraint and logic programming
1 Hardware → Theorem proving and SAT solving
1 Software and its engineering → Software libraries and repositories

Refine by Keyword
1 Modelling
1 Practical Applicability
1 Prototyping
1 PySAT
1 Python
Show More...

Refine by Type
3 document

Refine by Publication Year
1 2022
1 2023
1 2024