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.