From: Freed on
Given a set of statements known to be true, I need to deriver 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.
From: Freed on
On 25 Juni, 05:15, Tim Little <t...(a)little-possums.net> wrote:

> So if there exists any feasible algorithm at all, it has to depend
> upon special (as yet unstated) properties of the expected input.

You're right. For the input I'm expecting, the number of statements in
the form I'm after will be "small" in relation to the number of
combinations of literals, as the input will be mostly grouped around
subsets of literals.