Carlos Ansótegui

JAIR Journal 2026 Journal Article

Revisiting SAT-based Solvers: MaxSAT Rules and Core Sequences

• Josep Alòs
• Carlos Ansótegui
• Eduard Torres

In this paper, we revisit the state-of-the-art of MaxSAT solving. We focus on SAT-based MaxSAT solving algorithms, mainly on Core-guided MaxSAT solvers. We show how to describe Core-guided solvers with Non-CNF MaxSAT rules plus the Extension rule. Equipped with these rules, we show how to apply them alternatively to obtain new Core-guided MaxSAT solvers. Since Core-guided solvers essentially solve a sequence of SAT instances, we also discuss how Core-guided MaxSAT solvers traverse the search space of possible sequences of SAT instances, the existence of exponentially harder sequences, and how to avoid them. The experimental investigation shows comparable and complementary performance to state-of-the-art solvers.

SAT Conference 2022 Conference Paper

OptiLog V2: Model, Solve, Tune and Run

• Josep Alos
• Carlos Ansótegui
• Josep M. Salvia
• Eduard Torres

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.

SAT Conference 2021 Conference Paper

OptiLog: A Framework for SAT-based Systems

• Carlos Ansótegui
• Jesus Ojeda
• António Pacheco 0004
• Josep Pon
• Josep M. Salvia
• Eduard Torres

Abstract We present OptiLog, a new Python framework for rapid prototyping of SAT-based systems. OptiLog allows to use and integrate SAT solvers currently developed in C/C++ just by implementing the iSAT C++ interface. It also provides a Python binding to the PBLib C++ toolkit for encoding Pseudo Boolean and Cardinality constraints. Finally, it leverages the power of automatic configurators by allowing to easily create configuration scenarios including multiple solvers and encoders.

SAT Conference 2021 Conference Paper

PyDGGA: Distributed GGA for Automatic Configuration

• Carlos Ansótegui
• Josep Pon
• Meinolf Sellmann
• Kevin Tierney

Abstract We present PyDGGA, a Python tool that implements a distributed version of the automatic algorithm configurator GGA, which is a specialized genetic algorithm to find high quality parameters for solvers and algorithms. PyDGGA implements GGA using an event-driven architecture and runs a simulation of future generations of the genetic algorithm to maximize the usage of the available computing resources. Overall, PyDGGA offers a friendly interface to deploy elastic distributed AC scenarios on shared high-performance computing clusters.

IJCAI Conference 2021 Conference Paper

Reducing SAT to Max2SAT

• Carlos Ansótegui
• Jordi Levy

In the literature, we find reductions from 3SAT to Max2SAT. These reductions are based on the usage of a gadget, i. e. , a combinatorial structure that allows translating constraints of one problem to constraints of another. Unfortunately, the generation of these gadgets lacks an intuitive or efficient method. In this paper, we provide an efficient and constructive method for Reducing SAT to Max2SAT and show empirical results of how MaxSAT solvers are more efficient than SAT solvers solving the translation of hard formulas for Resolution.

JAIR Journal 2019 Journal Article

Community Structure in Industrial SAT Instances

• Carlos Ansótegui
• Maria Luisa Bonet
• Jesús Giráldez-Cru
• Jordi Levy
• Laurent Simon

Modern SAT solvers have experienced a remarkable progress on solving industrial instances. It is believed that most of these successful techniques exploit the underlying structure of industrial instances. Recently, there have been some attempts to analyze the structure of industrial SAT instances in terms of complex networks, with the aim of explaining the success of SAT solving techniques, and possibly improving them. In this paper, we study the community structure, or modularity, of industrial SAT instances. In a graph with clear community structure, or high modularity, we can find a partition of its nodes into communities such that most edges connect variables of the same community. Representing SAT instances as graphs, we show that most application benchmarks are characterized by a high modularity. On the contrary, random SAT instances are closer to the classical Erdös-Rényi random graph model, where no structure can be observed. We also analyze how this structure evolves by the effects of the execution of a CDCL SAT solver, and observe that new clauses learned by the solver during the search contribute to destroy the original structure of the formula. Motivated by this observation, we finally present an application that exploits the community structure to detect relevant learned clauses, and we show that detecting these clauses results in an improvement on the performance of the SAT solver. Empirically, we observe that this improves the performance of several SAT solvers on industrial SAT formulas, especially on satisfiable instances.

AIJ Journal 2017 Journal Article

WPM3: An (in)complete algorithm for weighted partial MaxSAT

• Carlos Ansótegui
• Joel Gabàs

