Youssef Hamadi

AAMAS Conference 2024 Conference Paper

Towards Socially-Acceptable Multi-Criteria Resolution of the 4D-Contracts Repair Problem

• Youssef Hamadi
• Gauthier Picard

We use multi-agent systems to solve conflicts between drone flight paths (4D contracts) in urban traffic, installing safety and service quality. Intuitive corrective actions are chosen considering delay, quality, and energy. We explore different algorithms based on graph search, auctions, and distributed optimization for decision-making and action evaluation. We test these in a simulated surveillance scenario with unforeseen emergency trajectories.

AAAI Conference 2015 Conference Paper

Stochastic Local Search for Satisfiability Modulo Theories

• Andreas Fröhlich
• Armin Biere
• Christoph Wintersteiger
• Youssef Hamadi

Satisfiability Modulo Theories (SMT) is essential for many practical applications, e. g. , in hard- and software verification, and increasingly also in other scientific areas like computational biology. A large number of applications in these areas benefit from bit-precise reasoning over finite-domain variables. Current approaches in this area translate a formula over bit-vectors to an equisatisfiable propositional formula, which is then given to a SAT solver. In this paper, we present a novel stochastic local search (SLS) algorithm to solve SMT problems, especially those in the theory of bit-vectors, directly on the theory level. We explain how several successful techniques used in modern SLS solvers for SAT can be lifted to the SMT level. Experimental results show that our approach can compete with state-of-the-art bit-vector solvers on many practical instances and, sometimes, outperform existing solvers. This offers interesting possibilities in combining our approach with existing techniques, and, moreover, new insights into the importance of exploiting problem structure in SLS solvers for SAT. Our approach is modular and, therefore, extensible to support other theories, potentially allowing SLS to become part of the more general SMT framework.

ECAI Conference 2012 Conference Paper

A Multi-objective Approach to Balance Buildings Construction Cost and Energy Efficiency

• Álvaro Fialho
• Youssef Hamadi
• Marc Schoenauer

The issue of energy efficiency of buildings must be taken into account as early as possible in the life cycle of buildings, i. e. , during the architectural phase. The orientation of the building, its structure, the choice of materials, windows and other openings, all these aspects participate to the future energy consumption profile in a complex and highly non-linear way. Furthermore, even though sustainability is today a major objective, the cost of the construction remains another decision factor that cannot be underestimated - and energy efficiency and cost are alas contradictory objectives. Thus the problem of designing efficient buildings is a multi-objective problem. This work tackles this problem using a state-of-the-art evolutionary multi-objective algorithm, HYPE, tightly linked to an energy con-sumption simulation program, EnergyPlus. Several parameters defining the design are considered, namely the orientation angle, the materials used for the thermal insulation of the walls, and the size of the windows in order to explore daylighting. In the end, a diverse set of Pareto optimal solutions (i. e. , solutions offering optimal trade-offs between both objectives) are proposed to the decision maker. The approach is validated on five buildings of different categories, where energy savings of up to 20% compared to the original design are automatically obtained.

AAAI Conference 2012 Conference Paper

Seven Challenges in Parallel SAT Solving

• Youssef Hamadi
• Christoph Wintersteiger

This paper provides a broad overview of the situation in the area of Parallel Search with a specific focus on Parallel SAT Solving. A set of challenges to researchers is presented which, we believe, must be met to ensure the practical applicability of Parallel SAT Solvers in the future. All these challenges are described informally, but put into perspective with related research results, and a (subjective) grading of difficulty for each of them is provided.

SoCS Conference 2010 Conference Paper

Adaptive K-Parallel Best-First Search: A Simple but Efficient Algorithm for Multi-Core Domain-Independent Planning

• Vincent Vidal 0001
• Lucas Bordeaux
• Youssef Hamadi

Motivated by the recent hardware evolution towards multi-core machines, we investigate parallel planning techniques in a shared-memory environment. We consider, more specifically, parallel versions of a best-first search algorithm that run K threads, each expanding the next best node from the open list. We show that the proposed technique has a number of advantages. First, it is (reasonably) simple: we show how the algorithm can be obtained from a sequential version mostly by adding parallel annotations. Second, we conduct an extensive empirical study that shows that this approach is quite effective. It is also dynamic in the sense that the number of nodes expanded in parallel is adapted during the search. Overall we show that the approach is promising for parallel domain-independent, suboptimal planning.

IJCAI Conference 2009 Conference Paper

• Youssef Hamadi
• Said Jabbour
• Lakhdar Sais

Conflict driven clause learning, one of the most important component of modern SAT solvers, is also recognized as very important in parallel SAT solving. Indeed, it allows clause sharing between multiple processing units working on related (sub- )problems. However, without limitation, sharing clauses might lead to an exponential blow up in communication or to the sharing of irrelevant clauses. This paper, proposes two innovative policies to dynamically adjust the size of shared clauses between any pair of processing units. The first approach controls the overall number of exchanged clauses whereas the second additionally exploits the relevance quality of shared clauses. Experimental results show important improvements of the state-of the-art parallel SAT solver.

IJCAI Conference 2009 Conference Paper

• Lucas Bordeaux
• Youssef Hamadi
• Horst Samulowitz

SAT Conference 2008 Conference Paper

A Generalized Framework for Conflict Analysis

• Gilles Audemard
• Lucas Bordeaux
• Youssef Hamadi
• Saïd Jabbour
• Lakhdar Saïs

Abstract This paper presents an extension of Conflict Driven Clauses Learning (CDCL). It relies on an extended notion of implication graph containing additional arcs, called inverse arcs. These are obtained by taking into account the satisfied clauses of the formula, which are usually ignored by conflict analysis. This extension captures more conveniently the whole propagation process, and opens new perspectives for CDCL-based approaches. Among other benefits, our extension leads to a new conflict analysis scheme that exploits the additional arcs to back-jump to higher levels. Experimental results show that the integration of our generalized conflict analysis scheme within two state-of-the-art solvers improves their performance.

ECAI Conference 2008 Conference Paper

Vivifying Propositional Clausal Formulae

• Cédric Piette
• Youssef Hamadi
• Lakhdar Saïs

In this paper, we present a new way to preprocess Boolean formulae in Conjunctive Normal Form (CNF). In contrast to most of the current pre-processing techniques, our approach aims at improving the filtering power of the original clauses while producing a small number of additional and relevant clauses. More precisely, an incomplete redundancy check is performed on each original clauses through unit propagation, leading to either a sub-clause or to a new relevant one generated by the clause learning scheme. This preprocessor is empirically compared to the best existing one in terms of size reduction and the ability to improve a state-of-the-art satisfiability solver.

ECAI Conference 2006 Conference Paper

Distributed Log-Based Reconciliation

• Yek Loong Chong
• Youssef Hamadi

Computer Supported Cooperative Work (CSCW) defines software tools and technology to support groups of people working together on a project, often at different sites [5]. In this work, we present four distributed algorithms for log-based reconciliation, an important NP-hard problem occurring in CSCW. Our methods remove the classical drawbacks of centralized systems like single point of failure, performance bottleneck and loss of autonomy. The problem is formalized using the Distributed Constraint Satisfaction paradigm (DisCSP). In the worst case, the message passing complexity of our methods range from O(p 2 ) to O(2 p ) in a system of p nodes. Experimental results confirm our theoretical analysis and allow us to establish quality and efficiency trade-off for each method.

ECAI Conference 1998 Conference Paper

Distributed Intelligent Backtracking

• Youssef Hamadi
• Christian Bessière
• Joël Quinqueton