<p>I can share some details of experiments that I'm running on Boolean strings.</p>

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

<p>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 <strong>not</strong>.</p>

<p>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 <strong>not</strong> Horn.</p>

<p>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.</p>

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

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

<p>Other comments? questions?</p>

CC BY-SA 3.0
2015-04-14T21:46:02.243Z
https://oeis.org/A102897 has values up to $n=7$.
Emil Jeřábek
CC BY-SA 3.0
2015-03-16T06:30:15.603Z
2015-03-16T06:30:15.603Z
Martin Seymour
<p>(I was going to add a quick comment, but I'm not being allowed to.)</p>

<p>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 <a href="https://cstheory.stackexchange.com/questions/200/translating-sat-to-hornsat">Translating SAT to HornSAT</a>.</p>

<p>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.</p>

CC BY-SA 3.0
2014-11-24T21:05:03.920Z
2014-11-24T21:05:03.920Z
2017-04-13T12:32:28.167Z
Martin Seymour
<p>$\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.</p>

<p>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 <em>arbitrary</em> 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 <a href="http://en.wikipedia.org/wiki/Closure_operator"><em>closure operators</em></a> (functions $C\colon\pw([n])\to\pw([n])$ satisfying $X\subseteq C(Y)\iff C(X)\subseteq C(Y)$), <em>consequence relations</em> (relations ${\vdash}\subseteq\pw([n])\times[n]$ satisfying a handful of natural conditions), and I guess there are more similar combinatorial characterizations (<a href="https://oeis.org/A102896">https://oeis.org/A102896</a> or <a href="https://oeis.org/A102897">https://oeis.org/A102897</a> mention semilattices).</p>

<p>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).</p>

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

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

<p>See <a href="http://www.renyi.hu/~ohkatona/paper_72.pdf">http://www.renyi.hu/~ohkatona/paper_72.pdf</a> for related information.</p>

CC BY-SA 3.0
2014-11-24T16:39:47.433Z
Perfect, thanks!  In particular, this means that the number of different sets of Boolean vectors that can be represented by an $n$-variable Horn-SAT instance is at least something like $2^{2^{n-1-(1/2)\log n}}$.  So Horn-SAT is actually quite expressive, in some sense.
András Salamon
CC BY-SA 3.0
2014-11-24T16:32:52.023Z
2014-11-24T16:32:52.023Z
Emil Jeřábek
<p>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.</p>

<p>We know that <a href="https://cstheory.stackexchange.com/q/200/109">Horn-SAT is less expressive than SAT</a>, 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.</p>

<blockquote>
  <p>What is the number of solution spaces of a Horn-SAT$_n$ instance?</p>
</blockquote>

<p>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.</p>

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

<hr>

<p>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.</p>

CC BY-SA 3.0
2014-11-24T11:39:13.370Z
Exactly the same as the number of subsets of $\mathcal P(\{1,\dots,n\})$ closed under nonempty intersections. Or twice the number of closure operators on an $n$-element base set.
Emil Jeřábek
CC BY-SA 3.0
2014-11-24T12:00:36.343Z
@Emil: are asymptotics or bounds known for these expressions?
András Salamon
CC BY-SA 3.0
2014-11-24T12:35:34.847Z
Certainly. I have to rush, but you can start at https://oeis.org/A102897.
Emil Jeřábek
<cc.complexity-theory><co.combinatorics><sat>
How many sets of vectors can be represented as the solutions of a Horn-SAT instance?
András Salamon
# How many sets of vectors can be represented as the solutions of a Horn-SAT instance?

(Asked by: username_0 on 2014-11-24)

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](https://cstheory.stackexchange.com/q/200/109), 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.

**Tags:** cc.complexity-theory, co.combinatorics, sat
> **Comments:**
> **username_1**: Exactly the same as the number of subsets of $\mathcal P(\{1,\dots,n\})$ closed under nonempty intersections. Or twice the number of closure operators on an $n$-element base set.  
> **username_0**: @Emil: are asymptotics or bounds known for these expressions?  
> **username_1**: Certainly. I have to rush, but you can start at https://oeis.org/A102897.  

---

## 3 answers

### Answer by username_1 on 2014-11-24. Score: 8 | Accepted answer

$\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*](http://en.wikipedia.org/wiki/Closure_operator) (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.

> **Comments:**
> **username_0**: Perfect, thanks!  In particular, this means that the number of different sets of Boolean vectors that can be represented by an $n$-variable Horn-SAT instance is at least something like $2^{2^{n-1-(1/2)\log n}}$.  So Horn-SAT is actually quite expressive, in some sense.  

---

### Answer by username_2 on 2015-03-16. Score: 1

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?

> **Comments:**
> **username_1**: https://oeis.org/A102897 has values up to $n=7$.  

---

### Answer by username_2 on 2014-11-24. Score: -1

(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](https://cstheory.stackexchange.com/questions/200/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.


---

