# Is it possible to perform clause-pair minimization on a CNF instance in $o(n^2)$ time?

Let $$\varphi(X)$$ be a boolean formula in CNF over a set $$X$$ of boolean variables $$x_1,x_2,...,x_n$$. Let $$c_i$$ denote $$i^{th}$$ clause in $$\varphi(X)$$. $$x_j^0$$ denotes $$\overline{x_j}$$ and $$x_j^1$$ denotes $$x_j$$.

$$\varphi(X)$$ is considered clause-pair minimal if $$\forall i\forall j\neq i$$ the CNF $$c_i\land c_j$$ consisting of two clauses can't be replaced with an equivalent CNF that has fewer literals in it.

A clause-pair minimizer is a procedure that takes $$\varphi(X)$$ as an input and returns an equivalent clause-pair minimal formula.

The procedure consists of the following rules:

1. If there is a pair of clauses $$c_i\subseteq c_j$$ then remove $$c_j$$ from the formula.
2. Suppose there is a clause $$c_i$$ that contains a set of literals denoting variables $$X_i\subset X$$ and a clause $$c_j$$ that contains a set of literals denoting variables $$X_j\subset X_i$$. Also, suppose that all but one literals in $$X_j$$ appear in both clauses under the same sign. Then you can remove that literal from $$c_j$$. I.e. $$(x_1^{s_1}\lor x_2^{s_1}\lor...\lor x_{|c_{i-1}|}^{s_{i-1}}\lor x_{|c_i|}^{s_i})\land(x_1^{s_1}\lor x_2^{s_2}\lor...\lor x_{|c_{i-1}|}^{s_{i-1}}\lor\overline{x_{|c_i|}^{s_i}}\lor x_{|c_{i+1}|}^{s_{i+1}}\lor...\lor x_{|c_j|}^{s_j})$$ is equivalent to $$(x_1^{s_1}\lor x_2^{s_1}\lor...\lor x_{|c_{i-1}|}^{s_{i-1}}\lor x_{|c_i|}^{s_i})\land(x_1^{s_1}\lor x_2^{s_2}\lor...\lor x_{|c_{i-1}|}^{s_{i-1}}\lor x_{|c_{i+1}|}^{s_{i+1}}\lor...\lor x_{|c_j|}^{s_j})$$

Is it possible, for example, to do this in $$\mathcal O(n\log n)$$ time by using sorting?

• What does $\psi(X/X'/x_k)$ mean? What does "term width" mean? What does the free-standing sentence "$X' \subset X$" mean - how does it relate to the rest of the text? Can you define your notation in the question? $(\cdots \lor \cdots) \land c_j$ is not a clause, so you can't replace them with that.
– D.W.
Commented Dec 14, 2023 at 4:05