[Date Prev][Date Next][Date Index]

Talk Announcement - Research Seminar @ DBAI

Der Arbeitsbereich für Datenbanken und Artificial Intelligence am Institut
für Informationssysteme lädt zu folgenden Vorträgen am 

Montag, 15.6. 2009, im Seminarraum 184/2, 3.Stock, Favoritenstr. 9-11, ein:


14:00 Uhr:  Max-ASP -- Maximum Satisfiability of Answer Set Programs 
            (Emilia Oikarinen, Helsinki University of Technology - TKK)

15:00 Uhr:  Results on the Power of Structure-Based Decision Heuristics for SAT
            (Matti Järvisalo, Helsinki University of Technology - TKK)


Mo, 15.6. 2009. 14:00 Uhr, Seminarraum 184/2

Max-ASP: Maximum Satisfiability of Answer Set Programs

We study answer set programming (ASP) in the generalized context 
of soft constraints and optimization criteria. In analogy to the 
well-known Max-SAT problem of maximum satisfiability of propositional 
formulas, we introduce the problems of unweighted and weighted Max-ASP. 
Given a normal logic program P, in Max-ASP the goal is to find so called 
optimal Max-ASP models, which minimize the total cost of unsatisfied rules 
in P and are at the same time answer sets for the set of satisfied rules 
in P. Inference rules for Max-ASP are developed, resulting in a complete 
branch-and-bound algorithm for finding optimal models for weighted Max-ASP 
instances. The Max-ASP problem is also compared to earlier proposed 
related concepts in the context of ASP. Furthermore, translations between 
Max-ASP and Max-SAT are studied.
Joint work with Matti Järvisalo.

Emilia Oikarinen

Department of Information and Computer Science
Helsinki University of Technology - TKK


Mo, 15.6. 2009. 15:00 Uhr, Seminarraum 184/2

Results on the Power of Structure-Based Decision Heuristics for SAT

Constraint reasoning techniques based on Boolean satisfiability (SAT) 
have proven extremely effective for solving hard, industrially relevant 
combinatorial problems in domains such as hardware and software 
verification and AI planning. In the SAT-based approaches, a problem is 
encoded in propositional logic, and this declarative specification is 
then solved using general-purpose SAT solvers.
Understanding the effect of the inherent structural properties of 
real-world SAT instances is considered a key aspect in developing 
increasingly efficient and robust SAT solvers.  Complete, DPLL-style SAT 
solvers are the most efficient ones for real-world applications today. 
This is due to highly efficient, nontrivial search space traversal and 
pruning, and clause learning. One key component in driving search is the 
decision heuristics. Many different structure-based decision heuristics 
have been proposed, attempting to exploit knowledge of the underlying 
problem structure. In this talk I will present a high-level review of our 
work on analyzing the effectiveness and inherent limitations of 
structure-based decision heuristics. The main results are proof 
complexity theoretic hierarchies of heuristics, with exponential 
differences in the power of different heuristics. Practical 
implications of such heuristics have also been considered through an 
extensive experimental evaluation.
Joint work with Tommi Junttila and Ilkka Niemelä.

Matti Järvisalo

Department of Information and Computer Science
Helsinki University of Technology - TKK