Carlos Ansotegui

AAMAS Conference 2018 Conference Paper

Moral Values in Norm Decision Making

• Marc Serramia
• Maite Lopez-Sanchez
• Juan A. Rodriguez-Aguilar
• Manel Rodriguez
• Michael Wooldridge
• Javier Morales
• Carlos Ansotegui

Most often, both agents and human societies use norms to coordinate their on-going activities. Nevertheless, choosing the ‘right’ set of norms to regulate these societies constitutes an open problem. Firstly, intrinsic norm relationships may lead to inconsistencies in the chosen set of norms. Secondly, and more importantly, there is an increasing demand of including ethical considerations in the decision making process. This paper focuses on choosing the ‘right’ norms by considering moral values together with society’s partial preferences over these values and the extent to which candidate norms promote them. The resulting decision making problem can then be encoded as a linear program, and hence solved by state-ofthe art solvers. Furthermore, we empirically test several optimisation scenarios so to determine the system’s performance and the characteristics of the problem that affect its hardness.

IJCAI Conference 2015 Conference Paper

Exploiting the Structure of Unsatisfiable Cores in MaxSAT

• Carlos Ansotegui
• Frederic Didier
• Joel Gabas

We propose a new approach that exploits the good properties of core-guided and model-guided MaxSAT solvers. In particular, we show how to effectively exploit the structure of unsatisfiable cores in MaxSAT instances. Experimental results on industrial instances show that the proposed approach outperforms both complete and incomplete stateof-the-art MaxSAT solvers at the last international MaxSAT Evaluation in terms of robustness and total number of solved instances.

IJCAI Conference 2015 Conference Paper

Model-Based Genetic Algorithms for Algorithm Configuration

• Carlos Ansotegui
• Yuri Malitsky
• Horst Samulowitz
• Meinolf Sellmann
• Kevin Tierney

AAAI Conference 2014 Conference Paper

MaxSAT by Improved Instance-Specific Algorithm Configuration

• Carlos Ansotegui
• Yuri Malitsky
• Meinolf Sellmann

Our objective is to boost the state-of-the-art performance in MaxSAT solving. To this end, we employ the instancespecific 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 MaxSAT Evaluation where they won six of the eleven categories.

AAAI Conference 2010 Conference Paper

A New Algorithm for Weighted Partial MaxSAT

• Carlos Ansotegui
• Maria Luisa Bonet
• Jordi Levy

We present and implement a Weighted Partial MaxSAT solver based on successive calls to a SAT solver. We prove the correctness of our algorithm and compare our solver with other Weighted Partial MaxSAT solvers.

IJCAI Conference 2007 Conference Paper

• Carlos Ansotegui
• Maria Luisa Bonet
• Jordi Levy
• Felip Manya

We define a translation from Weighted CSP to signed Max-SAT, and a complete resolution-style calculus for solving signed Max-SAT. Based on these results, we then describe an original exact algorithm for solving Weighted CSP. Finally, we define several derived rules and prove that they enforce the main soft arc consistency defined in the literature when applied to Weighted CSP instances.

AAAI Conference 2007 Conference Paper

Inference Rules for High-Order Consistency in Weighted CSP

• Carlos Ansotegui
• Jordi Levy

Recently defined resolution calculi for Max-SAT and signed Max-SAT have provided a logical characterization of the solving techniques applied by Max-SAT and WCSP solvers. In this paper we first define a new resolution rule, called signed Max-SAT parallel resolution, and prove that it is sound and complete for signed Max-SAT. Second, we define a restriction and a generalization of the previous rule called, respectively, signed Max-SAT i-consistency resolution and signed Max-SAT (i, j)-consistency resolution. These rules have the following property: if a WCSP signed encoding is closed under signed Max-SAT i-consistency, then the WCSP is i-consistent, and if it is closed under signed Max-SAT (i, j)-consistency, then the WCSP is (i, j)-consistent. A new and practical insight derived from the definition of these new rules is that algorithms for enforcing high order consistency should incorporate an efficient and effective component for detecting minimal unsatisfiable cores. Finally, we describe an algorithm that applies directional soft consistency with the previous rules.

AAAI Conference 2006 Conference Paper

The Impact of Balancing on Problem Hardness in a Highly Structured Domain

• Carlos Ansotegui
• Cesar Fernandez

Random problem distributions have played a key role in the study and design of algorithms for constraint satisfaction and Boolean satisfiability, as well as in our understanding of problem hardness, beyond standard worst-case complexity. We consider random problem distributions from a highly structured problem domain that generalizes the Quasigroup Completion problem (QCP) and Quasigroup with Holes (QWH), a widely used domain that captures the structure underlying a range of real-world applications. Our problem domain is also a generalization of the well-known Sudoku puzzle: we consider Sudoku instances of arbitrary order, with the additional generalization that the block regions can have rectangular shape, in addition to the standard square shape. We evaluate the computational hardness of Generalized Sudoku instances, for different parameter settings. Our experimental hardness results show that we can generate instances that are considerably harder than QCP/QWH instances of the same size. More interestingly, we show the impact of different balancing strategies on problem hardness. We also provide insights into backbone variables in Generalized Sudoku instances and how they correlate to problem hardness.

AAAI Conference 2005 Conference Paper

The Achilles’ Heel of QBF

• Carlos Ansotegui

In recent years we have seen significant progress in the area of Boolean satisfiability (SAT) solving and its applications. As a new challenge, the community is now moving to investigate whether similar advances can be made in the use of Quantified Boolean Formulas (QBF). QBF provides a natural framework for capturing problem solving and planning in multiagent settings. However, contrarily to single-agent planning, which can be effectively formulated as SAT, we show that a QBF approach to planning in a multi-agent setting leads to significant unexpected computational difficulties. We identify as a key difficulty of the QBF approach the fact that QBF solvers often end up exploring a much larger search space than the natural search space of the original problem. This is in contrast to the experience with SAT approaches. We also show how one can alleviate these problems by introducing two special QBF formulations and a new QBF solution strategy. We present experiments that show the effectiveness of our approach in terms of a significant improvement in performance compared to earlier work in this area. Our work also provides a general methodology for formulating adversarial scenarios in QBF.