Arrow Research search

Author name cluster

Jordi Planes

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers
2 author rows

Possible papers

8

KR Conference 2024 Conference Paper

Distance-Restricted Explanations: Theoretical Underpinnings & Efficient Implementation

  • Yacine Izza
  • Xuanxiang Huang
  • Antonio Morgado
  • Jordi Planes
  • Alexey Ignatiev
  • Joao Marques-Silva

The uses of machine learning (ML) have snowballed in recent years. In many cases, ML models are highly complex, and their operation is beyond the understanding of human decision-makers. Nevertheless, some uses of ML models involve high-stakes and safety-critical applications. Explainable artificial intelligence (XAI) aims to help human decision-makers in understanding the operation of such complex ML models, thus eliciting trust in their operation. Unfortunately, the majority of past XAI work is based on informal approaches, that offer no guarantees of rigor. Unsurprisingly, there exists comprehensive experimental and theoretical evidence confirming that informal methods of XAI can provide human-decision makers with erroneous information. Logic-based XAI represents a rigorous approach to explainability; it is model-based and offers the strongest guarantees of rigor of computed explanations. However, a well-known drawback of logic-based XAI is the complexity of logic reasoning, especially for highly complex ML models. Recent work proposed distance-restricted explanations, i. e. explanations that are rigorous provided the distance to a given input is small enough. Distance-restricted explainability is tightly related with adversarial robustness, and it has been shown to scale for moderately complex ML models, but the number of inputs still represents a key limiting factor. This paper investigates novel algorithms for scaling up the performance of logic-based explainers when computing and enumerating ML model explanations with a large number of inputs.

AAAI Conference 2018 Conference Paper

Classification of Malware by Using Structural Entropy on Convolutional Neural Networks

  • Daniel Gibert
  • Carles Mateu
  • Jordi Planes
  • Ramon Vicens

The number of malicious programs has grown both in number and in sophistication. Analyzing the malicious intent of vast amounts of data requires huge resources and thus, effective categorization of malware is required. In this paper, the content of a malicious program is represented as an entropy stream, where each value describes the amount of entropy of a small chunk of code in a specific location of the file. Wavelet transforms are then applied to this entropy signal to describe the variation in the entropic energy. Motivated by the visual similarity between streams of entropy of malicious software belonging to the same family, we propose a file agnostic deep learning approach for categorization of malware. Our method exploits the fact that most variants are generated by using common obfuscation techniques and that compression and encryption algorithms retain some properties present in the original code. This allows us to find discriminative patterns that almost all variants in a family share. Our method has been evaluated using the data provided by Microsoft for the BigData Innovators Gathering Anti-Malware Prediction Challenge, and achieved promising results in comparison with the State of the Art.

LPAR Conference 2013 Conference Paper

Maximal Falsifiability - Definitions, Algorithms, and Applications

  • Alexey Ignatiev
  • António Morgado 0001
  • Jordi Planes
  • João Marques-Silva 0001

Abstract Similarly to Maximum Satisfiability (MaxSAT), Minimum Satisfiability (MinSAT) is an optimization extension of the Boolean Satisfiability (SAT) decision problem. In recent years, both problems have been studied in terms of exact and approximation algorithms. In addition, the MaxSAT problem has been characterized in terms ofMaximal Satisfiable Subsets (MSSes) andMinimal Correction Subsets (MCSes), as well as Minimal Unsatisfiable Subsets (MUSes) and minimal hitting set dualization. However, and in contrast with MaxSAT, no such characterizations exist for MinSAT. This paper addresses this issue by casting the MinSAT problem in a more general framework. The paper studies Maximal Falsifiability, the problem of computing a subset-maximal set of clauses that can be simultaneously falsified, and shows that MinSAT corresponds to the complement of a largest subset-maximal set of simultaneously falsifiable clauses, i. e. the solution of the Maximum Falsifiability (MaxFalse) problem. Additional contributions of the paper include novel algorithms for Maximum and Maximal Falsifiability, as well as minimal hitting set dualization results for the MaxFalse problem. Moreover, the proposed algorithms are validated on practical instances.

SAT Conference 2011 Conference Paper

