7
$\begingroup$

A Horn clause is a disjunctive clause of literals containing at most one unnegated literal. Examples are $$ \neg p \lor \neg r \lor \neg q,\\ \neg s \lor q,\\ \neg s \lor \neg q\lor r,\\ s,\\ \neg r \lor t,\\ \neg q \lor \neg t\lor p. $$ Determining whether or not a set of Horn clauses is simultaneously satisfiable takes polynomial time: this is the problem known as HORNSAT. The algorithm does the following:

  • If there is a clause containing only a single positive literal, set the letter of that literal to true; then remove the negation of that literal from all clauses containing it. Repeat until no such clauses exist.
  • Then, if there is an empty clause, the set is not satisfiable.
  • If there is no empty clause, the set is satisfiable, with satisfying assignment given by setting all unset letters to false.

Following the algorithm, you can quickly see that the above set of clauses is not simultaneously satisfiable, since the last five clauses force all used letters to be true, while the first clause asks at least one to be false.

Now, the problem #HORNSAT asks the following: given a set of Horn clauses, how many simultaneously satisfying assignments are there? One might expect the problem to be easier than #SAT, since HORNSAT is so much easier than SAT; on the other hand, it "feels" NP-hard.

Improve this question
$\endgroup$
0

1 Answer 1

Reset to default
7
$\begingroup$

Even if decision is easy, the counting problem #HORNSAT is #P-complete [1], the counting analog of NP-completeness problem. Thus it is very unlikely it has a polynomial time algorithm (for example, if $P \neq NP$ then #HORNSAT has no ptime algorithm).

See [1] for a dichotomy characterizing the clause restrictions leading to tractable instances of #SAT. More precisely, it is shown that the only restriction of clauses that gives tractable instances for #SAT are the clauses of the form $x_1 \oplus x_2 \oplus ...\oplus x_n = 0$ where $\oplus$ is the sum modulo $2$. The other restrictions (#2-SAT, #HORNSAT, ...) are all #P-complete.

[1] Nadia Creignou, Miki Hermann: Complexity of Generalized Satisfiability Counting Problems. Inf. Comput. 125(1): 1-12 (1996), http://www.sciencedirect.com/science/article/pii/S0890540196900164?via%3Dihub

Improve this answer
$\endgroup$
2
  • $\begingroup$ Which lemma or theorem is it (clauses using $\oplus_i x_i\equiv0\implies\#SAT\in P$? Is it in $P$ or in $\oplus L$? $\endgroup$
    – Turbo
    May 11, 2021 at 3:50
  • $\begingroup$ Theorem 4.1 of [1]. But basically, it boils down to solving linear equations on $\mathbb{F}_2$. I am not sure about lower complexity. $\endgroup$
    – holf
    May 11, 2021 at 5:41

Your Answer

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

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