1
$\begingroup$

I have large cnf with thousands of variables, but with known compact backdoor set. I think this set can be used by CDCL solvers to choose assignment variables to simplify formula much faster, but I failed to find solver with such feature.

Kissat and cadical (top performers of SAT competitions) can't do that.

Is there any solvers which can use backdoor set for speed up?

Edit: as a backdoor set I mean subset of variables that make formula solvable in polynomial time after assignment. For example if cnf with $N$ variables have backdoor set with $M<N$ variables then it solvation can be accelerated from $O(const_1^N)$ to $O(const_2^M) + O((N-M)^{const_3})$

$\endgroup$
3
  • 1
    $\begingroup$ I encourage you to edit your post to provide a self-contained definition of what you mean by a "backdoor". (The paper isn't entirely clear to me, and it lists two separate definitions.) You might have to implement your own algorithm to use this, so I think it's better to ask how to make use of this. I'm not sure a question asking for an existing software package that happens to have this unusual feature will be on-topic here. $\endgroup$
    – D.W.
    Commented Feb 12 at 6:22
  • $\begingroup$ Please don't use "Edit: [more stuff added]". Instead, revise your question so it reads well for someone who encounters it for the first time. It's often a good idea to define any technical terms before first use. See cs.meta.stackexchange.com/q/657/755 $\endgroup$
    – D.W.
    Commented Feb 12 at 17:25
  • $\begingroup$ Also you definition isn't clear to me. I don't know what you mean by "subset that make .. after assignment". Do you mean that for every possible assignment, after (doing something with that assignment -- what? substituting into the formula?) the formula is solvable in polynomial time? Something else? I don't understand what you mean by "solvable in formula time". For that to be meaningful, you have to specify a particular algorithm for solving it in polynomial time. This issue is even mentioned in the paper. Please specify what algorithm you have in mind. $\endgroup$
    – D.W.
    Commented Feb 12 at 17:26

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.