Maximum Satisfiability (MaxSAT) has been used to solve efficiently many combinatorial optimization problems. At recent editions of international MaxSAT Evaluation (MSE), the best performing solvers for real world (industrial) problems were those implementing SAT-based algorithms. These algorithms reformulate the MaxSAT optimization problem into a sequence of SAT decision problems where Pseudo-Boolean (PB) constraints may be introduced. In order to identify the most suitable PB constraints, some algorithms (core-guided) analyze the unsatisfiable cores retrieved from the previous SAT problems in the sequence while refining the lower bound. In this paper, we first conduct a comprehensive study on the complete core-guided algorithms Eva and OLL, that inspired the best performing solvers on industrial instances at MSE-2014. Despite of its apparently different foundations, we show how they are intimately related and identify how to improve them. In this sense, we present our complete core-guided algorithm WPM3. We show how to further exploit the analysis of unsatisfiable cores by being aware of their global structure, i. e. , how the cores are interrelated. This is used to encode more efficient PB constraints and enables the algorithm to obtain assignments and refine also the upper bound. Therefore, WPM3 can also work as an incomplete algorithm. At MSE-2015, it showed a competitive performance on industrial instances. It got one out of three gold medals at the complete track and dominated at the incomplete track.

AIJ Journal 2016 Journal Article

MaxSAT by improved instance-specific algorithm configuration

• Carlos Ansótegui
• Joel Gabàs
• Yuri Malitsky
• Meinolf Sellmann

Our objective is to boost the state-of-the-art performance in MaxSAT solving. To this end, we employ the instance-specific algorithm configurator ISAC, and improve it with the latest in portfolio technology. Experimental results on SAT show that this combination marks a significant step forward in our ability to tune algorithms instance-specifically. We then apply the new methodology to a number of MaxSAT problem domains and show that the resulting solvers consistently outperform the best existing solvers on the respective problem families. In fact, the solvers presented here were independently evaluated at the 2013 and 2014 MaxSAT Evaluations where they won several categories.

SAT Conference 2015 Conference Paper

Using Community Structure to Detect Relevant Learnt Clauses

• Carlos Ansótegui
• Jesús Giráldez-Cru
• Jordi Levy
• Laurent Simon 0001

Abstract Nowadays, Conflict-Driven Clause Learning (CDCL) techniques are one of the key components of modern SAT solvers specialized in industrial instances. Last years, one of the focuses has been put on strategies to select which learnt clauses are removed during the search. Originally, one need for removing clauses was motivated by the finiteness of memory. Recently, it has been shown that more aggressive clause deletion policies may improve solvers performance, even when memory is sufficient. Also, the utility of learnt clauses has been related to the modular structure of industrial SAT instances. In this paper, we show that augmenting SAT instances with learnt clauses does not always make them easier for the SAT solver. In fact, it makes worse the solver performance in many cases. However, we identify a set of highly useful learnt clauses, and we show that augmenting SAT instances with this set of clauses contributes to improve the solver performance in many cases, especially in satisfiable formulas. These clauses are related to the community structure of the formula, and they can be computed in a fast preprocessing step. This would suggest that the community structure may play an important role in clause deletion policies.

AIJ Journal 2013 Journal Article

SAT-based MaxSAT algorithms

• Carlos Ansótegui
• Maria Luisa Bonet
• Jordi Levy

Many industrial optimization problems can be translated to MaxSAT. Although the general problem is NP hard, like SAT, many practical problems may be solved using modern MaxSAT solvers. In this paper we present several algorithms specially designed to deal with industrial or real problems. All of them are based on the idea of solving MaxSAT through successive calls to a SAT solver. We show that this SAT-based technique is efficient in solving industrial problems. In fact, all state-of-the-art MaxSAT solvers that perform well in industrial instances are based on this technique. In particular, our solvers won the 2009 partial MaxSAT and the 2011 weighted partial MaxSAT industrial categories of the MaxSAT evaluation. We prove the correctness of all our algorithms. We also present a complete experimental study comparing the performance of our algorithms with latest MaxSAT solvers.

SAT Conference 2012 Conference Paper

The Community Structure of SAT Formulas

• Carlos Ansótegui
• Jesús Giráldez-Cru
• Jordi Levy

Abstract The research community on complex networks has developed techniques of analysis and algorithms that can be used by the SAT community to improve our knowledge about the structure of industrial SAT instances. It is often argued that modern SAT solvers are able to exploit this hidden structure, without a precise definition of this notion. In this paper, we show that most industrial SAT instances have a high modularity that is not present in random instances. We also show that successful techniques, like learning, (indirectly) take into account this community structure. Our experimental study reveal that most learnt clauses are local on one of those modules or communities.

