cnf() reorders the variables

[axkr]

In this JUnit test case the cnf() method reorders the variables and the JUnit test fails:

	public void testLogicNGCNF() {
		final FormulaFactory f = new FormulaFactory();
		final Variable x = f.variable("x");
		final Variable y = f.variable("y");
		final Literal notX = f.literal("x", false);
		final Literal notY = f.literal("y", false);
		// x & ~y | ~x & y
		final Formula formula = f.or(f.and(x, notY), f.and(notX, y)).cnf();
		assertEquals("(x | y) & (~x | ~y)", formula.toString());
	}

See: Symja JUnit tests

[SHildebrandt]

Hi,
LogicNG doesn't want to make any guarantee about the order of operands. I think in this case the order is just due to the internal implementation of the cnf algorithm. However the order can also be different because the formula factory caches all formulas it creates. See this example:

final FormulaFactory f = new FormulaFactory();
final Formula or1 = f.or(f.variable("x"), f.variable("y"));
final Formula or2 = f.or(f.variable("y"), f.variable("x"));
System.out.println(or1); // x | y
System.out.println(or2); // x | y
System.out.println(or1 == or2); // true

The second formula or2 is the same object as or1 since LogicNG recognizes, that both are semantically equal.

Btw. LogicNG even applies some simplifications like absorption, removal of duplicate operands, and some more, when formulas when they are created. For example

System.out.println(f.or(f.variable("x"), f.variable("x"), f.falsum())); // x

Hope this helps a bit to understand the way LogicNG works. ;)

[axkr]

If I have more than 2 variables and create a "big conjunctive normal form" the variables in every single clause could have different orderings?

And if I'm using Java Formula#equals() method for two arbitrary "mixed variable forms of cnf()" which are "logical identical", I get true as result?

[d-bischoff]

If I have more than 2 variables and create a "big conjunctive normal form" the variables in every single clause could have different orderings?

Yes.
You don't even need to create a CNF. The variable order inside each clause is not guaranteed to be as it was in the input. See the example from @SHildebrandt above.

And if I'm using Java Formula#equals() method for two arbitrary "mixed variable forms of cnf()" which are "logical identical", I get true as result?

If you mean "logical identical" as in syntactically identical, then yes.

factory.and(factory.variable("x"),factory.variable("y")).equals(factory.and(factory.variable("y"),factory.variable("x"))) returns true

If you mean semantically equivalent, then the answer might be false. You would need to call the solver for that question.

[czengler]

The equals method for formulas in LogicNG takes some trivial mathematical rules like commutativity or absorption into account.

That means, that formulas like "A & B" and "B & A & A" are considered equals. But it is not a full semantical equivalence check. Like @d-bischoff said: therefore you would have to call a SAT solver.

The formula factory in LogicNG is there to minimize heap consumption. Therefore, formulas are not created twice, if they are equal. Therefore if you create a formula "A & B" and afterwards you create a formula "B & A" with the same factory, the second one is not generated again, but the first one is returned.

[axkr]

So this is only a problem of the Formula#toString() method for easier readability?

[d-bischoff]

The described phenomenon is not only a property of Formula#toString(). Internally the variables are also re-sorted if you will. However this is not important in any case since the formulas are semantically equivalent. So I don't view this as a problem at all.