Souheib Baarir

An experience report on the optimization of the product configuration system of Renault

By Hao Xu, Souheib Baarir, Tewfik Ziadi, Siham Essodaigui, Yves Bossu, Lom Messan Hillah

2023-04-03

In Proceedings of the 26th international conference on engineering of complex computer systems (ICECCS’23)

Abstract The problem of configuring a variability model is widespread in many different domains. A leading automobile manufacturer has developed its technology internally to model vehicle diversity. This technology relies on the approach known as knowledge compilation to explore the configurations space. However, the growing variability and complexity of the vehicles’ range hardens the space representation problem and impacts performance requirements. This paper tackles these issues by exploiting symmetries that represent isomorphic parts in the configurations space.

Continue reading

Optimization of the product configuration system of renault

By Hao Xu, Souheib Baarir, Tewfik Ziadi, Siham Essodaigui, Yves Bossu, Lom Messan Hillah

2023-04-03

In Proceedings of the 38th ACM/SIGAPP symposium on applied computing (SAC’23)

Abstract The problem of configuring a variability model is widespread in many different domains. Renault has developed its technology internally to model vehicle diversity. This technology relies on the approach known as knowledge compilation to explore the configurations space. However, the growing variability and complexity of the vehicles’ range hardens the space representation problem and impacts performance requirements. This paper tackles these issues by exploiting symmetries that represent isomorphic parts in the configurations space.

Continue reading

Towards better heuristics for solving bounded model checking problems

Abstract This paper presents a new way to improve the performance of the SAT-based bounded model checking problem on sequential and parallel procedures by exploiting relevant information identified through the characteristics of the original problem. This led us to design a new way of building interesting heuristics based on the structure of the underlying problem. The proposed methodology is generic and can be applied for any SAT problem. This paper compares the state-of-the-art approaches with two new heuristics for sequential procedures: Structure-based and Linear Programming heuristics.

Continue reading

Tuning SAT solvers for LTL model checking

By Anissa Kheireddine, Étienne Renault, Souheib Baarir

2022-12-09

In Proceedings of the 29th asia-pacific software engineering conference (APSEC’22)

Abstract Bounded model checking (BMC) aims at checking whether a model satisfies a property. Most of the existing SAT-based BMC approaches rely on generic strategies, which are supposed to work for any SAT problem. The key idea defended in this paper is to tune SAT solvers algorithm using: (1) a static classification based on the variables used to encode the BMC into a Boolean formula; (2) and use the hierarchy of Manna&Pnueli that classifies any property expressed through Linear-time Temporal Logic (LTL).

Continue reading

CosySEL: Improving SAT solving using local symmetries

By S. Saouli, Souheib Baarir, C. Dutheillet, J. Devriendt

2022-12-08

In 24th international conference on verification, model checking, and abstract interpretation

Abstract Many satisfiability problems exhibit symmetry properties. Thus, the development of symmetry exploitation techniques seems a natural way to try to improve the efficiency of solvers by preventing them from exploring isomorphic parts of the search space. These techniques can be classified into two categories: dynamic and static symmetry breaking. Static approaches have often appeared to be more effective than dynamic ones. But although these approaches can be considered as complementary, very few works have tried to combine them.

Continue reading

Diversifying a parallel SAT solver with bayesian moment matching

By V. Vallade, S. Nejati, J. Sopena, V. Ganesh, Souheib Baarir

2022-12-08

In Symposium on dependable software engineering theories, tools and applications

Abstract In this paper, we present a Bayesian Moment Matching (BMM) in-processing technique for Conflict-Driven Clause-Learning (CDCL) SAT solvers. BMM is a probabilistic algorithm which takes as input a Boolean formula in conjunctive normal form and a prior on a possible satisfying assignment, and outputs a posterior for a new assignment most likely to maximize the number of satisfied clauses. We invoke this BMM method, as an in-processing technique, with the goal of updating the polarity and branching activity scores.

Continue reading

Towards better heuristics for solving bounded model checking problems

By Anissa Kheireddine, Étienne Renault, Souheib Baarir

2021-08-31

In Proceedings of the 27th international conference on principles and practice of constraint programmings (CP’21)

Abstract This paper presents a new way to improve the performance of the SAT-based bounded model checking problem by exploiting relevant information identified through the characteristics of the original problem. This led us to design a new way of building interesting heuristics based on the structure of the underlying problem. The proposed methodology is generic and can be applied for any SAT problem. This paper compares the state-of-the-art approach with two new heuristics: Structure-based and Linear Programming heuristics and show promising results.

Continue reading

On the usefulness of clause strengthening in parallel SAT solving

By Vincent Vallade, Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Fabrice Kordon

2020-08-01

In Proceedings of the 12th NASA formal methods symposium (NFM’20)

Abstract In the context of parallel SATisfiability solving, this paper presents an implementation and evaluation of a clause strengthening algorithm. The developed component can be easily combined with (virtually) any CDCL-like SAT solver. Our implementation is integrated as a part of Painless, a generic and modular framework for building parallel SAT solvers.

Continue reading

Community and LBD-based clause sharing policy for parallel SAT solving

By Vincent Vallade, Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Vijay Ganesh, Fabrice Kordon

2020-06-01

In Proceedings of the 23rd international conference on theory and applications of satisfiability testing (SAT’20)

Abstract Modern parallel SAT solvers rely heavily on effective clause sharing policies for their performance. The core problem being addressed by these policies can be succinctly stated as “the problem of identifying high-quality learnt clauses” that when shared between the worker nodes of parallel solvers results in improved performance than otherwise. The term “high-quality clauses” is often defined in terms of metrics that solver designers have identified over years of empirical study.

Continue reading

Modular and efficient divide-and-conquer SAT solver on top of the Painless framework

By Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Fabrice Kordon

2019-02-13

In Proceedings of the 25th international conference on tools and algorithms for the construction and analysis of systems (TACAS’19)

Abstract Over the last decade, parallel SATisfiability solving has been widely studied from both theoretical and practical aspects. There are two main approaches. First, divide-and-conquer (D&C) splits the search space, each solver being in charge of a particular subspace. The second one, portfolio launches multiple solvers in parallel, and the first to find a solution ends the computation. However although D&C based approaches seem to be the natural way to work in parallel, portfolio ones experimentally provide better performances.

Continue reading