Project

General

Profile

Bug #19

GML formula takes long

Added by Thorsten Wißmann over 3 years ago. Updated 9 months ago.

Status:
New
Priority:
Normal
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

Feature #22: Directly implement GML using linear unequalitiesNewThorsten Wißmann

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

Also available in: Atom PDF