<p>For any <span class="math-container">$0&lt;k\le n$</span>, the maximal size of such a set of clauses is <span class="math-container">$$\binom nk2^{k-1},$$</span>
i.e., <span class="math-container">$1/2$</span> of the number of all <span class="math-container">$k$</span>-clauses. (I’m assuming a clause cannot contain any variable both positively and negatively.) (For <span class="math-container">$k=0$</span>, the answer is clearly <span class="math-container">$1$</span>.)</p>
<p>The problem can be restated as the maximal size of an independent set in a graph whose vertices are <span class="math-container">$k$</span>-clauses in <span class="math-container">$n$</span> variables, and with edges <span class="math-container">$\{C_0,C_1\}$</span> such that <span class="math-container">$C_0$</span> and <span class="math-container">$C_1$</span> resolve to a <span class="math-container">$(k-1)$</span>-clause. This is equivalent to the condition that <span class="math-container">$C_0$</span> and <span class="math-container">$C_1$</span> differ just by negating one literal (which implies, in particular, that they have the same set of variables): the resolvent of <span class="math-container">$C_0$</span> and <span class="math-container">$C_1$</span> includes <span class="math-container">$k-1$</span> literals from each clause, hence it has only <span class="math-container">$k-1$</span> literals in total iff the contributions from the two clauses are identical.</p>
<p>This graph has <span class="math-container">$\binom nk$</span> connected components, each of which consists of clauses that use a particular set of <span class="math-container">$k$</span> variables; each component is in turn isomorphic to the Hamming graph with vertex set <span class="math-container">$\{0,1\}^k$</span> and edges connecting vertices of Hamming distance <span class="math-container">$1$</span> (the vectors in <span class="math-container">$\{0,1\}^k$</span> indicate which variables are negated). The independence number of the Hamming graph is well known to be <span class="math-container">$2^{k-1}$</span> (for <span class="math-container">$k&gt;0$</span>): on the one hand, the set of vectors with even Hamming weight forms an independent set of size <span class="math-container">$2^{k-1}$</span>; on the other hand, the vectors in any independent set must differ in their first <span class="math-container">$k-1$</span> coordinates. Of course, the independence number of the whole graph is the sum of independence numbers of its components, thus <span class="math-container">$\binom nk2^{k-1}$</span>.</p>
<p>This argument gives an explicit set of <span class="math-container">$\binom nk2^{k-1}$</span> clauses as a witness: the set of all clauses that have an even number of positive literals (for <span class="math-container">$n=k$</span>, this is the CNF expansion of <span class="math-container">$x_1\oplus\dots\oplus x_n$</span>, as rus9384 puts in in the comments).</p>
<p>[NB: If we <em>do</em> allow a variable to occur both positively and negatively in a clause, the answer changes to <span class="math-container">$\frac12\binom{2n}k$</span> (= <span class="math-container">$1/2$</span> of all <span class="math-container">$k$</span>-clauses) for <span class="math-container">$k$</span> odd, and <span class="math-container">$\frac12\bigl(\binom{2n}k+\binom n{k/2}\bigr)$</span> for <span class="math-container">$k$</span> even, by a similar argument. But given the motivation of the question, I doubt this is the intended interpretation.]</p>

CC BY-SA 4.0
2024-01-15T19:56:09.517Z
2024-01-16T07:48:11.793Z
2024-01-16T07:48:11.793Z
Emil Jeřábek
<p>Let <span class="math-container">$n$</span> be the number of variables and <span class="math-container">$k$</span> the size of the clauses. What is the maximum number of k-clauses such that no two clauses can be resolved to a smaller (less than <span class="math-container">$k$</span>) clause.</p>
<p>I will accept an answer for when <span class="math-container">$n=k$</span>.</p>
<p>I think these are correct:</p>
<p>N | K | Max</p>
<p>n | 1 | n</p>
<p><span class="math-container">$(a)$</span></p>
<p>2 | 2 | 2</p>
<p><span class="math-container">$(a \lor b)(\bar a \lor \bar b)$</span></p>
<p>3 | 3 | 2</p>
<p><span class="math-container">$(a \lor b \lor c)(\bar a \lor \bar b \lor \bar c)$</span></p>
<p>4 | 4 | 8</p>
<p><span class="math-container">$(a \lor b \lor c \lor d)(\bar a \lor \bar b \lor c \lor d)(\bar a \lor b \lor \bar c \lor d)(\bar a \lor b \lor c \lor \bar d)(a \lor \bar b \lor \bar c \lor d)(a \lor \bar b \lor c \lor \bar d)(a \lor b \lor \bar c \lor \bar d)(\bar a \lor \bar b \lor \bar c \lor \bar d)$</span></p>
<p>I didn't find any promising sequences on <a href="https://oeis.org/" rel="nofollow noreferrer">Sloanes Online Encyclopedia of Integer Sequences</a>.</p>
<p>This is related to <a href="https://cstheory.stackexchange.com/questions/53602/how-often-can-a-clause-cause-a-conflict">How often can a clause cause a conflict</a></p>
<p>Rus9384 pointed out I made mistake for n=k=3:</p>
<p><span class="math-container">$(\bar a \lor \bar b \lor \bar c)(\bar a \lor b \lor c)(a \lor \bar b \lor c)(a \lor b \lor \bar c)$</span></p>

