[Solved]: Algorithm for a special case of SAT/#SAT

Problem Detail: 

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)$$

Asked By : René G

Answered By : Fizz

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

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/39889

3.2K people like this

 Download Related Notes/Documents