Incremental optimizer performance

[dreinon]

Is it normal for the incremental optimizer to stay a long time (minutes) after finding optimal solution:
value:100, elapsed time(s):46.94204223199995?

[dreinon]

Now I found that when I stopped the process (Ctrl+C) I get this output:

value:100, elapsed time(s):46.94204223199995
C^C     No solution can be found for problem XXXXXX.
        Reason: canceled
        total number of iterations: 2
        value: 100
       XXXXXXXXX satisfiability checked in 46.94s

Substituded private info for XXX

[tpaviot]

Yes it is. Each time the incremental solver finds a value, it looks for another one, better. If ever the previous solution was the optimum, then there's no other solution and the solver may take time to find one or check satisfiability.

[dreinon]

Although if it found a solution for 100 utilization in 46 secs (output: XXXXXXXXX satisfiability checked in 46.94s), what is it doing after finding it that takes that long?

[tpaviot]

Well, I don't know, I never faced this issue. minutes you say? How many exactly?

[dreinon]

Right, sorry, I might have explained myself wrong. I meant to ask if in the current implementation there is a reasonably long process after getting to 100. It's weird because it takes minutes after logging this:
value:100, elapsed time(s):46.94204223199995
But whenever I press Ctrl+C, the solver says not solution could be found because cancelled, but then logs:

total number of iterations: 2
        value: 100
       XXXXXXXXX satisfiability checked in 46.94s

I don't exactly know how many minutes because I stopped it before, but it had already taken like 5.
Thanks!

[tpaviot]

What is the max_time value for your solver?

[dreinon]

I set a 1200 so it could always solve it, might this be the issue?

[tpaviot]

Yes. The solver tries to find a solution for 101, but there's not any value. I have to add another constraint telling that the resource utilization cannot exceed 100 and that it's not worth trying to find a better value.

[tpaviot]

@dreinon can you please check commit 147f7f5

[dreinon]

Oh, I didn't know that by adding that constraint it would stop there, I first thought to stop the incremental optimizator loop when it targets values of 100 or 0. Nice though!

[dreinon]

Having tried this constraint solution, I think it doesn't work as expected. Before, the optimizer was able to find 100 utilization solution in 15-60 seconds, but it directly found the 100 solution. Now it does this:

value:87, elapsed time(s):4.068104371999652
value:94, elapsed time(s):90.38284010200005
value:97, elapsed time(s):91.11049879999882
value:100, elapsed time(s):91.77813899299872

It's still very good, but it's strange that it behaves differently, right?

[tpaviot]

Adding a bound to a z3 integer variable slightly changes the wy the solver performs the computation (however it's a bit unclear to me). Did you try the "QF_IDL" logics? Another way to go would be to add a "stop_value" parameter to the incremental solver, that would break the loop as soon as the objective is reached. This way, you could have your 15-16s solution. FYI it's difficult for me to benchmark changes without any additional information. I recently add a benchlark/ folder (see https://github.com/tpaviot/ProcessScheduler/tree/master/benchmark), it is quite useful to measure impacts of commits on computation time/memory footprint. If you can contribute a similar benchmark for your problem, it will be quite useful.

[dreinon]

Solver type:
===========
        -> SMT solver using logics QF_IDL
Incremental optimizer:
======================
        No solution can be found for problem XXXXXXx
        Reason: Benchmark is not in QF_IDL (integer difference logic).

Got this when I used "QF_IDL" logics

[tpaviot]

yep, me too, try "QF_UFIDL" that should work

[dreinon]

I looked at the benchmark file. With contribute with a similar benchmark, you mean implement it in my problem and send you the output, or make an example of my problem without private info and upload a benchmark file for it to the repo?

[tpaviot]

The second Le mar. 1 juin 2021 à 14:06, dreinon ***@***.***> a écrit :

…

I looked at the benchmark file. With contribute with a similar benchmark, you mean implement it in my problem and send you the output, or make an example of my problem without private info and upload a benchmark file for it to the repo? — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#54 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAFBFIW6VQAG4KVFMUTMY2LTQTEL3ANCNFSM454HZLDQ> .

[dreinon]

I think I could do that.

[tpaviot]

cool, after that I can automatically run the benchmark on azure cloud to check the effects of any change

[dreinon]

N = list(range(10, n, step))  # from 4 to N, step 2

for num_dev_teams in N:

Is this part of the dev_team problem, or is it to see how the problem scales?

[tpaviot]

Just to see how it scales, and what is the complexity O(n) or O(n^2) or O(n^3) etc.

[dreinon]

Ok.

[dreinon]

I have the following variables that might be interesting to see how the problem scales wrt them. Could you tell me which ones do you find interesting?

HORIZON = 60 # Horizon of the problem (multiple of 10 for simplicity)
PERIODS = [(10*i, 10*(i+1)) for i in range(int(HORIZON/10))]  # Periods of 10 slots from 0 to horizon
MAX_TASKS_PER_PERIOD = 2 # Maximum tasks that a worker can do in each period (workload constraint)
MAX_TASKS_IN_PROBLEM = 4 # Maximum tasks that a worker can do in the whole problem
NB_WORKERS = 10 # Number of workers
NB_TASKS_PER_WORKER = 5 # Number of optional tasks per worker

[tpaviot]

Setting the HORIZON as the variable for the benchmark would be interesting, because it increases the periods and finally the max_tasks

[dreinon]

Okay!