CC BY-SA 4.0
2024-01-15T20:11:44.413Z
This is not correct for $3$: you need to encode $a\oplus b\oplus c$ just as how you did with $2$ and $4$.
rus9384
CC BY-SA 4.0
2024-01-15T22:43:08.153Z
@rus9384 Do you mean use XOR? I am assuming CNF. All I can use is OR.
Russell Easterly
CC BY-SA 4.0
2024-01-16T00:04:00.050Z
I am saying that XOR translates to an exponentially long CNF. XOR over $n$ variables requires $2^{n-1}$ clauses. For 3 it is 4 clauses.
rus9384
<sat><resolution>
Max number of k-clauses such that no two clauses can be resolved?
Russell Easterly
# Max number of k-clauses such that no two clauses can be resolved?

(Asked by: username_0 on 2024-01-15)

Let $n$ be the number of variables and $k$ the size of the clauses. What is the maximum number of k-clauses such that no two clauses can be resolved to a smaller (less than $k$) clause.

I will accept an answer for when $n=k$.

I think these are correct:

N | K | Max

n | 1 | n

$(a)$

2 | 2 | 2

$(a \lor b)(\bar a \lor \bar b)$

3 | 3 | 2

$(a \lor b \lor c)(\bar a \lor \bar b \lor \bar c)$

4 | 4 | 8

$(a \lor b \lor c \lor d)(\bar a \lor \bar b \lor c \lor d)(\bar a \lor b \lor \bar c \lor d)(\bar a \lor b \lor c \lor \bar d)(a \lor \bar b \lor \bar c \lor d)(a \lor \bar b \lor c \lor \bar d)(a \lor b \lor \bar c \lor \bar d)(\bar a \lor \bar b \lor \bar c \lor \bar d)$

I didn't find any promising sequences on [Sloanes Online Encyclopedia of Integer Sequences](https://oeis.org/).

This is related to [How often can a clause cause a conflict](https://cstheory.stackexchange.com/questions/53602/how-often-can-a-clause-cause-a-conflict)

Rus9384 pointed out I made mistake for n=k=3:

$(\bar a \lor \bar b \lor \bar c)(\bar a \lor b \lor c)(a \lor \bar b \lor c)(a \lor b \lor \bar c)$

**Tags:** sat, resolution
> **Comments:**
> **username_1**: This is not correct for $3$: you need to encode $a\oplus b\oplus c$ just as how you did with $2$ and $4$.  
> **username_0**: @rus9384 Do you mean use XOR? I am assuming CNF. All I can use is OR.  
> **username_1**: I am saying that XOR translates to an exponentially long CNF. XOR over $n$ variables requires $2^{n-1}$ clauses. For 3 it is 4 clauses.  

---

## 1 answers

### Answer by username_2 on 2024-01-15. Score: 1 | Accepted answer

For any $0, the maximal size of such a set of clauses is $$\binom nk2^{k-1},$$
i.e., $1/2$ of the number of all $k$-clauses. (I’m assuming a clause cannot contain any variable both positively and negatively.) (For $k=0$, the answer is clearly $1$.)

The problem can be restated as the maximal size of an independent set in a graph whose vertices are $k$-clauses in $n$ variables, and with edges $\{C\_0,C\_1\}$ such that $C\_0$ and $C\_1$ resolve to a $(k-1)$-clause. This is equivalent to the condition that $C\_0$ and $C\_1$ differ just by negating one literal (which implies, in particular, that they have the same set of variables): the resolvent of $C\_0$ and $C\_1$ includes $k-1$ literals from each clause, hence it has only $k-1$ literals in total iff the contributions from the two clauses are identical.

This graph has $\binom nk$ connected components, each of which consists of clauses that use a particular set of $k$ variables; each component is in turn isomorphic to the Hamming graph with vertex set $\{0,1\}^k$ and edges connecting vertices of Hamming distance $1$ (the vectors in $\{0,1\}^k$ indicate which variables are negated). The independence number of the Hamming graph is well known to be $2^{k-1}$ (for $k>0$): on the one hand, the set of vectors with even Hamming weight forms an independent set of size $2^{k-1}$; on the other hand, the vectors in any independent set must differ in their first $k-1$ coordinates. Of course, the independence number of the whole graph is the sum of independence numbers of its components, thus $\binom nk2^{k-1}$.

This argument gives an explicit set of $\binom nk2^{k-1}$ clauses as a witness: the set of all clauses that have an even number of positive literals (for $n=k$, this is the CNF expansion of $x\_1\oplus\dots\oplus x\_n$, as rus9384 puts in in the comments).

[NB: If we *do* allow a variable to occur both positively and negatively in a clause, the answer changes to $\frac12\binom{2n}k$ (= $1/2$ of all $k$-clauses) for $k$ odd, and $\frac12\bigl(\binom{2n}k+\binom n{k/2}\bigr)$ for $k$ even, by a similar argument. But given the motivation of the question, I doubt this is the intended interpretation.]


---

