general.hpp File Reference

Plans on backdoor-related algorithms. More...

Go to the source code of this file.

Detailed Description

Plans on backdoor-related algorithms.

Blind search for backdoors of size k
  • strong/weak/deletion_backdoor_search(F,k,C), where
    1. F is a clause-set,
    2. k a natural number,
    3. and C a unary predicate for the base class (thus C(F) is true iff F belongs to the "tractable" class),
    just runs through all subsets V of size at most k (starting from below) of the variable-set, and returns V in case
    1. "strong": for all partial assignments phi with domain V, vp * F is in C;
    2. "weak": there exists a partial assignment phi with domain V such that phi * F is satisfiable and belongs to C;
    3. "deletion": V * F is in C.
    Otherwise false is returned.
  • I (OK) expect that in general usage of r_k(U,S) (see Satisfiability/Lisp/Reductions/plans/GeneralisedUCP.hpp; especially topic "Use oracles") is more useful, since it strengthens strong, weak and deletion backdoors by inference (if any of those backdoors of size k exists, then r_k with U = C cap USAT and S = C cap SAT reduces F to {} or {{}}).
2-CNF backdoors
Horn backdoors
Backdoors w.r.t. clause-sets of bounded deficiency
  • The parameterised translation of the transversal problem to the problem of detecting a backdoor w.r.t. CLS_{delta^* <= r} (see [Szeider, Matched formulas and backdoor sets, SAT 2007]) should be implemented.
  • Somewhere we also need to implement the various algorithms for clause-sets with bounded maximal deficiency.

Definition in file general.hpp.