# Deriving the complete set of “non-redundant” true statements in disjunctive form in propositional logic

Given a finite set of statements known to be true, I need to derive all the "non-redundant" statements in disjunctive form using only literals that can be derived from this set of statements, i e all statements on the form (a ∨ b ∨ c ∨ ...) where a, b ... are literals. By non-redundant I mean that I do not wish to include a statement if one of the literals could be removed and it would still always be true (given the initial set of statements).

Another way of looking at this would be that I want a statements in conjunctive normal form, but that includes all non-redundant statements as the inner groups, not just the minimal set equivalent to the initial set of statements.

A naive algorithm for this would be to test all assignments of truth values to literals, keeping only the ones that 1) are true given the initial set of statements 2) are non-redundant (tested by assigning false to each of the literals in the statement, checking if it still remains slow). However, the number of literals I'll be working with will be so large that this naive approach is not feasible.

Edit:

What I'm looking for is an algorithm that will efficiently produce the set of statements as described above, such as the strategies that can be used to convert to a conjunctive normal form.

-
You need to be more specific about what type of answer you are looking for, since it looks like you have already presented one answer in your question. Also, I'm sure you intend for the initial set to be finite. –  Carl Mummert Jun 24 '10 at 12:46
Thank you, edited the question to clarify. –  SoftMemes Jun 24 '10 at 20:33
The problem you are asking about is coNP-hard. Start with any propositional formula P and you take a new variable A. Look at the formula (P OR A), which is clearly satisfiable. The formula "A" is of the form you are interested in, since it is a disjunction of exactly one literal. And "A" is a consequence of (P OR A) if and only if P is unsatisfiable. –  Carl Mummert Jun 24 '10 at 23:17
This problem should also be tagged as pertaining to complexity. –  Iddo Tzameret Jul 1 '10 at 10:41
Carl, please note that your argument works for many reasonable representations of P, such as boolean circuits or CNF, but not for all. As an example, if P is represented as a (reduced ordered) BDD, then checking satisfiability is a constant time operation. Using this representation may be seen as "cheating" because there are known explicit functions for which the BDD representation is exponential in the number of variables. However, I'd say it is an interesting variant of the problem, that may well be useful in practice. –  rgrig Jul 30 '10 at 11:05

I believe your problem is: Given a boolean function $\phi$, find the set of its prime clauses (aka prime implicates). This is equivalent to finding all the prime implicants of $\lnot\phi$.

You will find in the paper A Knowledge Compilation Map many references to papers that discuss variants of this problem. For example, the paper Algorithms for Selective Enumeration of Prime Implicants focuses on the case when $\phi$ is given in DNF or CNF (and also has many good references). Another interesting paper is Implicit and Incremental Computation of Primes and Essential Primes of Boolean Functions that represents the resulting set as a BDD, which may be much smaller than a simple list. (Though a ZBDD, invented later, might work even better.)

In short, there are lots of algorithms, none works fast all the time, but some might be fast enough in practice.

(Note: Knuth uses the term conjunctive prime form for the conjunction of prime clauses. This appears in fascicle 0 of volume 4 of TAoCP from 2005-2009. But the name didn't yet caught on.)

-
I could hardly ask for a more complete answer, thank you! –  SoftMemes Jul 31 '10 at 21:41

I don't think you're asking what you want to ask.

Given some set of formulae {$p_i$}, what can we say about the "literals that can be derived from this set of statements"?

Conjoin the $p_i$ and put the result in minimal disjunctive normal form (using a standard technique like the Quine-McCluskey algorithm). The will produce some $r = r_1 \vee \ldots \vee r_n$, where each $r_i$ is a conjunction of literals.

1. Suppose the set {$p_i$} is consistent. Then a literal $l$ will be derivable from the {$p_i$} just in case $l$ appears in each disjunct $r_i$. Let the set of such literals be {$l_i$}.

2. Suppose {$p_i$} is inconsistent. Then in each disjunct $r_i$ you will find some literal and its negation. In this case every literal will be derivable from the {$p_i$}. Let {$l_i$} then be the set of all literals.

What can we now say about disjunctions of the {$l_i$} that are non-redundant in your sense? Each $l_i$ will trivially belong to that set. But $l_i \vee q$ will be redundant for any $q$. So the set you want is just {$l_i$}.

Perhaps I've misunderstood your question, but it any case it sounds like a circuit-minimization problem, and you're not going to find a solution that's better than exponential in the number of atomic variables unless you add some constraints to the problem. You should look at the aforementioned Quine-McCluskey algorithm, as well as the "Espresso" algorithm.

-
I do not quite follow your reasoning here. True, each literal appearing in each disjunct r_i will be derivable from {p_i} and follow my form, but they will not form the complete set of disjunctions of literals that do so. For example, A or B is in a minimal DNF, and the statement A or B itself would be in the set of derivable statements in the form I've described. –  SoftMemes Jun 25 '10 at 10:35
Ah. I thought you wanted both $A$ and $B$ to be individually derivable, not just the disjunction $A \vee B$. –  user7071 Jun 25 '10 at 15:19

If the phrase "Given a finite set of statements known to be true" means that the set is tautological (i.e., every propositional assignment to all the variables satisfies all the propositions in the set of initial statements), then the only non-redundant statements written as disjunctions of literals which are derivable (that is, implied semantically) from the initial set of statements are: $(x \vee \neg x)$, for all variables $x$.

If you don't specify a condition on the initial finite set of statements, then Carl Mummert's comment above shows the problem to be coNP-complete, and thus believed to have no efficient algorithm.

-

Just to complement the answer of rgrig. There is a tool that computes all prime implicates zres. Unfortunately, I encountered buggy behavior with this tool. I have some naive implementation, which I could make available, if there is not anything else.

-