[Question] How to reduce syntactic size of a formula

[yanntm]

Hi,

Thanks for making your package available, it's a nice piece of software.
I'm trying to minimize some boolean formulas, with the metric that resulting syntactic tree should have as few nodes as possible.
Part of the goal on my test set is the fact some atoms in formulas disappear, as they are asserted in both forms (a OR !a => true, a AND !a =>false). This is not immediately obvious, the formulas are pretty large, so I'm trying to use your package for this.

I've tried running MCQ, but the conversion to what looks like CNF makes some of my formulas blow up in size; this is not ideal.
I'm thinking of trying MCQ (which should always be better than CNF, right ?) then DNF and choosing the smallest, iff. it is syntactically smaller than my original formula.

And wrapping the whole thing so if some step/transformation blows up, just skip it and choose from remaining candidates.

But maybe there are better ways to do this ?

Thank you

[axkr]

Maybe related to #12 ?

[yanntm]

Not as far as I can see, except I'm indeed using the QMC mentionned in that post.

[czengler]

LogicNG simplifies some "easy" things on the fly, e.g. A & ~A is simplified to $true when parsing a formula. But to really compute the "syntactical minimal tree" of a formula is a very hard problem, where we have no out-of-the box algorithm in LogicNG.

We implemented some industrial applications, where simplifying the formula was part of the problem. But there we hand-crafted some algorithms based on methods of LogicNG. E.g. what you always can do is compute backbones of your formula (literals that always hold) and propagate them through your formula. We have the BackboneSimplifier for this. Depending on the input format, a CNF or DNF with a following subsumption (Subsumption) and/or unit propagation (UnitPropagation) could help.

But in general there is not "one way" to simplify a formula for all possible applications. Often domain knowledge or additional constraints can also help to simplify a formula.

Another way would be, to transform the formula to a BDD, using e.g. the FORCE heuristics. Note that this is also not possible for each formula - BDD construction is also NP-hard. But in our experience, the FORCE heuristics yields pretty good results on real-life formulas.

[czengler]

if you could provide a test formula of yours (if needed, anonymized with the Anonymizer), we could take a look at the formula, if we see some possibilities to simplify it :)

[yanntm]

Thanks for the answer; the formulas are part of a test set for the Model Checking Contest and unfortunately there is not much domain knowledge to grab here since they are mostly random (with some patterns, (a1 & a2 | a3 & a4 | ... ) & (b1 & b2 | b3 & b4 | ...) is pretty common). Given the randomness however, there is a lot of garbage that can and is simplified away by LogicNG.
I think DNF + Subsumption might be the right chain, to obtain something like a1 & (a2 | a3) ?
Would UnitPropagation sometimes simplify more variables/terms than the plain DNF ?

[yanntm]

thanks for the help I found some compromises I can work with, basically with some timeouts and limits to expansion size that is accepted, and trying different forms.