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.

P, such as boolean circuits or CNF, but not for all. As an example, ifPis 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