5
$\begingroup$

Does anyone know of an algorithm that can solve the following special case of SAT in polynomial time? Are there any algorithms that can solve the counting (#SAT) version of it in polynomial time?

Special case: If clause $a$ and clause $b$ have one or more variables in common, that is, there exists some variable $x$ that is in both $a$ and $b$, at least one of the shared variables is positive in $a$ and negated in $b$ or vice-versa.

Example: $$(a \vee b \vee c) \wedge (\bar{a} \vee c \vee d)$$

Example of an instance that does not fit in the special case: $$(a \vee b \vee c) \wedge (a \vee c \vee d)$$

Improve this question
$\endgroup$
11
  • $\begingroup$ Have you tried checking whether resolution is effective on this special case? Have you tried any of the standard hard cases for resolution to see if they can be expressed in this special form? $\endgroup$
    – D.W. ♦
    Commented Feb 27, 2015 at 21:54
  • $\begingroup$ @D.W. I've looked all over and haven't found anything. The reason I ask here is because I think I found an algorithm for this and am therefore surprised it hasn't been solved already. $\endgroup$
    – Elliot Gorokhovsky
    Commented Feb 27, 2015 at 21:56
  • $\begingroup$ I don't mean to be annoying, but I notice that your comment doesn't actually answer either of my two questions... Seems like that would be one avenue you could investigate, if you want a direction that might enable you to answer your own question and help you understand the problem better. $\endgroup$
    – D.W. ♦
    Commented Feb 27, 2015 at 22:00
  • $\begingroup$ A good way to prove that would be to find an explicit counterexample: an example of a formula that is of your special type, and for which resolution will take exponential time. One way to look for such a counterexample might be to look at the standard hard cases for resolution (which are known to create an exponential slowdown) and see if they can be expressed in this special form. $\endgroup$
    – D.W. ♦
    Commented Feb 27, 2015 at 22:02
  • $\begingroup$ There may also be some useful information buried in this more general question: cs.stackexchange.com/questions/8952/… $\endgroup$
    – Luke Mathieson
    Commented Feb 28, 2015 at 1:16

1 Answer 1

Reset to default
2
+200
$\begingroup$

From Solving #SAT using vertex covers, published at SAT'06 by Naomi Nishimura, Prabhakar Ragde, and Stefan Szeider:

A cluster formula is a variable-disjoint union of so-called hitting formulas; any two clauses of a hitting formula clash in at least one literal. The known polynomial time algorithm for computing the number of models of a hitting formula can be extended in a straight-forward way to compute the number of models of a cluster formula.

Clash is later clarified/defined as:

We consider propositional formulas in conjunctive normal form (CNF), represented as sets of clauses. That is, a literal is a (propositional) variable $x$ or a negated variable $\overline{x}$; a clause is a finite set of literals not containing a complementary pair $x$ and $\overline{x}$; a formula is a finite set of clauses. For a literal $ℓ = \overline{x}$ we write $\overline{ℓ} = x$; for a clause $C$ we set $\overline{C} = \{ \overline{ℓ} : ℓ ∈ C \}$. We say that two clauses $C$, $D$ overlap if $C ∩ D \neq ∅$; we say that $C$ and $D$ clash if $C$ and $\overline{D}$ overlap. Note that two clauses can clash and overlap at the same time. [...] A formula is a hitting formula if any two of its clauses clash (see [17]). A cluster formula is the variable-disjoint union of hitting formulas [...]

Lemma 3. #SAT can be solved in polynomial time for cluster formulas.

So their cluster formula seems to be exactly what you have defined.

There's also a journal version that paper, it seems; the result is (not surprisingly) also mentioned in a 2011/2012 survey paper "Backdoors to satisfaction" on which Szeider is a co-author, and which was published in some festschrift My first instinct that this was a more suitable question on cstheory.SE was perhaps not wrong. :-)

Also the notion of hitting formulas is cited to [17]:

  • H. Kleine Buning and X. Zhao. Satisfiable formulas closed under replacement. In H. Kautz and B. Selman, editors, Proceedings for the Workshop on Theory and Applications of Satisfiability, volume 9 of Electronic Notes in Discrete Mathematics. Elsevier Science Publishers, North-Holland, 2001.

In another paper, the fact that

It is known that for hitting formulas the satisfiability problem can be solved efficiently [7].

is cited to an even older paper:

  • K. Iwama "CNF satisfiability test by counting and polynomial average time" SIAM J. Comput., 18 (1989), pp. 385–391
Improve this answer
$\endgroup$
6
  • 2
    $\begingroup$ The formula $(x \lor \lnot y) \land (y \lor \lnot z) \land (z \lor \lnot w)$ satisfies the requirements of the OP but is not a cluster formula. $\endgroup$
    – Yuval Filmus
    Commented Mar 4, 2015 at 4:05
  • $\begingroup$ @Yuval Filmus: Why not? The first two caluses are hitting (in $y$), the last two clauses are hitting (in $z$) and the first and the last clause have no variables in common. $\endgroup$
    – got trolled too much this week
    Commented Mar 4, 2015 at 4:08
  • $\begingroup$ The clauses $x\lor\lnot y$ and $z\lor\lnot w$ don't clash, but the formula cannot be written as a non-trivial conjunction of variable-disjoint formulas. $\endgroup$
    – Yuval Filmus
    Commented Mar 4, 2015 at 4:10
  • $\begingroup$ @Yuval Filmus: You're right, the definition for cluster given in Nishimura et al. doesn't cover this case (because $z$ from the last clause also appears in another clause, namely in the 2nd one). However, I wonder if it's still not contained in the result by Iwama, which is stated only in terms of the probabilities of the variables. I'll have to get back to this. $\endgroup$
    – got trolled too much this week
    Commented Mar 4, 2015 at 4:15
  • $\begingroup$ I'm still leaving this answer here (for a while) because it seems the OP has not logged in yet to read it an he'll probably want to cite it as related work anyway. $\endgroup$
    – got trolled too much this week
    Commented Mar 4, 2015 at 5:02

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.