> I've wanted to explore calling to a SAT solver (or other solvers) from > within miniKanren for a while. Do you think a simple SAT solver slong > the lines of MiniSAT could be implemented with this approach?
It's close to the original one that was made for minimips here: https://github.com/orchid-hybrid/microKanren-sagittarius/blob/master/miruKanren/eqeq-watch.scm for example: (fresh (x y) (watch x (lambda (x1) (watch y (lambda (y1) (== q (* x1 y1)))))) (== x 5) (== y 5)) > I've wanted to explore calling to a SAT solver (or other solvers) from > within miniKanren for a while. Do you think a simple SAT solver slong > the lines of MiniSAT could be implemented with this approach? I think it's to inefficient to do anything as involved as that, but may still be useful in triggering finite domain constraints or something. -- You received this message because you are subscribed to the Google Groups "minikanren" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/minikanren. For more options, visit https://groups.google.com/d/optout.
