# How are prime implicates of HORN-Formulas defined?

I'm confused about the definition of prime implicates in Horn formulas.

For example in the paper of Kira 2012 on page 109 it is stated:

Now in the paper of Boros 2010 on page 82 the following definition is used:

My goal is to decide whether a Horn formula is prime or not in polynomial time. For that I want to assume the definition used in Kira 2012.

How can I prove that the two definitions above for prime implications of Horn formulas are equivalent?

Edit: What I have so far is that if we assume Kiras definition and have for example a clause $$C=\neg x_1 \vee \neg x_2 \vee x_3$$ of formula $$F$$ and $$C$$ is prime then $$F\rightarrow C$$. If one neglects a literal in C we get $$C_1=\neg x_1 \vee \neg x_2$$ and obviously $$C_1 \rightarrow C$$. Therefore, since $$C$$ is prime then by Kiras definition no other proper sub-clause of $$C$$ is an implicant so $$F \nrightarrow C_1$$. Neglecting more literals in $$C_1$$ to get $$C_2$$ will give $$C_2\rightarrow C_1 \rightarrow C$$. Then by definition of $$C$$ it must be that $$F\nrightarrow C_2 \rightarrow C_1$$ and we get that all sub-clauses of $$C_1$$ are not prime if we check that $$C_1$$ is not prime. Therefore, to check if a Formula $$F$$ is prime we consider each clause $$C$$ and neglect all literals of $$C$$ once and check if the new clause is not prime. If One clause is prime it follows that F is not prime.

I think the equivalence for the other direction is similarly . Assume the definition of Boros. Then if we consider the clause $$C$$ and drop an arbitrary literal we get $$C_1$$ which is not an implicate if $$C$$ is prime so $$F\nrightarrow C_1$$. Again we have oviously $$C_1 \rightarrow C$$ and by dropping any more arbitrary literals in $$C_1$$ to get $$C_2$$ we note $$F\nrightarrow C_2 \rightarrow C_1$$(otherwise $$F\rightarrow C_2 \rightarrow C_1$$ which is wrong since $$C_1$$ is no implicate). Since by dropping literals we can produce arbitrary sub-clauses one can follow that also all proper sub-clauses of C cant be prime otherwise $$F\rightarrow C_2 \rightarrow C_1$$ which is a contradiction. And Kiras definition follows.

Is my reasoning correct?

• What have you tried? What progress have you made? Have you tried working through some examples?
– D.W.
Jul 18, 2020 at 6:13
• @D.W. Okay, I added my progress so far.
– Pepe
Jul 18, 2020 at 18:20

This equivalence is a somewhat folklore idea in papers about prime implicants. A small proof is presented in the "Definitions" section of this paper. The idea behind the equivalence is that, if $$C$$ is not a prime implicant for $$\varphi$$, then there is a proper subset $$C'$$ of $$C$$ (identifying clauses with the set of literals they force) such that $$C'$$ is an implicant of $$\varphi$$. But if this is the case, then you can fill $$C'$$ with the literals in $$C \setminus C'$$ until it has size $$|C| - 1$$, and thus, you obtain an implicant that is $$C$$ minus exactly one literal you "dropped". The other direction of the equivalence is trivial: if no proper subset of $$C$$ is an implicant, then dropping any literal of $$C$$ gives you something that is not an implicant.