How many sets of vectors can be represented as the solutions of a Horn-SAT instance?

Question

Let the solution space of a SAT instance be the set of Boolean vectors of satisfying assignments of $\{0,1\}$ to the variables (that result in the formula evaluating to TRUE). In other words, a solution space represents all the solutions of an instance. There are at most $2^n$ solutions, so $n$-variable SAT (denoted here by SAT$_n$) can represent at most $2^{2^n}$ different solution spaces. Moreover, it is easy to see that this number can actually be reached, by considering instances where every clause contains all $n$ variables.

We know that Horn-SAT is less expressive than SAT, for instance there is no Horn-SAT$_2$ representation of the solution space of $a \lor b$, which contains the 3 vectors $01, 10, 11$. Hence Horn-SAT$_n$ must be able to represent fewer than $2^{2^n}$ solution spaces.

What is the number of solution spaces of a Horn-SAT$_n$ instance?

For completeness, recall that a literal is either a variable or its negation, and that $n$-variable SAT consists of formulas built from at most $n$ variables (we can fix the set of variable names, e.g. $\{1,2,\dots,n\}$), in conjunctive normal form (a conjunction of disjunctions), where each disjunction of literals is known as a clause. Horn-SAT$_n$ is the fragment of $n$-variable SAT where each clause in an input formula contains at most one non-negated variable.

An equivalent counting formulation of the question is: how many different values can #Horn-SAT$_n$ have? However, note that I am not interested here in the complexity of #Horn-SAT, just its range of values for each number of variables.

---

If one tries to work syntactically, then one faces the same challenge as for SAT. Suppose one tries to count the number of different SAT instances syntactically. There are $2^{3^n}$ different ways to write down a SAT instance with $n$ variables and no repeated clauses (if the variable order is fixed and no variable may appear more than once in a clause), so one has to find the equivalence classes of syntactically different instances that lead to the same solution space, to retrieve the $2^{2^n}$ number. One then needs to similarly take the quotient of the set of different Horn-SAT instances with $n$ variables to obtain the correct value of the number of different solution spaces. It is not clear to me how to take quotients for SAT, let alone how to do so for Horn-SAT.

Answer 1

$\def\pw{\mathcal P}$ It is an easy exercise to show that if we identify Boolean assignments to $n$ variables with subsets of $[n]=\{0,\dots,n-1\}$, then the solution sets of Horn CNFs are exactly the families $S\subseteq\pw([n])$ that are closed under nonempty intersections.

The picture is a little nicer for conjunctions of clauses each of which contains exactly one positive literal. Their solution sets are families closed under arbitrary intersections (where in particular the empty intersection is the full set), also known as closure systems or Moore families. These are in 1–1 correspondence with closure operators (functions $C\colon\pw([n])\to\pw([n])$ satisfying $X\subseteq C(Y)\iff C(X)\subseteq C(Y)$), consequence relations (relations ${\vdash}\subseteq\pw([n])\times[n]$ satisfying a handful of natural conditions), and I guess there are more similar combinatorial characterizations (https://oeis.org/A102896 or https://oeis.org/A102897 mention semilattices).

These two numbers only differ by a factor of two (given a closure system $S$, we may either retain $[n]\in S$ or throw it out without affecting anything else).

Alekseev proved that the number $\alpha(n)$ of closure systems on an $n$-element set satisfies

$$2^{\binom{n}{\lfloor n/2\rfloor}}\le\alpha(n)\le2^{\binom{n}{\lfloor n/2\rfloor}(1+o(1))}.$$

See http://www.renyi.hu/~ohkatona/paper_72.pdf for related information.

Answer 2

I can share some details of experiments that I'm running on Boolean strings.

The number of 2-bit strings are too few -- not much to observe here.

The number of 3-bit strings is $2^3 = 8$, hence the number of possible subsets is $2^8 = 256$. It turns out that 122 of these are Horn sets and 134 are not.

The number of 4-bit strings is $2^4 = 16$, hence the number of possible subsets is $2^{16} = 65536$. Out of these, only 4960 are Horn sets and 60576 are not Horn.

For $n = 5$, the number of possible subsets is $65536^2$, which is more than 4 billion. I only have access to 3 machines on campus, so I have divided the problem into several cases and running them case by case (even then, it's going take 2-3 weeks to run). Looking at the computation so far, only about 5% of the sets seem to be Horn.

For $n \ge 6$, I don't have the computing power! (Or it'll take months)

Am doing the testing using GAWK. $~$Happy to share the code files. (How to post files here?)

Other comments? questions?

Answer 3

(I was going to add a quick comment, but I'm not being allowed to.)

If you take into account equi-satisfiability, then you can get lots more Horn formulas. For example, considering $\phi \equiv (p \lor q)$, there is a reduction from $\phi$ to a Horn formula. See my answer under Translating SAT to HornSAT.

If you try using the above technique to reduce an arbitrary 3-SAT formula to a Horn formula, you cannot do it in poly time -- since two 3-clauses resolve to a 4-clause, two 4-clauses resolve to a 6-clause, and so on... the result is an exponential number of clauses.. but I digress.. I'm going off-topic, so let me stop here.