core-logic

hifumi123 2024-06-30T21:42:49.709259Z

Is there a feasible way to express minimization in CLP(FD)? My use case involves finding x_1, ..., x_j so that m = a_1 x_1 + ... + a_j x_j has minimal distance from a natural number n. i.e. |m - n| is minimized. Everything here is a natural number. It's easy to write (fd/eq (= m (+ (* a1 x1) ... (* aj xj))) but this ends up generating a bunch of "non-optimal" solutions. If you ignore the minimization problem, then you can add a variable r and a goal like

(l/conde
  [(fd/+ m r n)
   (fd/>= m n)]
  [(fd/+ n r m)
   (fd/< m n)])
so that we get values of |m - n| in each solution. Then we can manually pick the solution with smallest r from Clojure code. But this still has a major performance issue since we generate possibly thousands of non-optimal solutions I've started to think what I want is an SMT solver instead of core.logic, but Clojure doesn't seem to have any good libraries or wrappers for things like Z3, so I'm trying my best to stick with core.logic