Minimization doesn't finish

[fredericg]

Heb een zeer eenvoudige minimalisatieapplicatie, maar om een of andere reden raakt de minimize(t,s,term) methode in een loop.

vocabulary bike_voc{
    type Fiets
    type Klant
    type Uren isa int
    type Prijs isa int
    type Totaal isa int

    PrijsPerUur(Fiets):Prijs
    partial TotaalPrijs(Fiets,Klant):Prijs
    Verhuurd(Klant,Fiets,Uren)
    TotaalVerhuurd:Totaal
}

theory fiets_theo:bike_voc{
    !f: ?=<1k u: Verhuurd(k,f,u).       

    {
        !f k t: TotaalPrijs(f,k) = t <- ?u: Verhuurd(k,f,u) & t = PrijsPerUur(f)*u.
    }

    {
        TotaalVerhuurd = #{k f u: Verhuurd(k,f,u)}.
    }
}

term totaal_verhuurd:bike_voc{
    -TotaalVerhuurd
}

structure fiets_struc:bike_voc{
    Fiets = {B1; B2; B3}
    Klant = {Tom; Jan; Marc}
    Uren = {1..24}
    Totaal = {0..5}
    Prijs = {0..999}

    PrijsPerUur = {
                    B1->5;
                    B2->3;
                    B3->2
                  }
}

include <mx>
procedure main(){
    stdoptions.verbosity.solving = 1
    stdoptions.nbmodels = 1
    stdoptions.xsb = true
    stdoptions.cpsupport = true

    local models = minimize(fiets_theo,fiets_struc,totaal_verhuurd)
    printmodels(models)
}

[fredericg]

Het punt is dat ik minimize gebruik om te maximizen door het tegengestelde van de term te nemen, als ik minimize, zonder de - voor de term eindigt de minimization wel.

[Broes De Cat]

Minimize zit niet in een loop, maar heeft waarde 3 gevonden en is nu aan het bewijzen dat dat de optimale waarde is. Optimaliteit bewijzen is typisch niet makkelijk (je range van prijs is niet 'klein'), dus dat kan lang duren. Maar ik zal eens kijken of een herformulering helpt.

Side note: cpsupport en definities werken niet samen. Als je functies definieert die niet recursief zijn, gebruik je voorlopig beter equivalenties om betere performantie te hebben.

[fredericg]

Aha, bedankt voor interessante info!

[Broes De Cat]

Je kan je issue oplossen door TotaalVerhuurd = #{k f u: Verhuurd(k,f,u)}. aan te passen naar TotaalVerhuurd = #{f: ?k u: Verhuurd(k,f,u)}. omdat je eigenlijk fietsen aan het tellen bent, en geen fietsen+uren+klanten