Generate repairing model for the tuning

ozgurakgun commented 4 years ago

A subset of the where statements can be converted to irace forbidden statements. Waiting for input from @ndangtt on this.

ndangtt commented 4 years ago

Hi Oz!

Sorry it took so longgg to have it! Here we go! :D

In this first proposal, we focus on partial function only. It should be extended to other types later on when this one is tested successfully. Here I assume that we already replace middle/delta as min/max (pull request).

What we need is a repair.essence file generated automatically by conjure generator-parameter. This model receive as input a generator configuration. Solving it will give us a repaired version of the generator configuration. There are two groups of repairing constraints:

Constraints to make sure that the repaired values always follow the rules of min<=max
Constraints represent the dependency between cardinality and the defined domain of a partial function.

Example 1: a partial function with fixed domain

$ model.essence
given f: function (minSize 1) int(1..10) --> int(1..)

$ generator.essence
given f_cardMin: int(1..100)
given f_cardMax: int(1..100)
given f_defined_min: int(1..10)
given f_defined_max: int(1..10)
given f_range_min: int(1..100)
given f_range_max: int(1..100)
...

The repair.essence should include:

All parameters in generator.essence as input (including the percentage one for boolean function in general cases, even though it doesn't need to be repaired), and a repaired_ decision variable for each of them
min/max constraints

a constraint to make sure that the maximum cardinality of a partial function never exceeds the size of its domain.


$ repair.essence
given f_cardMin: int(1..100)
given f_cardMax: int(1..100)
given f_defined_min: int(1..10)
given f_defined_max: int(1..10)
given f_range_min: int(1..100)
given f_range_max: int(1..100)

find repaired_f_cardMin: int(1..100) find repaired_f_cardMax: int(1..100) find repaired_f_defined_min: int(1..10) find repaired_f_defined_max: int(1..10) find repaired_f_range_min: int(1..100) find repaired_f_range_max: int(1..100)

$ Constraints to make sure that the the repaired values always follow the rules of min<=max such that repaired_f_cardMin <= repaired_f_cardMax, repaired_f_defined_min <= repaired_f_defined_max, repaired_f_range_min <= repaired_f_range_max

$ Constraints represent the dependency between cardinality and the defined domain of a partial function such that (repaired_f_defined_max-repaired_f_defined_min+1) >= repaired_f_cardMax

minimising |repaired_f_cardMin-f_cardMin| +|repaired_f_cardMax-f_cardMax| +|repaired_f_defined_min-f_defined_min| +|repaired_f_defined_max-f_defined_max| +|repaired_f_range_min-f_range_min| +|repaired_f_range_max-f_range_max|

Note: You may wonder if this repairing model would do something like this: given `x_min=10` and `x_max=4`, we may end up having the repaired version as `x_min=x_max=10` or `x_min=x_max=4`. But it won't happen, as in my repairing script, I already fixed those in advance by simply swapping values of min and max variables if `min>max` before giving them to `repair.essence` as input, i.e., `x_min=4` and `x_max=10`. The constraints shown in `repair.essence` are just to make sure that the `repaired_` values of those variables still follow this rule of `min<=max`.

### Example 2: a partial function with domain's upper bound depending on another variable
When the partial function's domain's upper bound is defined by another variable, we have an extra constraint on the dependency.

$model.essence given m: int(1..) given f: function (minSize 1) int(1..m) --> int(1..)

$ repair.essence ... such that repaired_f_defined_max <= repaired_m_max, $ this is the extra constraint (repaired_f_defined_max-repaired_f_defined_min+1) >= repaired_f_cardMax ...

### Example 3: a partial function with domain's lower bound and domain's upper bound depending on other variables
Similarly, when the partial function's domain's lower and upper bounds are defined by other variables, we have two extra constraints on the dependency.

$ model.essence given m1: int(1..) given m2: int(1..) given f: function (minSize 1) int(m1..m2) --> int(1..)

$ repair.essece ... such that repaired_f_defined_min >= repaired_m1_min, $ this is the extra constraint repaired_f_defined_max <= repaired_m2_max, $ this is the extra constraint (repaired_f_defined_max-repaired_f_defined_min+1) >= repaired_f_cardMax ...

### Example 4: the same as example 3, but with a boolean function
For boolean function, we have the `f_percentage` param for the generator spec. We don't need to do any repairing for such param, so the only thing we need is to have a constraint to make sure that the repaired one is equal to the original value.

$ model.essence given m1: int(1..) given m2: int(1..) given f: function (minSize 1) int(m1..m2) --> bool

$ repair.essence ... given f_percentage: int(0..100) find repaired_f_percentage: int(0..100) such that repaired_f_percentage = f_percentage $ this is the repairing constraint ...



[testcase-01.zip](https://github.com/conjure-cp/conjure/files/4535806/testcase-01.zip)
[testcase-02.zip](https://github.com/conjure-cp/conjure/files/4535808/testcase-02.zip)
[testcase-03.zip](https://github.com/conjure-cp/conjure/files/4535809/testcase-03.zip)
[testcase-04.zip](https://github.com/conjure-cp/conjure/files/4594082/testcase-04.zip)

ott2 commented 4 years ago

Although I have reservations about whether we can always solve the repair in reasonable time (these kinds of problems can be very hard, and if we are assuming that repair is quick and easy when it is not, then it might be better just giving up on the current parameter vector and trying another one), I do support the change to min/max. It made sense to use mid/delta but it is becoming more and more difficult to justify it now.

ndangtt commented 4 years ago

@ott2: regarding the difficulty of the repairing problem, the constraints described above seem all trivial to solve to me. But it's just simply my guess, as I don't have experience with minion's solving procedure. If we do find that they are difficult, or if the repairing instances are too large to go through the pipeline (which I don't really expect to happen, as the repairing model is pretty flat), then we could consider using Athanor instead of minion to solve the repairing problem, as proving unsat is not a necessary requirement. (we still need to use minion for solving the generator spec though, as we need the ability to prove unsat in that case).

Some other reasons why I think we should use the repair:

The repair problem only contains integer decision variables, which makes it generally much simpler than the generator problem (which can contain high-level structures as decision variables). This is why I think it should be easy to solve.
Giving up on a generator configuration immediately can cause a big issue with the tuning. If the space is largely dominated by unsat generator configurations (which is the case for our classical planning problems), the tuning won't be able to do anything useful, as there's no guidance for the search.

ozgurakgun commented 4 years ago

Example 4: I don't think this one is necessary since we are minimising the difference.

ndangtt commented 4 years ago

@ozgurakgun: you're right! We don't need it indeed! :)

ozgurakgun commented 4 years ago

here it is! let me know if anything is broken please.

ndangtt commented 4 years ago

Thanks very much for the implementation, Oz!

I currently get three issues. Could you please help to have a look? :D

Issue 1: incorrect variable names in some of the generated repairing constraints, as listed below for example 3.

$ model-instanceRepair.essence
given m1_min: int(1..100)
given m1_max: int(1..100)
given f_defined_min: int(1..100)
given f_defined_max: int(1..100)
such that
    repaired_f_defined_min >= m1, $ corrected version: repaired_m1_min instead of m1
    repaired_f_defined_max <= m2, $ corrected version: repaired_m2_max instead of m2
...

model.essence.txt model-instanceRepair.essence.txt model-instanceRepair-corrected.essence.txt

Issue 2: for total functions, we don't have cardinality and defined params. However, those params currently appear in the repairing spec. They should be removed, together with the `such that` keyword.

$ model.essence
given f1: function (total) int(1..10) --> bool

$ model-instanceRepair.essence
given f1_percentage: int(0..100)
find repaired_f1_percentage: int(0..100)
such that                       $ this line should be removed
    f1_cardMin <= f1_cardMax,   $ this line should be removed
    f1_defined_min >= 1,        $ this line should be removed
    f1_defined_max <= 10,       $ this line should be removed
    f1_defined_min <= f1_defined_max    $ this line should be removed
minimising sum([|repaired_f1_percentage - f1_percentage|; int(1)])

model.essence.txt model-instanceRepair.essence.txt

Issue 3: when partial functions are wrapped up in a record, the repairing constraints are no longer generated by `conjure`.

$ model.essence
given r: record { f: function int(1..10) --> bool }

$ model-instanceRepair.essence
given r_f_cardMin: int(0..10)
given r_f_cardMax: int(0..10)
given r_f_defined_min: int(1..10)
given r_f_defined_max: int(1..10)
given r_f_percentage: int(0..100)
find repaired_r_f_cardMin: int(0..10)
find repaired_r_f_cardMax: int(0..10)
find repaired_r_f_defined_min: int(1..10)
find repaired_r_f_defined_max: int(1..10)
find repaired_r_f_percentage: int(0..100)
such that           $ all repairing constraints are missing
minimising
sum([|repaired_r_f_cardMin - r_f_cardMin|, |repaired_r_f_cardMax - r_f_cardMax|,
         |repaired_r_f_defined_min - r_f_defined_min|, |repaired_r_f_defined_max - r_f_defined_max|,
         |repaired_r_f_percentage - r_f_percentage|;
             int(1..5)])

model.essence.txt model-instanceRepair.essence.txt

ndangtt commented 4 years ago

Hi Oz,

Please find below some of the issues I still have:

testcase-03:

$ model.essence
given m1, m2: int(1..)
given f: function (minSize 1) int(m1..m2) --> int(1..)

$ model-instanceRepair.essence
....
such that
  repaired_f_defined_min >= m1_min, $ correcting: repaired_m1_min instead of m1_min
  repaired_f_defined_max <= m2_max, $ correcting: repaired_m2_max instead of m2_max
...

The reason why I'd like to have repaired_m1_min instead of m1_min is because it provides more flexibility for the repairing. Consider this case, for example: f_defined_min and f_cardMin are already good, we'd only want to repair m1_min to satisfy the constraints.

testcase-06: `defined_min` and `defined_max` still appear in repair essence for total functions

$ model.essence
given f: function (total) int(1..10) --> bool

$ model-instanceRepair.essence
...
such that f_defined_min <= f_defined_max  $ corrected: this line should be removed
...

testcase-07: partial functions where domain's lower & upper bounds are expressions.

$ model.essence
given m1,m2: int(1..)
given r: record {
    f: function int(0+m1..1+m2) --> bool
}

$ model-instanceRepair.essence
...
such that
    repaired_r_f_defined_min >= 0 + m1,  $ corrected: 0 + repaired_m1_min
    repaired_r_f_defined_max <= 1 + m2,  $ corrected: 1 + repaired_m2_max
...

testcase-08: partial functions where domain's lower & upper bounds are expressions with multiple sub-domains (we're currently under the assumption that those sub-domains are contiguous, we'd need to update the repair constraints on cardinality if they're not, but it's more complicated...)

$ model.essence
given m1,m2,m3: int(1..)
letting d be domain int(m1..m1+m2,m1+m2+1..m1+m2+m3)
given f: function d --> bool

$ model-instanceRepair.essence
...
such that
    $ correction 1: max -> min
    $ correction 2 (testcase-07): m1 -> repaired_m1_min, m2 -> repaired_m2_min
    repaired_f_defined_min >= max([m1, m1 + m2 + 1; int(1..2)]),  

    $ correction 1: min -> max
    $ correction 2 (testcase-07): m1 -> repaired_m1_max, m2 -> repaired_m2_max, m3 -> repaired_m3_max
    repaired_f_defined_max <= min([m1 + m2, m1 + m2 + m3; int(1..2)]),
...

testcase-09: partial functions with domain defined by cartesian products.

Sorry I didn't realise this case in my original post. Classical planning models are so painful :P

$ model.essence
given m1, m2: int(1..)
letting d1 be domain int(1..m1)
letting d2 be domain int(1..m2)
given f: function (d1,d2) --> bool

$ model-instanceRepair.essence
...
find repaired_f_defined_tuple1_min: int(1..100)
find repaired_f_defined_tuple1_max: int(1..100)
find repaired_f_defined_tuple2_min: int(1..100)
find repaired_f_defined_tuple2_max: int(1..100)
such that
    $ current output, this causes issues as there're no f_defined_min and f_defined_max
    $f_defined_max - f_defined_min + 1 >= repaired_f_cardMax,
    $ corrected output
    (repaired_f_defined_tuple1_max-repaired_f_defined_tuple1_min+1)*(repaired_f_defined_tuple2_max-repaired_f_defined_tuple2_min+1) >= repaired_f_cardMax,
...

ozgurakgun commented 4 years ago

ball in your court again @ndangtt :)

I won't bother closing the issue this time, feel free to close if you are happy with everything.

ndangtt commented 4 years ago

It passes all the tests so far, so I'm gonna close the issue :)

ozgurakgun commented 4 years ago

Oooooh - I was developing an emotional connection with this issue :)

Maybe open a new issue so I can stop thinking about the number 465 if/when new issues arise?

ndangtt commented 4 years ago

Haha yes I will. Let's leave this one rest in peace :P

conjure-cp / conjure