Half-checking propagators

This paper has now been published at ModRef 2020. Please see the updated post that includes a video presentation.

The paper Half-checking propagators by Mikael Z. Lagerkvist and Magnus Rattfeldt is now available from arXiv. This post summarizes the paper and gives some context on it. The paper is available on my research page.

A New PDF

The paper has not been accepted to a peer-reviewed venue so the most correct way to refer to it is, as Randall Munroe says in the above comic, a new pdf. Still, we think that the paper has some interesting ideas, and we want to share it with anyone interested.

The main problem with the paper currently is that we do not have enough compelling evidence that the techniques that we propose are useful. It is, as we often say, future work…

With that said, lets dive in to what the paper is about.

Idea: What if propagators need not be correct

Core to constraint programming systems is the idea of a propagator that removes values for variable domains that are in no solution to the propagators constraint. The main idea we started with is what would happen if a propagator was allowed to remove value that are also in solutions to the constraint!

The paper develops the theory and implications of allowing such propagators. In a normal system, there are many requirements on a propagator to ensure that the system works as intended. For our case, we could essentially remove all but a single requirement, namely

if a propagator indicates that something is a solution, then it is a solution.

This is related to the normal requirement that a propagator is correct, which is that a propagator identifies something as a solution if and only if it is a solution. Since we only retain half of the property, we called it half-checking.

Incompleteness, and regaining completeness

There are many types of incomplete solving methods for combinatorial (optimization) problems, such as local search, Large-Neighborhood Search, and streamliner constraints. Half-checking propagators is the first time, as far as we are aware, that incompleteness has been lifted into the core of a propagation solver, the propagators themselves.

Naturally, when solving a problem the user may want completeness. We can combine an incomplete version of the problem using half-checking propagators with a complete version using only normal propagators in a portfolio solver. A nice benefit is that since the system can use the same infrastructure for both the complete and the incomplete search, it is easier to engineer sharing of certain things, such as objective bounds and globally valid no-goods, compared to when integrating different systems in a portfolio.

Note that the idea of combining an incomplete search and a complete search is not new, and is for example a core part of the IBM ILOG CP Optimizer system.

Using half-checking propagators in a system

The natural implication is of course that solving problems with half-checking propagators is no longer a complete solution method: we may drop solutions. However, having half-checking propagators have many more implications, a few being

• All no-goods are not globally valid in a portfolio search. A no-good generated in a search using half-checking propagators is itself incomplete, since it may rule out a portion of the tree with a non-explored solution.
• In a lazy clause generation solver, the explanations generated have the same issue as no-goods, they may not be globally valid in a portfolio search.
• Testing becomes much harder, since there are fewer properties that can be used for testing.

Examples of half-checking propagators

We identified three general techniques for designing half-checking propagators

• Dominating solutions
• Heuristic bounds
• Heuristic solutions

For all three techniques, we developed a half-checking propagator for the cost-circuit constraint based on removing crossing lines, computing bounds inspired by Christofides algorithm, and analyzing 1-trees respectively. The details of the algorithms are best viewed in the paper.

Experimental evaluation showed that we performed a lot of additional propagation over standard cost-circuit propagation, and the three propagators had complementary pruning. Unfortunately, the pruning our propagators added did not translate to large gains when solving TSP instances. A large part may be problems that we found with trying to avoid some postings of no-goods across assets in a Gecode portfolio solver.

Implementation

The implementation is done in C++17 and uses the Gecode constraint programming system. The implementation is available on GitHub.

Side-track: A Variant of STR for R-tree construction

For implementing one of the propagators, we needeed a geometric look-up index for all the edges in a graph to speed up computation of crossing edges. We used an R-tree for this, and based our creation on the well-known STR (Sort-Tile-Recursive) construction. Standard STR doesn’t work very well for edges in a complete graph, since many of the edges have bounding boxes that cover a lot of the graph, making them potentially intersect with most other edges.

In order to handle the long edges, we modified STR to first sort on width and then on max x-position (and height and max y-position respectively). This batches up long/large edges on one side of the tree, while allowing for better filtering of sub-trees on the other side. This change led to a small but significant speed-up for look-ups in the tree, and we think may be useful whenever some of the elements to put in an R-tree may be large.

For implementation simplicity, we also changed the algorithm so that it subdivides into two buckets each time, and thus does multiple sorting passes. This costs more on construction, but not signifcantly so in our experience.

Our spatial index implementation is available on GitHub.

Reflections

The idea is naturally appealing, and we had a a lot of fun developing it. Unfortunately, we hit two main roadblocks in developing the idea

• In Gecode, portfolio solving (naturally) assumes all no-goods are valid for all assets. This turned out to be hard to fix, and is on-going work.
• While theoretically interesting and with demonstrated added pruning over the standard propagator, we could not show improved TSP solving.

We plan to continue investigating the potential of half-checking propagators, with the goal of proving that they are indeed a new and useful tool when designing constraint programming solutions.