Search Results

Documents authored by Torres, Eduard

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}
}
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