Johannes Fichte (Vienna University of Technology)
30/01/14 15:30 Talks
Complexity Barrier Breaking Red’s - Backdoors for ASP
Speaker:
Johannes Fichte (Vienna University of Technology)
Abstract:
Over the last two decades, propositional satisfiability (SAT) has become one of the most successful and widely applied techniques for the solution of NP-complete problems. The aim of this talk is to investigate theoretically how Sat can be utilized for the efficient solution of problems that are harder than NP or co-NP. In particular, we consider the fundamental reasoning problems in propositional disjunctive answer set programming (ASP), Brave Reasoning and Skeptical Reasoning, which ask whether a given atom is contained in at least one or in all answer sets, respectively.
We show that certain structural aspects of disjunctive logic programs can be utilized to break through this complexity barrier, using new techniques from Parameterized Complexity. In particular, we exhibit transformations from Brave and Skeptical Reasoning to Sat that run in time O(2 k n 2 ) where k is a structural parameter of the instance and n the input size. In other words, the reduction is fixed-parameter tractable for parameter k.
We think that our approach is applicable to many other hard combinatorial problems that lie beyond NP or co-NP, and thus significantly enlarge the applicability of SAT. We will sketch other applications and briefly discuss a newly introduced general theoretical framework by DeHaan and Szeider that supports the classification of parameterized problems on whether they admit such an FPT-reduction to SAT or not.
Date:
Thursday, January 30, 2014
Time:
3:30 pm - 4:30 pm
Location:
ASB Building, Room No. 9896, Simon Fraser University, Burnaby
Johannes Fichte (Vienna University of Technology)
Abstract:
Over the last two decades, propositional satisfiability (SAT) has become one of the most successful and widely applied techniques for the solution of NP-complete problems. The aim of this talk is to investigate theoretically how Sat can be utilized for the efficient solution of problems that are harder than NP or co-NP. In particular, we consider the fundamental reasoning problems in propositional disjunctive answer set programming (ASP), Brave Reasoning and Skeptical Reasoning, which ask whether a given atom is contained in at least one or in all answer sets, respectively.
We show that certain structural aspects of disjunctive logic programs can be utilized to break through this complexity barrier, using new techniques from Parameterized Complexity. In particular, we exhibit transformations from Brave and Skeptical Reasoning to Sat that run in time O(2 k n 2 ) where k is a structural parameter of the instance and n the input size. In other words, the reduction is fixed-parameter tractable for parameter k.
We think that our approach is applicable to many other hard combinatorial problems that lie beyond NP or co-NP, and thus significantly enlarge the applicability of SAT. We will sketch other applications and briefly discuss a newly introduced general theoretical framework by DeHaan and Szeider that supports the classification of parameterized problems on whether they admit such an FPT-reduction to SAT or not.
Date:
Thursday, January 30, 2014
Time:
3:30 pm - 4:30 pm
Location:
ASB Building, Room No. 9896, Simon Fraser University, Burnaby