Re: Generalized Quine-McCluskey

First let me thank you for the reply.

herbzet wrote:
If we wish to have a model with d elements (2^m < d < 2^(m + 1))
we will have to add some non-tautologous axioms to specifically
exclude some of the 2^(m + 1) elements. We may put these axioms
in a normal form so as to make clear what elements we are
excluding, e.g.

~(a ^ b ^ c) ^ ~(a ^ ~b ^ ~c) ^ ~(~a ^ b ^ ~c) ^ etc.

I'm guessing that you are looking to reduce such contingent
formulae in an efficient manner.

Well, computing all prime implicants produces a lot of prime implicants in general, so one may argue about calling it a "reduction". However, for user-given exclusion formulae (except some well-known counterexamples like parity), we expect a small number of prime implicants. In terms of your description, we are trying to find a data structure that allows a fast query, whether an arbitrary conjunction implies the formula describing the excluded elements. One possibility is to take the disjunction of all prime implicants as this data structure.


A formula is
a boolean combination of atomic propositions. An implicant of a formula
f is a conjunction of atomic propositions that implies f. A prime
implicant g of f is an implicant of f so that there is no other
implicant f' of f so that g implies f'.

Assuming that the prime implicants of a formula do not vary
in different models of 2^d elements:

The first problem is that there are equivalent formulae, e.g.

a = (a ^ a) = (a ^ a ^ a) = (a ^ (b v ~b)) = etc, etc.

All of these imply each other, and so are not prime by your
definition.

If we disallow repetitions of atomic formula, but allow
negation, we have as prime implicants of, say, a --

a, (a ^ b), (a ^ ~b), (a ^ c), (a ^ ~c), (a ^ d), (a ^ ~d), etc.

but not

(a ^ b ^ c), (a ^ b ^ ~c), (a ^ ~b ^ c), (a ^ ~b ^ ~c), (a ^ b ^ c ^ d),

etc., each of which implies one or more of the previous group, as
well as a.


I have to be more precise here to say when formulas are equivalent. Negation is forbidden, since a complement of a subset of {1,...,d} is another subset. In a conjunction, each on n variables x1,...,xn occurs exactly once (since "no occurrence of xi" is equivalent to "xi in {1,...,d}"). Let's see a conjunction as a set of atomic propositions, so two conjunctions which differ only by the order of atomic propositions are equal.

This means that a^a is forbidden (repetition), and a^~b is also forbidden, since it contains a negation. a^(bvc) contains a disjunction, so it's not an implicant at all.

Now, there is only one prime implicant of an atomic proposition "xi in A", namely, (xj in {1,...d} for all j and "xi in A"). So an atomic proposition "a" cannot have "avb" as a prime implicant.


When we are dealing with conjunctions of reduced formulae (so
that there are no equivalent formulae) then implication is
the same as inclusion, i.e. A implies B if every conjunct
of B is a conjunct of A; that is, the conjuncts of A
include the conjuncts of B.

Yes for formulae that are conjunctions of atomic propositions.
In general this is wrong, e.g.
f = (x1 in {1,2} and x2 in {1}) or (x1 in {2,3} and x2 in{2})
has
g = x1 in {2} and x2 in {1,2}
as a prime implicant (among some other prime implicants), but no disjunct of g is a disjunct of f.

So the problem reduces to finding formulae that include
as a conjunct the target formula phi, but do not include
a subformula that includes phi as a conjunct.


I don't understand that. I'm thinking of the target formula as a formula in the disjunctive normal form, that is a disjunction of all of the prime implicants. Are you suggesting the conjunctive normal form? This is also possible by the duality, but then I don't see how to test whether an arbitrary conjunction implies this CNF.

Best
sasha.
.