-
Chapter and Conference Paper
Feature Necessity & Relevancy in ML Classifier Explanations
Given a machine learning (ML) model and a prediction, explanations can be defined as sets of features which are sufficient for the prediction. In some applications, and besides asking for an explanation, it is...
-
Article
Open AccessArgumentation Reasoning with Graph Isomorphism Networks for Reddit Conversation Analysis
The automated analysis of different trends in online debating forums is an interesting tool for sampling the agreement between citizens in different topics. In previous work, we have defined computational mode...
-
Article
Using convolutional neural networks for classification of malware represented as images
The number of malicious files detected every year are counted by millions. One of the main reasons for these high volumes of different files is the fact that, in order to evade detection, malware authors add m...
-
Chapter and Conference Paper
An End-to-End Deep Learning Architecture for Classification of Malware’s Binary Content
In traditional machine learning techniques for malware detection and classification, significant efforts are expended on manually designing features based on expertise and domain-specific knowledge. These solu...
-
Article
Open AccessBlacklist muti-objective genetic algorithm for energy saving in heterogeneous environments
Reducing energy consumption in large-scale computing facilities has become a major concern in recent years. Most of the techniques have focused on determining the computing requirements based on load predictio...
-
Article
On the performance of MaxSAT and MinSAT solvers on 2SAT-MaxOnes
We analyze and compare two solvers for Boolean optimization problems: WMaxSatz, a solver for Partial MaxSAT, and MinSatz, a solver for Partial MinSAT. Both MaxSAT and MinSAT are similar, but previous results i...
-
Chapter and Conference Paper
Slowdown-Guided Genetic Algorithm for Job Scheduling in Federated Environments
Large-scale federated environments have emerged to meet the requirements of increasingly demanding scientific applications. However, the seemingly unlimited availability of computing resources and heterogeneit...
-
Article
Iterative and core-guided MaxSAT solving: A survey and assessment
Maximum Satisfiability (MaxSAT) is an optimization version of SAT, and many real world applications can be naturally encoded as such. Solving MaxSAT is an important problem from both a theoretica...
-
Chapter and Conference Paper
Maximal Falsifiability
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...
-
Chapter
Algorithms for Maximum Satisfiability Using Unsatisfiable Cores
Many decision and optimization problems in electronic design automation (EDA) can be solved with Boolean satisfiability (SAT). These include binate covering problem (BCP), pseudo-Boolean optimization (PBO), qu...
-
Chapter and Conference Paper
Analyzing the Instances of the MaxSAT Evaluation
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: ...
-
Article
Resolution-based lower bounds in MaxSAT
The lower bound (LB) implemented in branch and bound MaxSAT solvers is decisive for obtaining a competitive solver. In modern solvers like MaxSatz and MiniMaxSat, the LB relies on the cooperation of the undere...
-
Chapter and Conference Paper
Exploiting Cycle Structures in Max-SAT
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{...
-
Chapter and Conference Paper
Algorithms for Weighted Boolean Optimization
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 propos...
-
Article
An efficient solver for weighted Max-SAT
We present a new branch and bound algorithm for weighted Max-SAT, called Lazy which incorporates original data structures and inference rules, as well as a lower bound of better quality. We provide experimental e...
-
Chapter and Conference Paper
Transforming Inconsistent Subformulas in MaxSAT Lower Bound Computation
We define a new heuristic that guides the application of cycle resolution (CR) in MaxSAT, and show that it produces better lower bounds than those obtained by applying CR exhaustively as in Max-DPLL, and by ap...
-
Chapter and Conference Paper
Exploiting Unit Propagation to Compute Lower Bounds in Branch and Bound Max-SAT Solvers
One of the main differences between complete SAT solvers and exact Max-SAT solvers is that the former make an intensive use of unit propagation at each node of the proof tree while the latter, in order to ensu...
-
Chapter and Conference Paper
Improved Exact Solvers for Weighted Max-SAT
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.
-
Chapter and Conference Paper
A Max-SAT Solver with Lazy Data Structures
We present a new branch and bound algorithm for Max-SAT which incorporates original lazy data structures, a new variable selection heuristics and a lower bound of better quality. We provide experimental eviden...
-
Chapter and Conference Paper
Improved Branch and Bound Algorithms for Max-2-SAT and Weighted Max-2-SAT
We developed novel branch and bound algorithms for solving Max-SAT and weighted Max-SAT, which are variants of the algorithm of Borchers & Furman (BFA) [1]. We improved BFA by (i) defining a lower bound of bet...
