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: enter image description here

Now in the paper of Boros 2010 on page 82 the following definition is used: enter image description here

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?

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

1 Answer 1


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.

I don't see the relation with Horn formulas, as the equivalence is about definitions for prime implicants of any formula.

  • $\begingroup$ Thank you, this cleared up my understanding. $\endgroup$
    – Pepe
    Jul 19, 2020 at 0:57

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.