Séminaires
Séminaire du 25 janvier 2019
Lieu
LIP6, salle 24-25/405. Instructions pour venir ici.
Programme
14h00-15h00: Susanna Donatelli (Professore di Informatica, Dipartimento di Informatica, Università di Torino, Italy); Heuristic for variable order for decision diagram: definition and evaluation
Abstract :
Decision Diagrams (DD) have been successfully used to store the state
space of large discrete event dynamic systems (DEDS), typically
described in terms of discrete variables and events. The availability
of well-established libraries, as well as more recent ones, makes the
use of DD in this context very straightforward. On the other side it
is well known that the effectiveness of a DD representation of a state
space is strongly dependent on the specific assignment of the DEDS
variable to the DD levels, an NP-complete problem. Given that a brute
force approach is not feasible, many heuristics have been defined.
This talk concentrate on heuristics for variable orders, their
definition and their evaluation. In particular I will concentrate on
heuristics that make use of structural information of the system (like
p-semiflows for Petri net), on metrics to evaluate such heuristics
and on the use of metrics as meta-heuristics for the selection of
"good" orders.
15h00-15h30 : Hakan Metin (LIP6);
Abstract : SAT solvers are now widely used to solve a large variety of problems, including formal verification of systems. SAT problems derived from such applications often exhibit symmetry properties that could be exploited to speed up their solving. Static symmetry breaking is so far the most popular approach to take advantage of symmetries. It relies on a symmetry preprocessor which augments the initial problem with constraints that force the solver to consider only a few configurations among the many symmetric ones. In this talk, we present a way to exploit symmetries during the solver search.