knight n s = do a <- relation ((1,1),(n,n)) m <- atmost s $ do i <- indices a ; return $ a ! i assert [m] sequence_ $ do p <- indices a return $ assert $ do q <- indices a guard $ p == q || reaches p q return $ a!q return $ decode a reaches (px,py) (qx,qy) = 5 == (px - qx)^2 + (py - qy)^2