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)$$
Algorithm for a special case of SAT/#SAT
algorithms;complexity theory;satisfiability;polynomial time;counting
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 Theoryand Applications of Satisfiability, volume 9 of Electronic Notes in DiscreteMathematics. Elsevier Science Publishers, North-Holland, 2001.In another paper, the fact thatIt 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. 385391