|
|
Séminaires pôle IA
-
15 mars 2013 -- 14h, salle des séminaires : Felip Manyà -- CSIC Barcelone
Encoding and Solving Optimization Problems with MinSAT and MaxSAT
SAT offers a competitive framework for solving challenging decision problems in domains as diverse as hardware and software verification,
artificial intelligence, and operations research. In recent years, the success of SAT has led to investigate several extensions of SAT,
including Satisfiability Modulo Theories (SMT), Quantified Boolean Formulas (QBF), Pseudo-Boolean Constraints (PB), Model Counting (MC),
Maximum Satisfiability (MaxSAT), and Minimum Satisfiability (MinSAT).
In this talk we will focus on how MaxSAT and MinSAT can be used to solve NP-hard optimization problems. Firstly, we will define MaxSAT, MinSAT and existing variants of these problems. Secondly, we will give an overview of the most recent solving techniques that have been devised for these problems. Thirdly, we will present how NP-hard problems can be modeled as MaxSAT/MinSAT instances, and in particular how MaxCSP can be encoded into MaxSAT/MinSAT. Fourthly, we will report on empirical results that show that MaxSAT/MinSAT are very competitive on certain optimization problems. Finally, we will point out promising research directions.
-
22 mars 2013 : Richard Booth -- Université du Luxembourg
Quantifying disagreement in argument-based reasoning
An argumentation framework can be seen as expressing, in an abstract way, the conflicting information of an underlying logical knowledge
base. This conflicting information often allows for the presence of more than one possible reasonable position (extension/labelling) which
one can take. A relevant question, therefore, is how much these positions differ from each other. In this talk, we will examine the issue of how to define meaningful measures of distance between the (complete) labellings of a given argumentation framework. We provide concrete distance measures based on argument-wise label difference, as well as based on the notion of *issues*, and examine their properties.
-
5 avril 2013 : Christophe Lecoutre -- CRIL
|
| | |