[BUG] Exponential performance dropoff in addClauses with increasing number of AND subclauses in OR

[jpd236]

Describe the bug
When creating a clause of the form LogOp.or(LogOp.and(a, b), LogOp.and(c, d), ...) and adding it via Model#addClauses, the performance drops off exponentially.

I don't encounter the same performance issue when building an equivalent expression with a.and(b).or(c.and(d).or(...)).

To Reproduce
Here is some toy code that reproduces the issue. On my laptop, I start to see exponential increases in elapsed time around 10 AND clauses, and stop seeing progress above 17 AND clauses.

import org.chocosolver.solver.Model;
import org.chocosolver.solver.constraints.nary.cnf.LogOp;
import org.chocosolver.solver.variables.IntVar;

public class ChocoIssue {
    public static void main(String[] args) {
        Model m = new Model();
        IntVar[] vars = m.intVarArray(2, 1, 2);
        for (int i = 1; i < 100; i++) {
            LogOp[] ops = new LogOp[i];
            for (int j = 0; j < ops.length; j++) {
                ops[j] = LogOp.and(vars[0].eq(1).decompose().reify(), vars[1].eq(2).decompose().reify());
            }
            long startTime = System.nanoTime();
            m.addClauses(LogOp.or(ops));
            long endTime = System.nanoTime();
            System.out.println("Elapsed time for " + i + " clauses = " + (endTime - startTime));
        }
    }
}

Expected behavior
Since both approaches appear to be logically equivalent, I'd expect performance to be about the same. That said, I admit I'm a novice with this library and may absolutely be missing something silly that I'm doing here.

Environment (please complete the following information):

• Choco-solver version: 4.10.7
• JRE : 8

[jgFages]

Hello,

It seems to come from the CNF conversion (from an OR(AND...) expression to an AND(OR...) expression), which is huge in this case as it is somehow the exact opposite. @cprudhom do you think the CNF is necessary or is there here a margin for improvement ?

[cprudhom]

Indeed, the first step of m.addClauses(LogOp) API is to convert the syntactic tree in conjunctive normal form (CNF), that is a conjunction of clause (disjunction of literals).
In your case, the declared tree is in disjunctive normal form (DNF), a disjunction of conjunctions of literals, and the conversion to CNF is required (like https://en.wikipedia.org/wiki/Conjunctive_normal_form#Basic_algorithm).
Then, each clause is declared and added to the model.

In the second usage, the a.and(b).or(c.and(d).or(...)) expression is not pre-processed (there is no need for CNF) and is certainly decomposed into low arity constraints.