RFC: Constraints

[dcz-self]

I followed up on the suggestions from #37 (comment) and committed this proof of concept.

This is minimalistic and re-uses is/2 to constrain some variable to "less than N". For example:

?- is(A, 2), is(A, 5).
Found solution:
  A = #<2
No more solutions.

And to check if this makes sense for fully resolving variables, negative numbers are not allowed:

?- is(A, 2), is(A, 1).
Found solution:
  A = 0
No more solutions.

This messes with the unification core a bit. A variable can now be partially resolved, and there are "Constraint" terms to hold the data. It's probably actually not even needed, given that a constraint can be any term, but having a Rust-native type makes a Rust resolver easier.

Miraculously, this only breaks arithmetics tests (because of the re-used predicate).

Does this look like the right track?

[fatho]

I don't have a lot of time currently, so I just quickly skimmed it and left some thoughts. Probably in a week or two I can have a more in-depth look.

[fatho]

In the final version, anything resolver defined should just be represented as an AppTerm I'd say. Only reason I turned Cut into its own term type is because it has special implementation support in the solver core.

The surface language doesn't necessarily need to stick to alphanumeric names and prefix-notation for those special app-terms either. It would be fine to e.g. parse X #< 4 in the surface language as an AppTerm of the form #< (X, 4)

[dcz-self]

I did this mostly because it's more comfortable to have a Rust structure to operate on, rather than parse the terms AST every time a constraint needs to be dealt with.

If there was a generic way to add a constraint of an arbitrary type, I'd have used that.

[fatho]

This approach doesn't seem to generalize easily to multiple constraints. Intuitively, I'd say that variables are still either bound (Some(value) ) or unbound (None), but then on top of that, we keep another field in the state with the constraints.

That could be something like constraints: HashMap<Var, Vec<Constraint>>, but with some caveats such as that we need to be able to undo constraints when backtracking.

These constraints would then be used in two ways:

1. When finally unifying an unbound variable with a value, that value is checked against the constraints. This could easily be done by just making the unification of such variables push additional goals derived form the constraints onto the goal stack.
2. There could be a non-det predicate that binds a variable to all values that are still allowed by its current constraints, if one wishes to enumerate those values.

[dcz-self]

VarValue::Constrained<Term> could just become VarValue::Constrained<Vec<Term>>.

I initially wanted to add a special Constraints field, but:

1. I wanted to avoid altering backtracking, I don't understand that yet
2. Constraints are useless when the variable is bound to something anyway, giving variables 3 real states to be in. Okay, 2 states if constraints are a set of N, where 0∈N.

I don't understand goals yet, so the only way I could see checking the constraint against values was in the resolver. I guess I'll wait and see how you suggest it be done with goals.

Regarding 2., yeah, that would need to be done either way.

[fatho]

2. Constraints are useless when the variable is bound to something anyway

Not quite. Even if constraints appear before the unification of the variable, they can make the unification fail. Suppose you have X #< 4, X = 5 (where = is just unification), then that unification should obviously not succeed.

[dcz-self]

Okay, I forgot that a variable can be bound to something that contains another variable and still needs to be unified. I'm not exactly sure what that means for tracking the constraints, though.

I just remembered: I wanted to track multiple constraints in-band as a tree structure, e.g. by having an "and" term, rather than a vector.

[fatho]

I just remembered: I wanted to track multiple constraints in-band as a tree structure, e.g. by having an "and" term, rather than a vector.

In this case, you'll get into trouble with backtracking. Right now, it's enough to remember which variables were set, and when reverting to a previous choice point, we can simply unset those variables.
But if you keep incrementally building up these constraint values, you need to actually restore the previous constraint, and can't simply set it to None.
That feels too invasive for the non-constraint code path, so I still think maintaining constraints separately is the way to go.

---

I don't really have the capacity to dive in deep, but I had a few more thoughts on going the constraints route for this (while keeping the underlying types of variables unchanged):

1. Generally, I think a constraint could be represented as a pair of a variable and a term, like so:

   pub struct Constraint {
       var: Var,
       constraint: TermId,
   }

2. Interpretation of constraint terms would be up to the resolver.
3. This representation allows us to maintain constraints in the SolutionState as a simple Vec<Constraint>, which makes it easy to include into the checkpoint mechanism for backtracking. When making a checkpoint, we simply remember the length of that constraint stack, and when backtracking, we drop all constraints that have been added since then.
4. A Vec<Constraint> has O(n) access for listing all constraints of a variable by itself, but I think it should be possible to maintain an indexing structure alongside it, if performance is an issue.
5. Resolvers would need a method in ResolveContext to push additional constraints.
6. The resolver trait would need another method that gets called whenever a variable is unified with a non-variable. At that point, it would then look at the constraints, and possibly push extra goals onto the goal stack. For example, if there's a constraint X < 4 for a variable X, and that variable is unified with some concrete value, then the resolver would generate a goal is_less(X, 4) which is simply a regular predicate that then gets checked later on. (Or alternatively, the resolver could immediately allow or reject the unification from within the hook, not sure what's better).
7. The resolver probably also needs a way of obtaining all constraints for a variable, in case one wants to implement a predicate to enumerate all possible values of a constrained variable.
8. All of this gets tricky once we start unifying variables with variables, because then we need to ensure that we also take the union of the constraints. For example, if we have the constraint X < 5 and Y > 2, and then later we unify X and Y, we then know that X > 2 must also hold. I don't have a good idea for this yet.

[dcz-self]

But if you keep incrementally building up these constraint values

Am I understanding correctly that the number of contraints would actually never drop until the variable is fully resolved?

The way I imagined this (and while ignoring backtracking which I know too little about) was that the resolver would unify constraints if possible at every variable unification. Then it would have enough information to unify X < 5, Y > 7, because it could be fed both at the time of unifying X and Y.

I'm not sure of the performance impact of that kind of eager resolution even without backtracking considerations. On the one hand, this could stop unsatisfiable branches early, on the other, the computations for the satisfiable ones could be repeated a lot on entering the same branch from dfferent contexts.

[fatho]

Am I understanding correctly that the number of contraints would actually never drop until the variable is fully resolved?

In the above idea, yes.

and while ignoring backtracking

Any solution to this problem cannot ignore backtracking though, and that's where a lot of the complexity arises from. If you have something like

foo(X) :- X #>= 4, bar(X).
foo(X) :- bar(X).

Then in the first branch of foo, we have a X >= 4 constraint that we carry along, but as soon as we backtrack and take the second branch, we must undo that constraint.

Keeping constraints separate makes that straightforward. If you eagerly resolve and combine constraints as you get them, you'll need some other strategy for undoing whatever you did to the constraints.

[dcz-self]

A quick-and-dirty idea: evaluate constraints eagerly, keep them in a tree:

constraint(A) · constraint(B) = constraint(ref(A), ref(B), A · B).

The resulting constraint A+B, referencing its ancestors, would be the one to undo when backtracking.

[dcz-self]

Thanks for taking the time to look at this.