Javier Larrosa

AAAI Conference 2024 Conference Paper

Theoretical and Empirical Analysis of Cost-Function Merging for Implicit Hitting Set WCSP Solving

• Javier Larrosa
• Conrado Martínez
• Emma Rollon

The Implicit Hitting Set (HS) approach has shown very effective for MaxSAT solving. However, only preliminary promising results have been obtained for the very similar Weighted CSP framework. In this paper we contribute towards both a better theoretical understanding of the HS approach and a more effective HS-based solvers for WCSP. First, we bound the minimum number of iterations of HS thanks to what we call distinguished cores. Then, we show a source of inefficiency by introducing two simple problems where HS is unfeasible. Next, we propose two reformulation methods that merge cost-functions to overcome the problem. We provide a theoretical analysis that quantifies the magnitude of the improvement of each method with respect to the number of iterations of the algorithm. In particular, we show that the reformulations can bring an exponential number of iterations down to a constant number in our working examples. Finally, we complement our theoretical analysis with two sets of experiments. First, we show that our results are aligned with real executions. Second, and most importantly, we conduct experiments on typical benchmark problems and show that cost-function merging may be heuristically applied and it may accelerate HS algorithms by several orders of magnitude. In some cases, it even outperforms state-of-the-art solvers.

AAAI Conference 2020 Conference Paper

Augmenting the Power of (Partial) MaxSat Resolution with Extension

• Javier Larrosa
• Emma Rollon

The refutation power of SAT and MaxSAT resolution is challenged by problems like the soft and hard Pigeon Hole Problem PHP for which short refutations do not exist. In this paper we augment the MaxSAT resolution proof system with an extension rule. The new proof system MaxResE is sound and complete, and more powerful than plain MaxSAT resolution, since it can refute the soft and hard PHP in polynomial time. We show that MaxResE refutations actually subtract lower bounds from the objective function encoded by the formulas. The resulting formula is the residual after the lower bound extraction. We experimentally show that the residual of the soft PHP (once its necessary cost of 1 has been efficiently subtracted with MaxResE) is a concise, easy to solve, satisfiable problem.

SAT Conference 2020 Conference Paper

Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems

• Javier Larrosa
• Emma Rollon

Abstract MaxSAT is a very popular language for discrete optimization with many domains of application. While there has been a lot of progress in MaxSAT solvers during the last decade, the theoretical analysis of MaxSAT inference has not followed the pace. Aiming at compensating that lack of balance, in this paper we do a proof complexity approach to MaxSAT resolution-based proof systems. First, we give some basic definitions on completeness and show that refutational completeness makes compleness redundant, as it happens in SAT. Then we take three inference rules such that adding them sequentially allows us to navigate from the weakest to the strongest resolution-based MaxSAT system available (i. e. , from standalone MaxSAT resolution to the recently proposed ResE), each rule making the system stronger. Finally, we show that the strongest system captures the recently proposed concept of Circular Proof while being conceptually simpler, since weights, which are intrinsic in MaxSAT, naturally guarantee the flow condition required for the SAT case.

JAIR Journal 2017 Journal Article

Residual-Guided Look-Ahead in AND/OR Search for Graphical Models

• William Lam
• Kalev Kask
• Javier Larrosa
• Rina Dechter

We introduce the concept of local bucket error for the mini-bucket heuristics and show how it can be used to improve the power of AND/OR search for combinatorial optimization tasks in graphical models (e.g. MAP/MPE or weighted CSPs). The local bucket error illuminates how the heuristic errors are distributed in the search space, guided by the mini-bucket heuristic. We present and analyze methods for compiling the local bucket-errors (exactly and approximately) and show that they can be used to yield an effective tool for balancing look-ahead overhead during search. This can be especially instrumental when memory is restricted, accommodating the generation of only weak compiled heuristics. We illustrate the impact of the proposed schemes in an extensive empirical evaluation for both finding exact solutions and anytime suboptimal solutions.

