Deriving the complete set of "non-redundant" true statements in disjunctive form in propositional logic - MathOverflow

Deriving the complete set of "non-redundant" true statements in disjunctive form in propositional logic

2010-06-24T07:00:55Z

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.

Answer by unknown (google) for Deriving the complete set of "non-redundant" true statements in disjunctive form in propositional logic

2010-06-24T21:27:14Z

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.

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$}.
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.

Answer by Iddo Tzameret for Deriving the complete set of "non-redundant" true statements in disjunctive form in propositional logic

2010-07-01T10:33:45Z

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.

Answer by rgrig for Deriving the complete set of "non-redundant" true statements in disjunctive form in propositional logic

2010-07-29T19:34:02Z

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.)

Answer by mikolas for Deriving the complete set of "non-redundant" true statements in disjunctive form in propositional logic

2010-07-29T20:40:34Z

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.