Plans on backdoorrelated algorithms.
More...
Go to the source code of this file.
Detailed Description
Plans on backdoorrelated algorithms.
 Todo:
 Blind search for backdoors of size k

strong/weak/deletion_backdoor_search(F,k,C), where

F is a clauseset,

k a natural number,

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 variableset, and returns V in case

"strong": for all partial assignments phi with domain V, vp * F is in C;

"weak": there exists a partial assignment phi with domain V such that phi * F is satisfiable and belongs to C;

"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 {{}}).
 Todo:
 2CNF backdoors
 Todo:
 Horn backdoors
 Todo:
 Backdoors w.r.t. clausesets 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 clausesets with bounded maximal deficiency.
Definition in file general.hpp.