IJCAI Conference 2016 Conference Paper

Limited Discrepancy AND/OR Search and Its Application to Optimization Tasks in Graphical Models

• Javier Larrosa
• Emma Rollon
• Rina Dechter

Many combinatorial problems are solved with a Depth-First search (DFS) guided by a heuristic and it is well-known that this method is very fragile with respect to heuristic mistakes. One standard way to make DFS more robust is to search by increasing number of discrepancies. This approach has been found useful in several domains where the search structure is a height-bounded OR tree. In this paper we investigate the generalization of discrepancy-based search to AND/OR search trees and propose an extension of the Limited Discrepancy Search (LDS) algorithm. We demonstrate the relevance of our proposal in the context of Graphical Models. In these problems, which can be solved with either a standard OR search tree or an AND/OR tree, we show the superiority of our approach. For a fixed number of discrepancies, the search space visited by the AND/OR algorithm strictly contains the search space visited by standard LDS, and many more nodes can be visited due to the multiplicative effect of the AND/OR decomposition. Besides, if the AND/OR tree achieves a significant size reduction with respect to the standard OR tree, the cost of each iteration of the AND/OR algorithm is asymptotically lower than in standard LDS. We report experiments on the minsum problem on different domains and show that the AND/OR version of LDS usually obtains better solutions given the same CPU time.

AAAI Conference 2016 Conference Paper

Look-Ahead with Mini-Bucket Heuristics for MPE

• Rina Dechter
• Kalev Kask
• William Lam
• Javier Larrosa

The paper investigates the potential of look-ahead in the context of AND/OR search in graphical models using the Mini- Bucket heuristic for combinatorial optimization tasks (e. g. , MAP/MPE or weighted CSPs). We present and analyze the complexity of computing the residual (a. k. a. Bellman update) of the Mini-Bucket heuristic and show how this can be used to identify which parts of the search space are more likely to benefit from look-ahead and how to bound its overhead. We also rephrase the look-ahead computation as a graphical model, to facilitate structure exploiting inference schemes. We demonstrate empirically that augmenting Mini-Bucket heuristics by look-ahead is a cost-effective way of increasing the power of Branch-And-Bound search.

ECAI Conference 2016 Conference Paper

On the Impact of Subproblem Orderings on Anytime AND/OR Best-First Search for Lower Bounds

• William Lam
• Kalev Kask
• Rina Dechter
• Javier Larrosa

Best-first search can be regarded as anytime scheme for producing lower bounds on the optimal solution, a characteristic that is mostly overlooked. We explore this topic in the context of AND/OR best-first search, guided by the MBE heuristic, when solving graphical models. In that context, the impact of the secondary heuristic for subproblem ordering may be significant, especially in the anytime context. Indeed, our paper illustrates this, showing that the new concept of bucket errors can advise in providing effective subproblem orderings in AND/OR search.

IJCAI Conference 2013 Conference Paper

Semiring-Based Mini-Bucket Partitioning Schemes

• Emma Rollon
• Javier Larrosa
• Rina Dechter

Graphical models are one of the most prominent frameworks to model complex systems and efficiently query them. Their underlying algebraic properties are captured by a valuation structure that, most usually, is a semiring. Depending on the semiring of choice, we can capture probabilistic models, constraint networks, cost networks, etc. In this paper we address the partitioning problem which occurs in many approximation techniques such as mini-bucket elimination and joingraph propagation algorithms. Roghly speaking, subject to complexity bounds, the algorithm needs to find a partition of a set of factors such that best approximates the whole set. While this problem has been addressed in the past in a particular case, we present here a general description. Furthermore, we also propose a general partitioning scheme. Our proposal is general in the sense that it is presented in terms of a generic semiring with the only additional requirements of a division operation and a refinement of its order. The proposed algorithm instantiates to the particular task of computing the probability of evidence, but also applies directly to other important reasoning tasks. We demonstrate its good empirical behaviour on the problem of computing the most probable explanation.

SAT Conference 2009 Conference Paper

Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates

• Javier Larrosa
• Robert Nieuwenhuis
• Albert Oliveras
• Enric Rodríguez-Carbonell

Abstract We consider optimization problems of the form ( S, cost ), where S is a clause set over Boolean variables x 1. .. x n, with an arbitrary cost function cost: \({\mathbb{B}}^n {\rightarrow} {\mathbb{R}}\), and the aim is to find a model A of S such that cost ( A ) is minimized. Here we study the generation of proofs of optimality in the context of branch-and-bound procedures for such problems. For this purpose we introduce, an abstract DPLL-based branch and bound algorithm that can model optimization concepts such as cost-based propagation and cost-based backjumping. Most, if not all, SAT-related optimization problems are in the scope of. Since many of the existing approaches for solving these problems can be seen as instances, allows one to formally reason about them in a simple way and exploit the enhancements of given here, in particular its uniform method for generating independently verifiable optimality proofs.

AIJ Journal 2008 Journal Article

A logical approach to efficient Max-SAT solving

• Javier Larrosa
• Federico Heras
• Simon de Givry

Weighted Max-SAT is the optimization version of SAT and many important problems can be naturally encoded as such. Solving weighted Max-SAT is an important problem from both a theoretical and a practical point of view. In recent years, there has been considerable interest in finding efficient solving techniques. Most of this work focuses on the computation of good quality lower bounds to be used within a branch and bound DPLL-like algorithm. Most often, these lower bounds are described in a procedural way. Because of that, it is difficult to realize the logic that is behind. In this paper we introduce an original framework for Max-SAT that stresses the parallelism with classical SAT. Then, we extend the two basic SAT solving techniques: search and inference. We show that many algorithmic tricks used in state-of-the-art Max-SAT solvers are easily expressible in logical terms in a unified manner, using our framework. We also introduce an original search algorithm that performs a restricted amount of weighted resolution at each visited node. We empirically compare our algorithm with a variety of solving alternatives on several benchmarks. Our experiments, which constitute to the best of our knowledge the most comprehensive Max-SAT evaluation ever reported, demonstrate the practical usability of our approach.

SAT Conference 2008 Conference Paper

A Max-SAT Inference-Based Pre-processing for Max-Clique

• Federico Heras
• Javier Larrosa

Abstract In this paper we propose the use of two resolution-based rules for the Max-SAT encoding of the Maximum Clique Problem. These rules simplify the problem instance in such a way that a lower bound of the optimum becomes explicit. Then, we present a pre-processing procedure that applies such rules. Empirical results show evidence that the lower bound obtained with the pre-processing outperforms previous approaches. Finally, we show that a branch-and-bound Max-SAT solver fed with the simplified problem can be boosted several orders of magnitude.

SAT Conference 2007 Conference Paper

MiniMaxSat: A New Weighted Max-SAT Solver

• Federico Heras
• Javier Larrosa
• Albert Oliveras

Abstract In this paper we introduce MiniMaxSat, a new Max-SAT solver that incorporates the best SAT and Max-SAT techniques. It can handle hard clauses (clauses of mandatory satisfaction as in SAT), soft clauses (clauses whose falsification is penalized by a cost as in Max-SAT) as well as pseudo-boolean objective functions and constraints. Its main features are: learning and backjumping on hard clauses; resolution-based and subtraction-based lower bounding; and lazy propagation with the two-watched literals scheme. Our empirical evaluation on a wide set of optimization benchmarks indicates that its performance is usually close to the best specialized alternative and, in some cases, even better.

ECAI Conference 2006 Conference Paper

Multi-Objective Propagation in Constraint Programming

• Emma Rollon
• Javier Larrosa

