scholarly journals Backdoor Sets for DLL Subsolvers

SAT 2005 ◽  
2007 ◽  
pp. 73-88
Author(s):  
Stefan Szeider
Keyword(s):  
Backdoor Sets

From Horn Strong Backdoor Sets to Ordered Strong Backdoor Sets

2007 ◽  
pp. 105-117
Author(s):  
Lionel Paris ◽  
Richard Ostrowski ◽  
Pierre Siegel ◽  
Lakhdar Saïs
Keyword(s):  
Backdoor Sets

Chapter 17. Fixed-Parameter Tractability

2021 ◽  
Author(s):  
Marko Samer ◽  
Stefan Szeider
Keyword(s):  
Polynomial Time ◽  
Parameterized Complexity ◽  
Complexity Analysis ◽  
Fixed Parameter Tractability ◽  
Graph Representations ◽  
Fine Grained ◽  
Input Size ◽  
Backdoor Sets ◽  
Fixed Parameter ◽  
Problem Instances

Parameterized complexity is a new theoretical framework that considers, in addition to the overall input size, the effects on computational complexity of a secondary measurement, the parameter. This two-dimensional viewpoint allows a fine-grained complexity analysis that takes structural properties of problem instances into account. The central notion is “fixed-parameter tractability” which refers to solvability in polynomial time for each fixed value of the parameter such that the order of the polynomial time bound is independent of the parameter. This chapter presents main concepts and recent results on the parameterized complexity of the satisfiability problem and it outlines fundamental algorithmic ideas that arise in this context. Among the parameters considered are the size of backdoor sets with respect to various tractable base classes and the treewidth of graph representations of satisfiability instances.

scholarly journals Backdoor Sets of Quantified Boolean Formulas

2008 ◽  
Vol 42 (1) ◽  
pp. 77-97 ◽  
Author(s):  
Marko Samer ◽  
Stefan Szeider
Keyword(s):  
Quantified Boolean Formulas ◽  
Backdoor Sets ◽  
Boolean Formulas

scholarly journals Backdoor Sets for DLL Subsolvers

2006 ◽  
Vol 35 (1-3) ◽  
pp. 73-88 ◽  
Author(s):  
Stefan Szeider
Keyword(s):  
Backdoor Sets

scholarly journals Backdoor DNFs

2021 ◽  
Author(s):  
Sebastian Ordyniak ◽  
Andre Schidler ◽  
Stefan Szeider
Keyword(s):  
Empirical Study ◽  
Fixed Parameter Tractability ◽  
Detection Problem ◽  
Partial Assignment ◽  
Backdoor Sets ◽  
Fixed Parameter ◽  
Cnf Formulas

We introduce backdoor DNFs, as a tool to measure the theoretical hardness of CNF formulas. Like backdoor sets and backdoor trees, backdoor DNFs are defined relative to a tractable class of CNF formulas. Each conjunctive term of a backdoor DNF defines a partial assignment that moves the input CNF formula into the base class. Backdoor DNFs are more expressive and potentially smaller than their predecessors backdoor sets and backdoor trees. We establish the fixed-parameter tractability of the backdoor DNF detection problem. Our results hold for the fundamental base classes Horn and 2CNF, and their combination. We complement our theoretical findings by an empirical study. Our experiments show that backdoor DNFs provide a significant improvement over their predecessors.

Sign in / Sign up

Export Citation Format

Share Document