Skip to content

FastLAS gets stuck in "Computing SAT-sufficient subset" when using numeric comparison predicates #9

Description

@Maysk

I have been experimenting with numeric operators in FastLAS, but I am facing performance issues.

In particular, the program below takes a very long time and eventually stops at:

Computing SAT-sufficient subset...

It does not seem to progress further.

Example Program

num(0..100).
#maxv(3).

#bias("penalty(1, X) :- in_head(X).").
#bias("penalty(1, X) :- in_body(X).").

#modeh(big(var(inst))).

#modeb(1, height(var(inst), var(num))).

#modeb(1, width(var(inst), var(num))).


greater_than(X,Y) :- num(X), num(Y), X > Y.
less_than(X,Y) :- num(X), num(Y), X < Y.

#bias("comparison(H) :- in_body(greater_than(H,_)).").
#bias("comparison(H) :- in_body(less_than(H,_)).").

#bias("attribute(H) :- in_body(height(_,H)).").
#bias("attribute(H) :- in_body(width(_,H)).").

#bias(":- attribute(H), not comparison(H).").
#bias(":- comparison(H), not attribute(H).").

#bias(":- in_body(greater_than(H,C1)), in_body(greater_than(H,C2)), C1 > C2.").
#bias(":- in_body(less_than(H,C1)), in_body(less_than(H,C2)), C1 > C2.").

#modeb(greater_than(var(num), const(num))).
#modeb(less_than(var(num), const(num))).

inst(a).
inst(b).
inst(c).
inst(d).
inst(e).

#pos(p1, {big(a)}, {}, {height(a,5). width (a, 70).}).
#pos(p2, {big(e)}, {}, {height(e,7). width (e, 60).}).

#neg(n1, {big(b)}, {}, {height(b,4). width(b, 50).}).
#neg(n2, {big(d)}, {}, {height(d,4). width(d, 80).}).
#neg(n3, {big(c)}, {}, {height(c,7). width(c, 50).}).

Command Used
FastLAS --threads 2 --nopl exemplo_numerico.las --space-size --debug

Am I doing something wrong?

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Fields

    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions