Federico Heras

IJCAI Conference 2013 Conference Paper

On Computing Minimal Correction Subsets

• Joao Marques-Silva
• Federico Heras
• Mikolas Janota
• Alessandro Previti
• Anton Belov

A set of constraints that cannot be simultaneously satisfied is over-constrained. Minimal relaxations and minimal explanations for over-constrained problems find many practical uses. For Boolean formulas, minimal relaxations of over-constrained problems are referred to as Minimal Correction Subsets (MCSes). MCSes find many applications, including the enumeration of MUSes. Existing approaches for computing MCSes either use a Maximum Satisfiability (MaxSAT) solver or iterative calls to a Boolean Satisfiability (SAT) solver. This paper shows that existing algorithms for MCS computation can be inefficient, and so inadequate, in certain practical settings. To address this problem, this paper develops a number of novel techniques for improving the performance of existing MCS computation algorithms. More importantly, the paper proposes a novel algorithm for computing MCSes. Both the techniques and the algorithm are evaluated empirically on representative problem instances, and are shown to yield the most efficient and robust solutions for MCS computation.

SAT Conference 2012 Conference Paper

Improvements to Core-Guided Binary Search for MaxSAT

• António Morgado 0001
• Federico Heras
• João Marques-Silva 0001

Abstract Maximum Satisfiability (MaxSAT ) and its weighted variants are well-known optimization formulations of Boolean Satisfiability ( SAT ). Motivated by practical applications, recent years have seen the development of core-guided algorithms for MaxSAT. Among these, core-guided binary search with disjoint cores ( BCD ) represents a recent robust solution. This paper identifies a number of inefficiencies in the original BCD algorithm, related with the computation of lower and upper bounds during the execution of the algorithm, and develops solutions for them. In addition, the paper proposes two additional novel techniques, which can be implemented on top of core-guided MaxSAT algorithms that maintain both lower and upper bounds. Experimental results, obtained on representative problem instances, indicate that the proposed optimizations yield significant performance gains, and allow solving more problem instances.

AAAI Conference 2011 Conference Paper

Core-Guided Binary Search Algorithms for Maximum Satisfiability

• Federico Heras
• Antonio Morgado
• Joao Marques-Silva

Several MaxSAT algorithms based on iterative SAT solving have been proposed in recent years. These algorithms are in general the most efficient for real-world applications. Existing data indicates that, among MaxSAT algorithms based on iterative SAT solving, the most efficient ones are core-guided, i. e. algorithms which guide the search by iteratively computing unsatisfiable subformulas (or cores). For weighted MaxSAT, core-guided algorithms exhibit a number of important drawbacks, including a possibly exponential number of iterations and the use of a large number of auxiliary variables. This paper develops two new algorithms for (weighted) MaxSAT that address these two drawbacks. The first MaxSAT algorithm implements core-guided iterative SAT solving with binary search. The second algorithm extends the first one by exploiting disjoint cores. The empirical evaluation shows that core-guided binary search is competitive with current MaxSAT solvers.

IJCAI Conference 2011 Conference Paper

Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms

• Federico Heras
• Joao Marques-Silva

This paper proposes the integration of the resolution rule for Max-SAT with unsatisfiability-based Max-SAT solvers. First, we show that the resolution rule for Max-SAT can be safely applied as dictated by the resolution proof associated with an unsatisfiable core when such proof is read-once, that is, each clause is used at most once in the resolution process. Second, we study how this property can be integrated in an unsatisfiability-based solver. In particular, the resolution rule for Max-SAT is applied to read-once proofs or to read-once subparts of a general proof. Finally, we perform an empirical investigation on structured instances from recent Max-SAT evaluations. Preliminary results show that the use of read-once resolution substantially improves the performance of the solver.

AIJ Journal 2008 Journal Article

A logical approach to efficient Max-SAT solving

• Javier Larrosa
• Federico Heras
• Simon de Givry

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.

IJCAI Conference 2005 Conference Paper

Existential arc consistency: Getting closer to full arc consistency in weighted CSPs

• Simon de Givry
• Federico Heras
• Matthias Zytnicki
• Javier

The weighted CSP framework is a soft constraint framework with a wide range of applications. Most current state-of-the-art complete solvers can be described as a basic depth-first branch and bound search that maintain some form of arc consistency during the search. In this paper we introduce a new stronger form of arc consistency, that we call existential directional arc consistency and we provide an algorithm to enforce it. The efficiency of the algorithm is empirically demonstrated in a variety of domains.