Bounding constraints are used to bound the tolerance of solutions under certain undesirable features. Standard solvers propagate them one by one. Often times, it is easy to satisfy them independently, but difficult to satisfy them simultaneously. Therefore, the standard propagation methods fail. In this paper we propose a novel approach inspired in multi-objective optimization. We compute a multi-objective lower bound set that, if large enough, can be used to detect the inconsistency of the problem. Our experiments on two domains inspired in real-world problems show that propagation of additive bounding constraints using our approach is clearly superior than previous approaches.

IJCAI Conference 2005 Conference Paper

Improving Tree Decomposition Methods With Function Filtering

• Martí Sánchez
• Javier Larrosa
• Pedro

IJCAI Conference 2005 Conference Paper

Resolution in Max-SAT and its relation to local consistency in weighted CSPs

• Javier Larrosa
• Federico

Max-SAT is an optimization version of the wellknown SAT problem. It is of great importance from both a theoretical and a practical point of view. In recent years, there has been considerable interest in finding efficient solving techniques [Alsinet et al. , 2003; Xing and Zhang, 2004; Shen and Zhang, 2004; de Givry et al. , 2003]. Most of this work focus on the computation of good quality lower bounds to be used within a branch and bound algorithm. Unfortunately, lower bounds are described in a procedural way. Because of that, it is difficult to realize the logic that is behind. In this paper we introduce a logical framework for Max-SAT solving. Using this framework, we introduce an extension of the Davis-Putnam algorithm (that we call Max-DPLL) and the resolution rule. Our framework has the advantage of nicely integrating branch and bound concepts such as the lower and upper bound, as well as hiding away implementation details. We show that Max-DPLL augmented with a restricted form of resolution at each branching point is an effective solving strategy. We also show that the resulting algorithm is closely related with some local consistency properties developed for weighted constraint satisfaction problems.

AIJ Journal 2005 Journal Article

Unifying tree decompositions for reasoning in graphical models

• Kalev Kask
• Rina Dechter
• Javier Larrosa
• Avi Dechter

The paper provides a unifying perspective of tree-decomposition algorithms appearing in various automated reasoning areas such as join-tree clustering for constraint-satisfaction and the clique-tree algorithm for probabilistic reasoning. Within this framework, we introduce a new algorithm, called bucket-tree elimination (BTE), that extends Bucket Elimination (BE) to trees, and show that it can provide a speed-up of n over BE for various reasoning tasks. Time-space tradeoffs of tree-decomposition processing are analyzed.

AIJ Journal 2004 Journal Article

Solving weighted CSP by maintaining arc consistency

• Javier Larrosa
• Thomas Schiex

Recently, a general definition of arc consistency (AC) for soft constraint frameworks has been proposed by T. Schiex [Proc. CP-2000, Singapore, 2000, pp. 411–424]. In this paper we specialize this definition to weighted CSP and introduce two O(ed 3) enforcing algorithms. Then, we refine the definition and introduce a stronger form of arc consistency (AC∗) along with two O(n 2 d 2+ed 3) algorithms. As in the CSP case, an important application of AC is to combine it with search. We empirically demonstrate that a branch and bound algorithm that maintains either AC or AC∗ is a state-of-the-art general solver for weighted CSP. Our experiments cover binary Max-CSP and Max-SAT problems.

ECAI Conference 2004 Conference Paper

Using Constraints with Memory to Implement Variable Elimination

• Martí Sánchez-Fibla
• Pedro Meseguer
• Javier Larrosa

IJCAI Conference 2003 Conference Paper

In the quest of the best form of local consistency for Weighted CSP

• Javier Larrosa
• Thomas Schiex

The weighted CSP (WCSP) framework is a soft constraint framework with a wide range of applications. In this paper, we consider the problem of maintaining local consistency during search for solving WCSP. We first refine the notions of directional arc consistency (DAC) and full directional arc consistency (FDAC) introduced in [Cooper, 2003] for binary WCSP, define algorithms that enforce these properties and study their complexities. We then consider algorithms that maintain either arc consistency (AC), DAC or FDAC during search. The efficiency of these algorithms is empirically studied. It appears that despite its high theoretical cost, the strongest FDAC property is the best choice.