Analyzing the Instances of the MaxSAT Evaluation

  • Josep Argelich
  • Chu-Min Li 0001
  • Felip Manyà
  • Jordi Planes

Abstract The MaxSAT Evaluation [1] is an affiliated event of the SAT Conference that is held every year since 2006, and is devoted to empirically evaluate exact MaxSAT algorithms solving any of the following problems: MaxSAT, Weighted MaxSAT (WMaxSAT), Partial MaxSAT (PMaxSAT), and Weighted Partial MaxSAT (WPMaxSAT).

SAT Conference 2009 Conference Paper

Algorithms for Weighted Boolean Optimization

  • Vasco Manquinho
  • João Marques-Silva 0001
  • Jordi Planes

Abstract The Pseudo-Boolean Optimization (PBO) and Maximum Satisfiability (MaxSAT) problems are natural optimization extensions of Boolean Satisfiability (SAT). In the recent past, different algorithms have been proposed for PBO and for MaxSAT, despite the existence of straightforward mappings from PBO to MaxSAT, and vice-versa. This papers proposes Weighted Boolean Optimization (WBO), a new unified framework that aggregates and extends PBO and MaxSAT. In addition, the paper proposes a new unsatisfiability-based algorithm for WBO, based on recent unsatisfiability-based algorithms for MaxSAT. Besides standard MaxSAT, the new algorithm can also be used to solve weighted MaxSAT and PBO, handling pseudo-Boolean constraints either natively or by translation to clausal form. Experimental results illustrate that unsatisfiability-based algorithms for MaxSAT can be orders of magnitude more efficient than existing dedicated algorithms. Finally, the paper illustrates how other algorithms for either PBO or MaxSAT can be extended to WBO.

SAT Conference 2009 Conference Paper

Exploiting Cycle Structures in Max-SAT

  • Chu-Min Li 0001
  • Felip Manyà
  • Nouredine Ould Mohamedou
  • Jordi Planes

Abstract We investigate the role of cycles structures (i. e. , subsets of clauses of the form \(\bar{l}_{1}\vee l_{2}, \bar{l}_{1}\vee l_{3}, \bar{l}_{2}\vee\bar{l}_{3}\) ) in the quality of the lower bound (LB) of modern MaxSAT solvers. Given a cycle structure, we have two options: (i) use the cycle structure just to detect inconsistent subformulas in the underestimation component, and (ii) replace the cycle structure with \(\bar{l}_{1}, l_{1}\vee\bar{l}_{2}\vee\bar{l}_{3}, \bar{l}_{1}\vee l_{2}\vee l_{3}\) by applying MaxSAT resolution and, at the same time, change the behaviour of the underestimation component. We first show that it is better to apply MaxSAT resolution to cycle structures occurring in inconsistent subformulas detected using unit propagation or failed literal detection. We then propose a heuristic that guides the application of MaxSAT resolution to cycle structures during failed literal detection, and evaluate this heuristic by implementing it in MaxSatz, obtaining a new solver called MaxSatz c. Our experiments on weighted MaxSAT and Partial MaxSAT instances indicate that MaxSatz c substantially improves MaxSatz on many hard random, crafted and industrial instances.

ECAI Conference 2008 Conference Paper

A MAX-SAT Algorithm Portfolio

  • Paulo J. Matos
  • Jordi Planes
  • Florian Letombe
  • João Marques-Silva 0001

The results of the last MaxSAT Evaluations suggest there is no universal best algorithm for solving MaxSAT, as the fastest solver often depends on the type of instance. Having an oracle able to predict the most suitable MaxSAT solver for a given instance would result in the most robust solver. Inspired by the success of SATzilla for SAT, this paper describes the first approach for a portfolio of algorithms for MaxSAT. Compared to existing solvers, the resulting portfolio can achieve significant performance improvements on a representative set of instances.

SAT Conference 2005 Conference Paper

Improved Exact Solvers for Weighted Max-SAT

  • Teresa Alsinet
  • Felip Manyà
  • Jordi Planes

Abstract We present two new branch and bound weighted Max-SAT solvers ( Lazy and Lazy *) which incorporate original data structures and inference rules, and a lower bound of better quality.

v2026.09.13