arXiv subjects

Jordi Coll

Publications and source records attributed to Jordi Coll.

4 recordsLinked to original sources

arXiv2026

SAT-IT: an Online Interactive SAT Tracer

Modern Boolean Satisfiability (SAT) solvers, based on the Conflict-Driven Clause Learning (CDCL) paradigm, achieve state-of-the-art efficiency but present a steep learning curve due to their sophisticated algorithms and highly optimized data structures. Understanding these complex mechanics and evaluating the effectiveness of problem encodings is notoriously challenging for students and emerging researchers. To ease this learning process, we introduce the Interactive SAT Tracer (SAT-IT), an open-access web environment designed to make the foundations of SAT solving highly visible and interactive. SAT-IT offers a staged pedagogical progression: from naive backtracking to DPLL and full CDCL with the two-watched literals scheme. Users can clearly inspect fundamental data structures, search space trails, and solving statistics. The tool interactive search space exploration is boosted with literal-level breakpoints for targeted inspection, alongside versatile automatic solving modes that offer both continuous real-time execution and state-based subroutine automation. Combined with a powerful ``what-if'' capability for stepping backward to explore alternative decisions, an instance manager, and an extensible architecture ready to support additional algorithms, SAT-IT serves as a practical, granular lens for experimenting with SAT solving algorithms and analysing encodings efficiency.

cs.LO↗

arXiv2025

Certified Branch-and-Bound MaxSAT Solving (Extended Version)

Over the past few decades, combinatorial solvers have seen remarkable performance improvements, enabling their practical use in real-world applications. In some of these applications, ensuring the correctness of the solver's output is critical. However, the complexity of modern solvers makes them susceptible to bugs in their source code. In the domain of satisfiability checking (SAT), this issue has been addressed through proof logging, where the solver generates a formal proof of the correctness of its answer. For more expressive problems like MaxSAT, the optimization variant of SAT, proof logging had not seen a comparable breakthrough until recently. In this paper, we show how to achieve proof logging for state-of-the-art techniques in Branch-and-Bound MaxSAT solving. This includes certifying look-ahead methods used in such algorithms as well as advanced clausal encodings of pseudo-Boolean constraints based on so-called Multi-Valued Decision Diagrams (MDDs). We implement these ideas in MaxCDCL, the dominant branch-and-bound solver, and experimentally demonstrate that proof logging is feasible with limited overhead, while proof checking remains a challenge.

cs.LO↗

arXiv2021

A Preliminary Case Study of Planning With Complex Transitions: Plotting

Plotting is a tile-matching puzzle video game published by Taito in 1989. Its objective is to reduce a given grid of coloured blocks down to a goal number or fewer. This is achieved by the avatar character repeatedly shooting the block it holds into the grid. Plotting is an example of a planning problem: given a model of the environment, a planning problem asks us to find a sequence of actions that can lead from an initial state of the environment to a given goal state while respecting some constraints. The key difficulty in modelling Plotting is in capturing the way the puzzle state changes after each shot. A single shot can affect multiple tiles directly, and the grid is affected by gravity so numerous other tiles can be affected indirectly. We present and evaluate a constraint model of the Plotting problem that captures this complexity. We also discuss the difficulties and inefficiencies of modelling Plotting in PDDL, the standard language used for input to specialised AI planners. We conclude by arguing that AI planning could benefit from a richer modelling language.

cs.AI↗

arXiv2021

SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints

When solving a combinatorial problem using propositional satisfiability (SAT), the encoding of the problem is of vital importance. We study encodings of Pseudo-Boolean (PB) constraints, a common type of arithmetic constraint that appears in a wide variety of combinatorial problems such as timetabling, scheduling, and resource allocation. In some cases PB constraints occur together with at-most-one (AMO) constraints over subsets of their variables (forming PB(AMO) constraints). Recent work has shown that taking account of AMOs when encoding PB constraints using decision diagrams can produce a dramatic improvement in solver efficiency. In this paper we extend the approach to other state-of-the-art encodings of PB constraints, developing several new encodings for PB(AMO) constraints. Also, we present a more compact and efficient version of the popular Generalized Totalizer encoding, named Reduced Generalized Totalizer. This new encoding is also adapted for PB(AMO) constraints for a further gain. Our experiments show that the encodings of PB(AMO) constraints can be substantially smaller than those of PB constraints. PB(AMO) encodings allow many more instances to be solved within a time limit, and solving time is improved by more than one order of magnitude in some cases. We also observed that there is no single overall winner among the considered encodings, but efficiency of each encoding may depend on PB(AMO) characteristics such as the magnitude of coefficient values.

cs.AI↗