AAAI Conference 2002 Conference Paper

Node and Arc Consistency in Weighted CSP

• Javier Larrosa

Recently, a general definition of arc consistency (AC) for soft constraint frameworks has been proposed (Schiex 2000). In this paper we specialize this definition to weighted CSP and introduce a O(ed3 ) algorithm. Then, we refine the definition and introduce a stronger form of arc consistency (AC*) along with a O(n2 d3 ) algorithm. We empirically demonstrate that AC* is likely to be much better than AC in terms of pruned values.

AIJ Journal 2002 Journal Article

On forward checking for non-binary constraint satisfaction

• Christian Bessière
• Pedro Meseguer
• Eugene C. Freuder
• Javier Larrosa

Solving non-binary constraint satisfaction problems, a crucial challenge today, can be tackled in two different ways: translating the non-binary problem into an equivalent binary one, or extending binary search algorithms to solve directly the original problem. The latter option raises some issues when we want to extend definitions written for the binary case. This paper focuses on the well-known forward checking algorithm, and shows that it can be generalized to several non-binary versions, all fitting its binary definition. The classical non-binary version, proposed by Van Hentenryck, is only one of these generalizations.

ECAI Conference 2002 Conference Paper

Pseudo-tree Search with Soft Constraints

• Javier Larrosa
• Pedro Meseguer
• Martí Sánchez-Fibla

AIJ Journal 1999 Journal Article

Maintaining reversible DAC for Max-CSP

• Javier Larrosa
• Pedro Meseguer
• Thomas Schiex

We introduce an exact algorithm for maximizing the number of satisfied constraints in an overconstrained CSP (Max-CSP). The algorithm, which can also solve weighted CSP, probabilistic CSP and other similar problems, is based on directed arc-inconsistency counts (DAC). The usage of DAC increases the lower bound of branch and bound based algorithms for Max-CSP, improving their efficiency. Originally, DAC were defined following a static variable ordering. In this paper, we relax this condition, showing how DAC can be defined from a directed constraint graph. These new graph-based DAC can be effectively used for lower bound computation. Interestingly, any directed constraint graph of the considered problem is suitable for DAC computation, so the selected graph can change dynamically during search, aiming at optimizing the exploitation of directed arc-inconsistencies. In addition, directed arc-inconsistencies are maintained during search, propagating the effect of value pruning. With these new elements we present the PFC maintaining reversible DAC algorithm (PFC-MRDAC), a natural successor of PFC-DAC for Max-CSP. We provide experimental evidence for the superiority of PFC-MRDAC on random and real overconstrained CSP instances, including problems with weighted constraints.

ECAI Conference 1998 Conference Paper

Partial Lazy Forward Checking for MAX-CSP

• Javier Larrosa
• Pedro Meseguer

AAAI Conference 1998 Conference Paper

Reversible DAC and Other Improvements for Solving Max-CSP

• Javier Larrosa
• Thomas Schiex

ECAI Conference 1996 Conference Paper

Phase Transition in MAX-CSP

• Javier Larrosa
• Pedro Meseguer

IJCAI Conference 1995 Conference Paper

Constraint Satisfaction as Global Optimization

• Pedro Meseguer
• Javier Larrosa

We present a optimization formulation for discrete binary CSP, based on the construction of a continuous function A(P) whose global maximum represents the best possible solution for that problem. By the best possible solution we mean either (i) a solution of the problem, if it is solvable, or (ii) a partial solution violating a minimal number of constraints, if the problem is unsolvable. This approach is based on relaxation labeling techniques used to enforce consistency in image interpretation. We have used a projected gradient ascent algorithm to maximize A(P) on the n-queens problem obtaining good results but with a high computational cost. To elude this problem, we have developed a heuristic for variable and value selection inspired in the direction in which A(P) is maximized. We have tested this heuristic with forward checking on several classes of CSP.