Thesis Topic Details

Topic ID:
Parameterized Algorithms for Backdoor Detection
Serge Gaspers
Research Area:
Algorithms, Theory, Discrete Mathematics
Associated Staff
Aleksandar Ignjatovic
Topic Details
Group Suitable:
Backdoor sets aim to explain the good running time of SAT solvers in practice. With the hypothesis that real-world Satisfiability instances exhibit a hidden structure that makes them much easier to solve than worst-case instances, backdoor sets capture the phenomenon that it is often sufficient for a backtracking algorithm to set a small number of key variables to trivialize the formula.

Let C denote some class of CNF formulas. Typically, C is a class for which the satisfiability of formulas in C can be decided in polynomial time. A strong backdoor set to C of a CNF formula F is a set B of variables such that each instantiation of the variables in B reduces F to a formula in C (the instantiation removes all clauses that contain a true literal and removes all false literals from the remaining clauses). A weak backdoor set to C of a CNF formula F is a set B of variables such that at least one instantiation of the variables in B reduces F to a satisfiable formula in C. See the survey [GS12].

The aim of this project is to design a faster FPT algorithm for detecting small backdoor sets to a fixed base class. For a given combination of backdoor variant (weak/strong) and base class C, this algorithm will decide for a CNF formula F and an integer k, whether F has a (weak/strong) backdoor to C of size at most k, running in time f(k)poly(n), where f(k) is a (typically exponential) function depending only on k and poly(n) is a polynomial in n. Variants where the input formula is restricted to some class of formulas are possible as well. For example, it can be decided in time 3^k*poly(n) whether a 3CNF formula has a weak backdoor set to the empty formula. Can it be done in time 2.5^k*poly(n)?

[GS12] Serge Gaspers and Stefan Szeider. Backdoors to Satisfaction. In Hans L. Bodlaender, Rodney G. Downey, Fedor V. Fomin, Dániel Marx, editors, The Multivariate Algorithmic Revolution and Beyond: Essays Dedicated to Michael R. Fellows on the Occasion of His 60th Birthday, Springer LNCS 7370, pp. 287-317, 2012.
Past Student Reports
No Reports Available. Contact the supervisor for more information.

Check out all available reports in the CSE Thesis Report Library.

NOTE: only current CSE students can login to view and select reports to download.