1. 29

  2. 11

    So that’s why you were asking about SMT solver techniques :P

    This is really cool! I think, though, that SMT is the wrong tool for the job. While it can do minimization, most SMT solvers aren’t really designed to do that, making them a lot slower. By contrast, constraint solvers are built from ground-up to do optimization problems. Not only are they going to have better heuristics, but they also have significant quality of life benefits. Like when you said

    Initial runs would sit and spin for ten or twenty minutes, and give no result.

    Something like MiniZinc outputs each new best-answer it comes across.

    In MiniZinc we could also use an inbuilt predicate:

    predicate knapsack(array [int] of int: w,
                       array [int] of int: p,
                       array [int] of var int: x,
                       var int: W,
                       var int: P)

    In which case the problem reduces to something like

    constraint knapsack(engine_prices, engine_thrust, out, 210, Thrust); 
    constraint knapsack(engine_prices, engine_steering, out, 210, Steering); 
    maximize Thrust + Steering/32;

    Since we use inbuilts, MZn gets massive speedups.

    ps omg is this escape velocity

    1. 4

      Yes! SMT solvers is the wrong tool for the job. I’ve had z3 running for eighteen hours now and I suspect it won’t be done in my lifetime.

      Davean has already written a solver that uses limp and coinor-cbc to solve the entire problem in three milliseconds, so I’m writing an addendum to the whole post.

      Also yes! Endless Sky is based on Escape Velocity!

    2. 4

      I feel like MiniZinc or PiCat would be better for this scenario

      1. 4

        Agreed, but I didn’t know any different before diving into the field of optimization!

      2. 2

        Thanks for writing this; a really nice little intro! :-)

        1. 1

          Glad you enjoyed it!

          I’m working on a follow up because I got a bunch of replies fixing errors in the post, describing solutions that work for them in much less time, three or four improved solutions to the exact same problem. Part 2 will have even more useful info!