4 Search Results for "Torres, Eduard"

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}
}
Document
DOI: 10.4230/LIPIcs.CP.2021.12
Building High Strength Mixed Covering Arrays with Constraints

Authors: Carlos Ansótegui, Jesús Ojeda, and Eduard Torres

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
Covering arrays have become a key piece in Combinatorial Testing. In particular, we focus on the efficient construction of Covering Arrays with Constraints of high strength. SAT solving technology has been proven to be well suited when solving Covering Arrays with Constraints. However, the size of the SAT reformulations rapidly grows up with higher strengths. To this end, we present a new incomplete algorithm that mitigates substantially memory blow-ups. The experimental results confirm the goodness of the approach, opening avenues for new practical applications.
Cite as

Carlos Ansótegui, Jesús Ojeda, and Eduard Torres. Building High Strength Mixed Covering Arrays with Constraints. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{ansotegui_et_al:LIPIcs.CP.2021.12,
  author =	{Ans\'{o}tegui, Carlos and Ojeda, Jes\'{u}s and Torres, Eduard},
  title =	{{Building High Strength Mixed Covering Arrays with Constraints}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{12:1--12:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.12},
  URN =		{urn:nbn:de:0030-drops-153036},
  doi =		{10.4230/LIPIcs.CP.2021.12},
  annote =	{Keywords: Combinatorial Testing, Covering Arrays, Maximum Satisfiability}
}
  • Refine by Author
  • 3 Ansótegui, Carlos
  • 3 Torres, Eduard
  • 2 Alòs, Josep
  • 2 Salvia, Josep M.
  • 1 Ignatiev, Alexey
  • Show More...

  • Refine by Classification
  • 4 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 Combinatorial Testing
  • 1 Covering Arrays
  • 1 Maximum Satisfiability
  • 1 Modelling
  • 1 Practical Applicability
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 1 2021
  • 1 2022
  • 1 2023
  • 1 2024

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact