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?

  • $\begingroup$ 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. $\endgroup$
    – D.W.
    Dec 14, 2023 at 4:05


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.