feat(pumpkin-solver): Implement consistency checker infrastructure

[maartenflippo]

A proper implementation of consistency checkers (see #383), with lessons learned from #374.

TODO

• Strong consistency
  • Bounds consistency
  • Domain consistency
• Weak consistency
  • Bounds consistency
  • Domain consistency
• Implement checkers for the following propagators (in order of importance, to validate the new API design):
  • Multiplication
  • Nogood
  • Reified
  • Linear less equal
  • Binary equal
  • Maximum
  • Absolute value
  • Cumulative
  • Disjunctive
  • Hypercube linear
• Merge refactor(pumpkin-solver): PropagatorConstructor::create now returns event registrations #456

[EmirDe]

Following up on our discussion from Friday:

(this is a long post, and some of the things are interconnected. It might be best to discuss it instead of text.)

Support generator

Conceptually, it would make sense that propagators generate propagation/retention certificates, since the propagator is to prove that it is working correctly.

Currently, the propagator generates propagation certificates as explanations, good. But retention certificates are attached to inference checkers through the support generator trait.

I think we could have inference checkers only do inference checking, and leave the retention certificates to the propagator. This also makes sense since the propagator may use some internal data structures / algorithms to construct the certificates. But in any case, generating retention certificates should be an immutable operation so the trace does not change.

Interface for inference and retention checkers

I like the interface for inference checkers, because it is reasonably decoupled from the solver, e.g., it has its own variables as input to which the solver translates to.

I think the retention checker could use a similar interface. Now the retention checkers rely on the internal solver details through the scope and local ids, but probably they could use the same as the inference checkers. This way we could have the retention checkers more decoupled from the solver.

Reified propagator wrappings and different way of registering variables for propagators

I understand that we have special consideration for the reified propagator, e.g., the constructor context has pending_inference_checkers because of the reified propagator.

Is the main problem that we do not know how many local ids will the underlying propagator make, which makes it difficult for the generic reified propagator to understand which local id it will take?

I think we could consider a slightly different way of registering variables for propagators, which could solve this issue.

Currently we ask propagators to, within the constructor, call "context.register". Instead, maybe we could do the following: as part of the return value of the propagator constructor, we return the propagator AND a mapping 'variable -> (local id, domain_event)'. Essentially, the propagator constructor tells the solver how it renamed the variables locally. The solver then registers the variables for watching after creating the propagator.

This might be a bit cleaner, and it will be harder to forget to register variables, since registering variables is part of the output of the create function. It would also help with the reified propagator situation, since then we would not need to wrap checkers (but see point below, very related), simply the create function will be called of the underlying propagator, and then the reified propagator can process that and see which local id it needs to select for the reified variable.

Creating propagators together with checkers

In the current design, the user is responsible for calling "add checkers" functions, and there is a lot of flexibility. I am thinking we might be able to streamline this a bit.

Ideally, the propagator constructor returns an initialised propagator, but also returns inference checker(s) and a retention checker, e.g., (propagator, list of inference checkers, list of retention checkers, possibly also a mapping from variables to local ids and their domain events). This way it is clearer that checkers are core parts, and not optional. Now this seems to be difficult to do fully, but maybe we can still come up with something in this direction, see below.

First observation is that perhaps the propagator and both checkers should take as input the PropagatorArgs struct. Conceptually this makes sense, since those input define what the propagator is, which is clearly what the checkers care about.

Being sure the correct number of checkers is returned: We discussed it, but after looking through the code again, I get the impression that each InferenceCode must have exactly one inference checker. We could ask the propagator to request inference codes from the context (instead of having propagators be able to make inference codes themselves), and this way we would know exactly how many checkers the propagator needs to return.

Specifying the retention checker: the propagator specifies the checker using an enum, which has the types (that may have additional fields) to specify which type of consistency is guaranteed (domain/bounds weak/regular consistency, or custom). This is a bit tricky because I am not entirely sure how to define consistency for a propagator if it can have multiple inferences or constraints.

Should propagators define consistency for each individual variable? Say these variables are going to be bound-consistent, and these domain-consistent?

Is it a fair assumption that a propagator has one consistency type per constraint tag it uses? This seems reasonable to me for bound/domain consistent propagators. For weakly consistent ones, it seems to me that retention consistency is actually defined on the level of an inference code and not on a constraint.

Assuming one retention per constraint tag, the propagator specifies the consistency as an enum with several types (with each type having its own fields). These enum types dictate how feasible solutions are going to checked (using one of the inference checkers) or how the infeasibility function will be used to check consistency (see below for infeasibility function). And then there is a fifth option ‘custom’ which then allows for any type of consistency checking that we have not yet covered with the ‘standard’ options.

Infeasibility function interface

For weakly consistent propagators, we use the infeasibility function to check whether it is consistent. Since we already learned that this can be a major bottleneck, then we can design the interface to allow the option for more efficient checking.

The infeasibility function could have this type of workflow (functions):
“Initialisation” function: it takes as input variables and their domains (like our inference checkers do now). The function can do some precomputation to make checking easier, or it can keep this as simple as copying the domains.
For cumulative, this could mean computing the timetable. For circuit, it could mean colouring nodes in a way that nodes within the same chain have the same colour.
“Is this value weakly supported for this variable?” function. Returns true or false.
For cumulative, since the timetable is computed, it is easy to check consistency. For circuit, simply checks if the edge is between the same colour of nodes.

(The alternative to the above is to have a checker with no initialisation apart from copying the domain, so then checking needs to recompute things. This is more trustworthy but too slow potentially.

The solver would simply initialise the function, and ask for each relevant value.

Contexts for checkers?

Minor point: do we want checkers to have "contexts" instead of receiving a list of arguments? We use this design everywhere so I am wondering if we should also use it for checkers.

[maartenflippo]

Support generator

I think we could have inference checkers only do inference checking, and leave the retention certificates to the propagator. This also makes sense since the propagator may use some internal data structures / algorithms to construct the certificates. But in any case, generating retention certificates should be an immutable operation so the trace does not change.

This could also work. As long as something implements the SupportGenerator trait, it can work. So we can have the propagator itself implement it, and pass a cloned version of itself as a support generator. Right now you are right the PropagatorChecker implements both the inference checker and support generator (or the more general retention checker trait).

Interface for inference and retention checkers

I like the interface for inference checkers, because it is reasonably decoupled from the solver, e.g., it has its own variables as input to which the solver translates to.

I think the retention checker could use a similar interface. Now the retention checkers rely on the internal solver details through the scope and local ids, but probably they could use the same as the inference checkers. This way we could have the retention checkers more decoupled from the solver.

We could extract a trimmed-down version of our ReadDomains trait here. It exposes methods such as lower_bound(var), upper_bound(var), etc. The retention checker can then receive an implementation of that trait, thereby decoupling our solver state from the library.

The only thing that is not clear to me is how we would deal with views. I suppose the CheckerVariable trait already handles some of that. So we may be able to expand that interface.

In general, I think it would be amazing to extract the retention checkers into a separate library. Just as with everything I do in pumpkin, I want the code to be good and re-usable, which is no different here. However, at the moment I do have to make choices with my time, and as I raised in the meeting as well, especially in the next two months I feel that extracting the retention checkers would just be one of the lowest priority things for me. That means we could end up blocking this PR, since it would require an interface change. So we would have to discuss what the pragmatic way forward is on this.

Reified propagator wrappings and different way of registering variables for propagators

Currently we ask propagators to, within the constructor, call "context.register". Instead, maybe we could do the following: as part of the return value of the propagator constructor, we return the propagator AND a mapping 'variable -> (local id, domain_event)'. Essentially, the propagator constructor tells the solver how it renamed the variables locally. The solver then registers the variables for watching after creating the propagator.

I suppose this can work as well. For e.g. the nogood propagator, which does not register anything in the constructor, this mapping can be empty. I agree it is also much more composable than the interface we have now. For this I would suggest doing a separate PR first, though. It would be better to review this change in isolation.

Being sure the correct number of checkers is returned: We discussed it, but after looking through the code again, I get the impression that each InferenceCode must have exactly one inference checker.

This is not true. I remind you of the example where a clausal encoding of a constraint that introduces $n$ clauses will create $n$ inference checkers with the same inference code. Currently, we accept an inference if there exists a checker among those $n$ that accepts it. Another example of this is the way we model $Ax = b$ constraints as $Ax \le b \land Ax \ge b$, which introduces two checkers using the same inference code.

Upon reflection, I suppose it is true for the inference checkers in one propagator during the constructor. In the example of the clausal encoding, the inference checkers are created when the constraint is added to the propagator, but the constructor for the clausal propagator does not register any. Similarly, in the example of $Ax = b$, each linear inequality propagator returns one inference checker for one inference code. In the solver there may be multiple checkers per inference code.

We could ask the propagator to request inference codes from the context (instead of having propagators be able to make inference codes themselves)

We actually used to have this design. Yet we moved away from it because we gained little from it, whilst making it difficult to debug (due to the indirection), and we had to always carry the mapping inference_code -> (constraint_id, label) everywhere.

Perhaps we will land on a preferable API that would benefit from from requesting inference codes, in which case we can revert the change. One benefit immediately is that the codes would implement Copy again, making them easier to work with (now they only implement Clone).

Creating propagators together with checkers

Is it a fair assumption that a propagator has one consistency type per constraint tag it uses? This seems reasonable to me for bound/domain consistent propagators. For weakly consistent ones, it seems to me that retention consistency is actually defined on the level of an inference code and not on a constraint.

I think this is not entirely true. E.g. if we post a time-table retention checker and an edge-finding retention checker for cumulative, even though the reasoning is not comparable, at fixed point both would need to accept the domains as they are for the consistency check to pass.

But you are right that it means there is a many to one relationship between consistency checkers and constraint tags, which is already supported to handle decompositions.

These enum types dictate how feasible solutions are going to checked (using one of the inference checkers) or how the infeasibility function will be used to check consistency (see below for infeasibility function)

I do not see what the enum version gives us that is not already afforded by the current design. The enum variants will just be implementations of the RetentionChecker trait. And now there is no need for a Custom variant, since all retention checkers are equal.

Infeasibility function interface

The infeasibility function could have this type of workflow (functions):
“Initialisation” function: it takes as input variables and their domains (like our inference checkers do now). The function can do some precomputation to make checking easier, or it can keep this as simple as copying the domains.

This is a great idea. I assume you intend that we call the initialization function once per fixed point, but that state can then be re-used for subsequent calls to determine whether a value is supported?

The alternative to the above is to have a checker with no initialisation apart from copying the domain, so then checking needs to recompute things. This is more trustworthy but too slow potentially.

I would assume this separation is worth it, since we know from experience that it is still important to get somewhat deep into the search tree to be confident in the propagators.

Contexts for checkers?

Minor point: do we want checkers to have "contexts" instead of receiving a list of arguments? We use this design everywhere so I am wondering if we should also use it for checkers.

I personally don't think so. The checkers take only few arguments, which means it is much clearer to spell those arguments out. The contexts make sense where we need many arguments (e.g. the resolution context combines so many fields that they would be impractical as individual arguments).

[ImkoMarijnissen]

About halfway through, but these are some intermediate comments.

Overall, I like the interface, though I think it is difficult to understand all of the different types (which is unavoidable with how general we want it to be). Perhaps we should add a dedicated page to all the different types in the checkers and how they interact with one another.

[ImkoMarijnissen]

I would argue that this is a bit too vague

[ImkoMarijnissen]

Couldn't this be implemented using the dyn_clone::clone_trait_object! macro?

[ImkoMarijnissen]

Maybe add a small comment what this is doing; spacing is off as well

[ImkoMarijnissen]

Docs

[ImkoMarijnissen]

Seems like we do not need this field when we have enqueued? Is it just to prevent the iteration complexity of a bitset?

[ImkoMarijnissen]

I think this is one example where it would be nice to have either a Result with an error enum or just an enum to provide this info directly

[ImkoMarijnissen]

Could suffer from floating point inaccuracies; should we use f32::EPSILON for this comparison (similar to np.isclose)?

[ImkoMarijnissen]

I would rewrite this documentation, it is not clear what the trait itself represents

[ImkoMarijnissen]

Could add information about what it means to be unsupported

[ImkoMarijnissen]

Just out of curiosity; these could not be derived?

[maartenflippo]

Summary of the meeting with @EmirDe and @ImkoMarijnissen:

Most of the interface changes proposed by @EmirDe are good, and we will make the necessary changes. A few things of note:

• I will try to figure out a design where propagators can implement the SupportGenerator interface. It could be beneficial to access the propagator state when creating supports. In addition, the retention checker (and support generator as well) need to receive the constraint ID to allow compound propagators to identify which constraint they are checking.
• Extracting the retention checkers into the checking crate has the lowest priority. If it is easy, great. Otherwise, I will create an issue to document that it is a goal, but it will have to be picked up in the future.

Sketch of part of the design:

/// Pumpkin

trait Propagator:
    fn propagate(...):

trait PropagatorConstructor:
    fn create(...) -> (impl Propagator, Mapping):
        let mapping = Mapping::new()
            .add(localid1, &self.a)
            .add(localid1, &self.b)
            .build()
        

/// Checking lib

struct LocalId(...);

trait Domains:

trait SupportGenerator<D>:
    fn support(&self, local_id, value, constraint_tag, ctx: D) -> Support<>:
        // hello

DomainConssitency<D>:
    fn check(generator: &impl SupportGen, ctx: D):
        for all vars
            for all values
                support_gen give me a support for var = val