patternMinor
Algorithm for a special case of SAT/#SAT
Viewed 0 times
casesatalgorithmspecialfor
Problem
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)$$
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)$$
Solution
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]:
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:
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
Context
StackExchange Computer Science Q#39889, answer score: 2
Revisions (0)
No revisions yet.