Improving the constraint framework

Now that we've lived with the constraint framework for eight months there are some clearer paths towards improvement.

Explicit constraint removal, and redundant var walking

We've just eliminated explicit constraint id management from master. The last annoying bit of explicit management foisted on people writing constraint solvers is explicit constraint removal if a constraint is entailed. Related to this annoyance is the performance issues around relevant?, runnable?, and constraint invocation.

A possible approach that addresses the current shortcomings:

(defn !=fdc [u v]
  (reify 
    IEnforceableConstraint
    IConstraintOp
    (-rator [_] `!=fd)
    (-rands [_] [u v])
    IEntailed
    (-entailed? [this _ vs]
      (disjoint? (get vs u) (get vs v)))
    IConstraintStep
    (-step [this s]
      (let-dom s [u du v dv]
        (let [du? (domain? du)
              su? (singleton-dom? du)
              dv? (domain? dv)
              sv? (singleton-dom? dv)]
          (and du? dv? (or su? sv?)
            (reify
              IEntailed
              (-entailed? [_ s]
                (-entailed? this s {u du v dv}))
              IEnforce
              (-enforce [_ s]
                (cond
                  (and su? sv? (= du dv)) nil
                  
                  su?
                  (when-let [vdiff (difference dv du)]
                    ((process-dom v vdiff) s))
                  
                  :else
                  (when-let [udiff (difference du dv)]
                    ((process-dom u udiff) s)))))))))
    IConstraintWatchedStores
    (-watched-stores [this] #{::subst ::fd})))

Note that IConstraintStep allows us to both do the pre-run -relevant? check and the -enforce step (invoke in master) without having to do multiple lookups for var values or domains. In master, the same lookups occur up to three times for a runnable & relevant constraint in master when invoked via run-constraint.

Also note that we have a new protocol IEntailed with two arities, one of which takes a map that contains vars that have changed during domain processing. -entailed? inside of -step just delegates to that. This means that prior to running a constraint we'll create a map that stores changes to vars for the post run -entailed? call - this is similar to how to how we track changes during unification. It looks like we can use IConstraintWatchedStores to know what changes to track!

We should look more closely how much constraint definitions will have to change. To reiterate the big benefits:

• No more explicit removal of constraints
• Better approach to avoiding multiple var / domain lookups
• Better pre/post entailment checking story

An open question - what will happen when a constraint gets queued, runs, and yet changes nothing? We should probably add the vars even if they don't trigger other constriants.

Other Constraints

The above outlined approach would benefit FD constraints the most, consider what != would like look:

(defn !=c [p]
  (reify
    ITreeConstraint
    IReifiableConstraint
    (-reifyc [this v r a]
      (let [p* (-reify a (map (fn [[lhs rhs]] `(~lhs ~rhs)) p) r)]
        (if (empty? p*)
          '()
          `(~'!= ~@p*))))
    IConstraintOp
    (-rator [_] `!=)
    (-rands [_] (seq (recover-vars p)))
    IEntailed
    (-entailed? [this _ _]
      (empty? p))
    IConstraintStep
    (-step [this s]
      (when (some #(not= (walk s %) %) (recover-vars p))
        (reify
          IEnforce
          (-enforce [_ s]
            (let [p (loop [sp (seq p) p p]
                      (if sp
                        (let [[x v] (first sp)
                              xv (walk* a x)
                              vv (walk* a v)]
                          (cond
                            (= xv vv) (recur (next sp) (dissoc p x))
                            (nil? (unify a xv vv)) nil
                            :else (recur (next sp) (assoc (dissoc p x) xv vv))))
                        p))]
              (if p
                (when-not (empty? p)
                  ((updatecg (with-meta (!=c p) (meta this)) a))
                a))))))
    IConstraintWatchedStores
    (-watched-stores [this] #{::subst})))

Note in this case we don't need a different -entailed? for pre and post run checks.

Disjunctive Constraints

Disequality is a disjunctive constraint. Currently our disequality implementation involves a lot of ugliness because we cannot express disjunctive constraints in the current framework - only conjuctive constraints. We would like to able to express that some constraint is satisfied if even one of its subconstraints is satisfied. At the same time we would like to be able to reify disequality in a straightforward manner.

Subsumed Constraints

If we gave each constraint an identifier we could know if a constraint is already in the constraint store.

(+fd x y z) ;; identifier [+fd x y z]

+fd here is a symbol and x, y, z are root vars. The constraint store could have a new field which simply stores this representation in a Clojure set.

Perhaps this system is good enough for disequality constraints since we'll be storing the subconstraints?