Speaker
Prof.
Tomi Janunen
(Aalto University)
Description
Propositional satisfiability (SAT) solvers provide a promising
computational platform for declarative problem solving. Over
the years, a great variety of benchmark problems has
emerged to help with the systematic evaluation of SAT
solvers under development. Both highly structural and
random benchmark instances are used and the
performance of SAT solvers on such instances depends
much on the underlying search paradigm. In this talk, I
present a compact way to translate logic programs, subject
to answer-set semantics proposed by Gelfond and Lifschitz,
into set of clauses so that satisfying assignments
correspond to answer sets. Thus, on one hand, SAT solvers
can harnessed as black boxes to the task of computing
answer sets. On the other hand, the translations provide
an easy way to generate challeging structural (or partly
randomized) benchmark instances for SAT solvers. Typical
answer-set programs involve natural parameters that can
be used for scaling the hardness of the resulting instances.
In the experimental part, I discuss the potential of SAT
solvers when solving NP-complete problems from the 2nd
Answer Set Programming Competition.
Primary author
Prof.
Tomi Janunen
(Aalto University)
