Search Results

Documents authored by Oliveras, Albert

Artifact
Software
DOI: 10.4230/artifacts.26035
enric-rodriguez/WhyUnsat

Authors: Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell

Abstract
Cite as

Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell. enric-rodriguez/WhyUnsat (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26035,
   title = {{enric-rodriguez/WhyUnsat}}, 
   author = {Nieuwenhuis, Robert and Oliveras, Albert and Rodr{\'\i}guez-Carbonell, Enric},
   note = {Software, Grant PID2024-157044OB-C32, funded by MICIU /AEI /10.13039/501100011033 / FEDER, UE, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:68a66c6e39049a7035e472378224d089a41143f4;origin=https://github.com/enric-rodriguez/WhyUnsat;visit=swh:1:snp:5fd506468b1330d7c357d31650ee99f1e5ca8a92;anchor=swh:1:rev:75181fe5faf5ae7bbbc51ce1b49f87bac637c77c}{\texttt{swh:1:dir:68a66c6e39049a7035e472378224d089a41143f4}} (visited on 2026-07-16)},
   url = {https://github.com/enric-rodriguez/WhyUnsat},
   doi = {10.4230/artifacts.26035},
}
Document
Tool Paper
DOI: 10.4230/LIPIcs.SAT.2026.39
WhyUnsat: A Practical Explanation Tool (Tool Paper)

Authors: Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract
Hard industrial planning, timetabling or scheduling instances for SAT typically have many high-level constraints, each expressed by a possibly large number of clauses. When a given instance is reported unsatisfiable by the SAT solver, the user normally needs an explanation why: a (hopefully small) subset of the constraints causing it. Our industrial applications require fast explanations, preferably faster than the original SAT run. For this, we leverage the original solver’s work through its unsatisfiability proof. Here we introduce WhyUnsat, and explain why it is fast and robust. In WhyUnsat one can always plug in the best current SAT solver and proof trimmer, without any modification, by simply indicating the path to their executables. WhyUnsat is also fast because it exploits, via MPI, the -progressively cheaper- shared-memory and distributed computing resources. Another requirement we had is that the tool should be anytime and user-friendly; indeed, it quickly shows a human-readable presentation of (an over-approximation of) the explanation, which is then progressively reduced until minimality (unless interrupted by the user). Finally, and not less importantly, here we explain how and why the WhyUnsat approach is now also directly applicable, at no implementation cost, to IPASIR-UP-based constraint programming by Lazy Clause Generation (LCG) as well as to SAT Modulo Theories (SMT).
Cite as

Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. WhyUnsat: A Practical Explanation Tool (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 39:1-39:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{nieuwenhuis_et_al:LIPIcs.SAT.2026.39,
  author =	{Nieuwenhuis, Robert and Oliveras, Albert and Rodr{\'\i}guez-Carbonell, Enric},
  title =	{{WhyUnsat: A Practical Explanation Tool}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{39:1--39:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.39},
  URN =		{urn:nbn:de:0030-drops-263456},
  doi =		{10.4230/LIPIcs.SAT.2026.39},
  annote =	{Keywords: SAT, SMT, Constraint Programming, Lazy Clause Generation}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.23
Symbolic Conflict Analysis in Pseudo-Boolean Optimization

Authors: Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Rui Zhao

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
In the the last two decades, a lot of effort has been devoted to the development of satisfiability-checking tools for a variety of SAT-related problems. However, most of these tools lack optimization capabilities. That is, instead of finding any solution, one is sometimes interested in a solution that is best according to some criterion. Pseudo-Boolean solvers can be used to deal with optimization by successively solving a series of problems that contain an additional pseudo-Boolean constraint expressing that a better solution is required. A key point for the success of this simple approach is that lemmas that are learned for one problem can be reused for subsequent ones. In this paper we go one step further and show how, by using a simple symbolic conflict analysis procedure, not only can lemmas be reused between problems but also strengthened, thus further pruning the search space traversal. In addition, we show how this technique automatically allows one to infer upper bounds in maximization problems, thus giving an estimation of how far the solver is from finding an optimal solution. Experimental results with our PB solver reveal that (i) this technique is indeed effective in practice, providing important speedups in problems where several solutions are found and (ii) on problems with very few solutions, where the impact of our technique is limited, its overhead is negligible.
Cite as

Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Rui Zhao. Symbolic Conflict Analysis in Pseudo-Boolean Optimization. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{nieuwenhuis_et_al:LIPIcs.SAT.2025.23,
  author =	{Nieuwenhuis, Robert and Oliveras, Albert and Rodr{\'\i}guez-Carbonell, Enric and Zhao, Rui},
  title =	{{Symbolic Conflict Analysis in Pseudo-Boolean Optimization}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.23},
  URN =		{urn:nbn:de:0030-drops-237579},
  doi =		{10.4230/LIPIcs.SAT.2025.23},
  annote =	{Keywords: SAT, Pseudo-Boolean Optimization, Conflict Analysis}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.22
Speeding up Pseudo-Boolean Propagation

Authors: Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Rui Zhao

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

Abstract
Unit propagation is known to be one of the most time-consuming procedures inside CDCL-based SAT solvers. Not surprisingly, it has been studied in depth and the two-watched-literal scheme, enhanced with implementation details boosting its performance, has emerged as the dominant method. In pseudo-Boolean solvers, the importance of unit propagation is similar, but no dominant method exists: counter propagation and watched-based extensions are efficient for different types of constraints, which has opened the door to hybrid methods. However, probably due to the higher complexity of implementing pseudo-Boolean solvers, research efforts have not focused much on concrete implementation details for unit propagation but rather on higher-level aspects of other procedures, such as conflict analysis. In this paper, we present (i) a novel methodology to precisely assess the performance of propagation mechanisms, (ii) an evaluation of implementation variants of the propagation methods present in {RoundingSat} and (iii) a detailed analysis showing that hybrid methods outperform the ones based on a single technique. Our final contribution is to show that a carefully implemented hybrid propagation method is considerably faster than the preferred propagation mechanism in {RoundingSat}, and that this improvement leads to a better overall performance of the solver.
Cite as

Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Rui Zhao. Speeding up Pseudo-Boolean Propagation. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{nieuwenhuis_et_al:LIPIcs.SAT.2024.22,
  author =	{Nieuwenhuis, Robert and Oliveras, Albert and Rodr{\'\i}guez-Carbonell, Enric and Zhao, Rui},
  title =	{{Speeding up Pseudo-Boolean Propagation}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{22:1--22:18},
  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.22},
  URN =		{urn:nbn:de:0030-drops-205449},
  doi =		{10.4230/LIPIcs.SAT.2024.22},
  annote =	{Keywords: SAT, Pseudo-Boolean Solving, Implementation-level Details}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.18
Learning Shorter Redundant Clauses in SDCL Using MaxSAT

Authors: Albert Oliveras, Chunxiao Li, Darryl Wu, Jonathan Chung, and Vijay Ganesh

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
In this paper we present the design and implementation of a Satisfaction-Driven Clause Learning (SDCL) SAT solver, MapleSDCL, which uses a MaxSAT-based technique that enables it to learn shorter, and hence better, redundant clauses. We also perform a thorough empirical evaluation of our method and show that our SDCL solver solves Mutilated Chess Board (MCB) problems significantly faster than CDCL solvers, without requiring any alteration to the branching heuristic used by the underlying CDCL SAT solver.
Cite as

Albert Oliveras, Chunxiao Li, Darryl Wu, Jonathan Chung, and Vijay Ganesh. Learning Shorter Redundant Clauses in SDCL Using MaxSAT. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{oliveras_et_al:LIPIcs.SAT.2023.18,
  author =	{Oliveras, Albert and Li, Chunxiao and Wu, Darryl and Chung, Jonathan and Ganesh, Vijay},
  title =	{{Learning Shorter Redundant Clauses in SDCL Using MaxSAT}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{18:1--18:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.18},
  URN =		{urn:nbn:de:0030-drops-184803},
  doi =		{10.4230/LIPIcs.SAT.2023.18},
  annote =	{Keywords: SAT, SDCL, MaxSAT}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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