Conf.dr. Stefan ANDREI
Universitatea Alexandru Ioan Cuza, Facultatea de Informatica
Iasi
Romania
-----------------------------------
          
Approximate Satisfiability Counting
-----------------------------------
          
ABSTRACT
-----------------------------------
The problem of counting satisfiability, i.e. count the number
of satisfying assignments for a SAT problem, is used successfully
in a number of problems. For example, it can provide heuristics
for guiding planning and search,  where an estimation of the
probability for a given search would help lead to a goal. Counting
satisfiability is a valuable approach for problems like constraint
satisfaction, knowledge compilation, probabilistic reasoning
and computing the permanent of a Boolean matrix. The difficulty
with counting satisfiability is that it is as  hard as NP-complete
problems, but probably much harder.  This means that solvers
to count the exact number of solutions may  need a large amount
on time on large propositional formulas.  In this talk, we provide
a fast alternative  by approximating the number of instances.
Our technique is based on successive variable and clause elimination.
Experimental results demonstrate that our technique is promising.
          
SHORT CV
-----------------------------------
Conf. dr. Stefan Andrei este cadru didactic la Facultatea de
informatica a Universitatii "Alexandru Ioan Cuza" din Iasi. A
predat cursuri de programare (limbajele C, C++, Java si Prolog),
Constructia compilatoarelor, Limbaje formale, Navigare Internet
si Sisteme distribuite. A obtinut doctoratul in domeniul informaticii
cu teza "Procesarea paralela", sustinuta la Universitatea din
Hamburg (Germania). Este preocupat de verificarea si depanarea
sistemelor in timp real si procesarea datelor in diverse limbaje
de programare. A obtinut premiile DAAD (1997), World Bank (1998-2000)
si Singapore - MIT Alliance (2002-2005).