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.
How many sets of vectors can be represented as the solutions of a Horn-SAT instance?
cc.complexity theory;co.combinatorics;sat
$\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 11 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.