logic-ng/LogicNG

When converting string formula, getting formula containing ~@RESERVED_CNF_0

Closed this issue · 3 comments

hwhh commented

When trying to parse the following string, the resulting CNF comes back with lots of @RESERVED_CNF_0 in it ?

(A & ~B | ~A & B) & (C & B & ~A & ~D & ~E | C & ~B & A & ~D & ~E | C & ~B & ~A & D & ~E | C & ~B & ~A & ~D & E | ~C & B & A & ~D & ~E | ~C & B & ~A & D & ~E | ~C & B & ~A & ~D & E | ~C & ~B & A & D & ~E | ~C & ~B & A & ~D & E | ~C & ~B & ~A & D & E) & (A & ~F | ~A & F) & (E & ~C | ~E & C)

rouven-walter commented

Hi hwhh, by parsing your formula string, no @RESERVED_CNF_0 variables will be included. However, I assume you converted your formula to a CNF after the parsing step. Can you show your code?

When converting a formula to CNF by formula.cnf() LogicNG tries to convert the formula to CNF by factorization. However, if certain criterias are fullfilled the CNF conversion switches to Tseitin/Plaisted-Greenbaum in order to convert the formula to an equisatisfiable CNF. And by using Tseitin/Plaisted-Greenbaum new auxiliary variables are created and added to the formula. These auxiliary variables are the @RESERVED_CNF_0 strings you encountered.

If you want a CNF without those auxiliary variables, you can explictely state that the CNF conversion should be done via factorization only:

String s = "(A & ~B | ~A & B) & (C & B & ~A & ~D & ~E | C & ~B & A & ~D & ~E | C & ~B & ~A & D & ~E | C & ~B & ~A & ~D & E | ~C & B & A & ~D & ~E | ~C & B & ~A & D & ~E " +
                "| ~C & B & ~A & ~D & E | ~C & ~B & A & D & ~E | ~C & ~B & A & ~D & E | ~C & ~B & ~A & D & E) & (A & ~F | ~A & F) & (E & ~C | ~E & C)";
FormulaFactory f = new FormulaFactory();
PropositionalParser p = new PropositionalParser(f);
Formula cnf = p.parse(s).transform(new CNFFactorization());
dstuebing commented

Hi, I have a similar problem when minimizing a formula with the Quine-McCluskey algorithm. For example, for minimizing formula
~5 & ~4 & 3 & 2 & 1 | ~3 & ~7 & ~2 & 1 | ~6 & 1 & ~3 & 2 | ~9 & 6 & 8 & ~1 | 3 & 4 & 2 & 1 | ~2 & 7 & 1 | ~10 & ~8 & ~1
I get a formula that has lots of auxiliary variables (e.g.@RESERVED_CNF_0).

Is it possible to get a minimized formula without these auxiliary variables?

rouven-walter commented

Hi @dangerdave1,
thank you, you just discovered a bug within the Quine-McCluskey algorithm. Instead of minimizing the given input formula, mistakenly the Tseitin transformed formula (containing auxiliary variables) was minimized and returned by Quine-McCluskey. We fixed this bug in the newest LogcNG version 1.4.1, released today. With the new release, the result is a minimized DNF without auxiliary variables.