## Bug #19

### GML formula takes long

Start date:

05/17/2014

Due date:

% Done:

0%

**Description**

The following GML formula takes much time:

./coalg.native sat GML <<< '~(A & B) & ~(B & C) & ~ (C & A) |- {>= 10 R} A & {>= 10 R} B & {>= 10 R} C & {<= 30 R} True'

Why? What's slow? The tableaux-rule? Minisat? GMLMIP?

Are tableaux-rules correct? Does it take that long in other reasoners like GMLMIP?

**Subtasks**

### History

#### #1 Updated by Thorsten Wißmann over 3 years ago

If you run the following input with glmmip, it takes very long (in the sense of: not terminating within minutes). It's because there are many queries to glpk, some of them take about 30 seconds, many of them less than a second. But all in all, it doesn't finish fast.

Logic:GML <9>p0 & <9>p1 & <9>p3 & ~<30>true

So this reduces to: Is gmlmip generating the correct queries for glpk? Is it a glpk-bug? Is it just a very hard problem? (actually very improbable if you look at the cardinalities)

#### #2 Updated by Thorsten Wißmann over 3 years ago

**Assignee**set to*Thorsten Wißmann***Priority**changed from*High*to*Normal*

Should be fixed as soon our own implementation of GML works.

#### #3 Updated by Thorsten Wißmann 9 months ago

On a fast machine, one gets the correct answer within 3 minutes:

$ ./main input-long-runtime Satisfiable Total Time: 171.648