ECAI Conference 2010 Conference Paper

Solving Pseudo-Boolean Modularity Constraints

• Carlos Ansótegui
• Ramón Béjar
• Cèsar Fernández 0001
• Francesc Guitart
• Carles Mateu

This paper introduces new solving strategies for the resolution of Pseudo-Boolean Modularity (PBMod) constraints. In particular, we deal with modular arithmetic constraints on Boolean variables. On the one hand, we analyze translations to Pseudo-Boolean (PB) constraints and apply PB solvers. We also look at those PB solvers that have shown that a transformation to the SAT problem can be an effective solving strategy for PB problems. Among the existing translation techniques we focus on the encoding based on a network of sorters. We extend this encoding technique to generate directly a SAT formula from the PBMod constraints. We compare our approach to other standard techniques such as Satisfiability Modulo Theories (SMT) solvers with support for the Quantifier Free Linear Integer Arithmetic (QF_LIA) theory and the GLPK package for Mixed Integer Programming. In order to conduct our experimental investigation we present a generator of random PBMod constraints and study the impact of the several parameters on the hardness of the instances.

IJCAI Conference 2009 Conference Paper

• Carlos Ansótegui
• Maria Luisa Bonet
• Jordi Levy

We focus on the random generation of SAT instances that have computational properties that are similar to real-world instances. It is known that industrial instances, even with a great number of variables, can be solved by a clever solver in a reasonable amount of time. This is not possible, in general, with classical randomly generated instances. We provide different generation models of SAT instances, extending the uniform and regular 3-CNF models. They are based on the use of non-uniform probability distributions to select variables. Our last model also uses a mechanism to produce clauses of different lengths as in industrial instances. We show the existence of the phase transition phenomena for our models and we study the hardness of the generated instances as a function of the parameters of the probability distributions. We prove that, with these parameters we can adjust the difficulty of the problems in the phase transition point. We measure hardness in terms of the performance of different solvers. We show how these models will allow us to generate random instances similar to industrial instances, of interest for testing purposes.

SAT Conference 2009 Conference Paper

Solving (Weighted) Partial MaxSAT through Satisfiability Testing

• Carlos Ansótegui
• Maria Luisa Bonet
• Jordi Levy

Abstract Recently, Fu and Malik described an unweighted Partial MaxSAT solver based on successive calls to a SAT solver. At the k th iteration the SAT solver tries to certify that there exist an assignment that satisfies all but k clauses. Later Marques-Silva and Planes implemented and extended these ideas. In this paper we present and implement two Partial MaxSAT solvers and the weighted variant of one of them. Both are based on Fu and Malik ideas. We prove the correctness of our algorithm and compare our solver with other (Weighted) MaxSAT and (Weighted) Partial MaxSAT solvers.

AAAI Conference 2008 Conference Paper

Generating Hard SAT/CSP Instances Using Expander Graphs

• Carlos Ansótegui
• Cèsar Fernández

In this paper we provide a new method to generate hard k-SAT instances. We incrementally construct a high girth bipartite incidence graph of the k-SAT instance. Having high girth assures high expansion for the graph, and high expansion implies high resolution width. We have extended this approach to generate hard n-ary CSP instances and we have also adapted this idea to increase the expansion of the system of linear equations used to generate XORSAT instances, being able to produce harder satisfiable instances than former generators.

AAAI Conference 2008 Conference Paper

Measuring the Hardness of SAT Instances

• Carlos Ansótegui
• Jordi Levy

The search of a precise measure of what hardness of SAT instances means for state-of-the-art solvers is a relevant research question. Among others, the space complexity of treelike resolution (also called hardness), the minimal size of strong backdoors and of cycle-cutsets, and the treewidth can be used for this purpose. We propose the use of the tree-like space complexity as a solid candidate to be the best measure for solvers based on DPLL. To support this thesis we provide a comparison with the other mentioned measures. We also conduct an experimental investigation to show how the proposed measure characterizes the hardness of random and industrial instances.

SAT Conference 2007 Conference Paper

Mapping CSP into Many-Valued SAT

• Carlos Ansótegui
• Maria Luisa Bonet
• Jordi Levy
• Felip Manyà

Abstract We first define a mapping from CSP to many-valued SAT which allows to solve CSP instances with many-valued SAT solvers. Second, we define a new many-valued resolution rule and prove that it is refutation complete for many-valued CNF formulas and, moreover, enforces CSP ( i, j )-consistency when applied to a many-valued SAT encoding of a CSP. Instances of our rule enforce well-known local consistency properties such as arc consistency and path consistency.

AAAI Conference 2007 Conference Paper

On Balanced CSPs with High Treewidth

• Carlos Ansótegui
• César Fernàndez

Tractable cases of the binary CSP are mainly divided in two classes: constraint language restrictions and constraint graph restrictions. To better understand and identify the hardest binary CSPs, in this work we propose methods to increase their hardness by increasing the balance of both the constraint language and the constraint graph. The balance of a constraint is increased by maximizing the number of domain elements with the same number of occurrences. The balance of the graph is defined using the classical definition from graph theory. In this sense we present two graph models; a first graph model that increases the balance of a graph maximizing the number of vertices with the same degree, and a second one that additionally increases the girth of the graph, because a high girth implies a high treewidth, an important parameter for binary CSPs hardness. Our results show that our more balanced graph models and constraints result in harder instances when compared to typical random binary CSP instances, by several orders of magnitude. Also we detect, at least for sparse constraint graphs, a higher treewidth for our graph models.

AAAI Conference 2006 Conference Paper

Disco—Novo—GoGo: Integrating Local Search and Complete Search with Restarts

• Meinolf Sellmann
• Carlos Ansótegui

A hybrid algorithm is devised to boost the performance of complete search on under-constrained problems. We suggest to use random variable selection in combination with restarts, augmented by a coarse-grained local search algorithm that learns favorable value heuristics over the course of several restarts. Numerical results show that this method can speedup complete search by orders of magnitude.

SAT Conference 2006 Conference Paper

QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency

• Ashish Sabharwal
• Carlos Ansótegui
• Carla P. Gomes
• Justin W. Hart
• Bart Selman

Abstract Quantified Boolean Formulas (QBFs) present the next big challenge for automated propositional reasoning. Not surprisingly, most of the present day QBF solvers are extensions of successful propositional satisfiability algorithms (SAT solvers). They directly integrate the lessons learned from SAT research, thus avoiding re-inventing the wheel. In particular, they use the standard conjunctive normal form (CNF) augmented with layers of variable quantification for modeling tasks as QBF. We argue that while CNF is well suited to “existential reasoning” as demonstrated by the success of modern SAT solvers, it is far from ideal for “universal reasoning” needed by QBF. The CNF restriction imposes an inherent asymmetry in QBF and artificially creates issues that have led to complex solutions, which, in retrospect, were unnecessary and sub-optimal. We take a step back and propose a new approach to QBF modeling based on a game-theoretic view of problems and on a dual CNF-DNF (disjunctive normal form) representation that treats the existential and universal parts of a problem symmetrically. It has several advantages: (1) it is generic, compact, and simpler, (2) unlike fully non-clausal encodings, it preserves the benefits of pure CNF and leverages the support for DNF already present in many QBF solvers, (3) it doesn’t use the so-called indicator variables for conversion into CNF, thus circumventing the associated illegal search space issue, and (4) our QBF solver based on the dual encoding ( Duaffle ) consistently outperforms the best solvers by two orders of magnitude on a hard class of benchmarks, even without using standard learning techniques.

SAT Conference 2004 Conference Paper

Mapping Problems with Finite-Domain Variables into Problems with Boolean Variables

• Carlos Ansótegui
• Felip Manyà

We define a collection of mappings that transform many-valued clausal forms into satisfiability equivalent Boolean clausal forms, analyze their complexity and evaluate them empirically on a set of benchmarks with state-of-the-art SAT solvers. Our results provide empirical evidence that encoding combinatorial problems with the mappings defined here can lead to substantial performance improvements in complete SAT solvers.

AAAI Conference 2004 Conference Paper

Modeling Choices in Quasigroup Completion: SAT Versus CSP

• Carlos Ansótegui
• Iván Dotuacute;

We perform a systematic comparison of SAT and CSP models for a challenging combinatorial problem, quasigroup completion (QCP). Our empirical results clearly indicate the superiority of the 3D SAT encoding (Kautz et al. 2001), with various solvers, over other SAT and CSP models. We propose a partial explanation of the observed performance. Analytically, we focus on the relative conciseness of the 3D model and the pruning power of unit propagation. Empirically, the focus is on the role of the unit-propagation heuristic of the best performing solver, Satz (Li & Anbulagan 1997), which proves crucial to its success, and results in a significant improvement in scalability when imported into the CSP solvers. Our results strongly suggest that SAT encodings of permutation problems (Hnich, Smith, & Walsh 2004) may well prove quite competitive in other domains, in particular when compared with the currently preferred channeling CSP models.