Grappling with Infinity in Constraint Solvers

Summary

Grappling with infinity in constraint solversPublished November 17, 2019 by Chris PatuzzoIn 2016, I created a programming language called Sentient. Since then, I’ve had time to reflect and think about the language. This series is about that.Many constraint-satisfaction problems deal with infinity in some shape or form. Even rudimentary problems, like "Find two integers that sum to 10". Solutions include:(4, 6)(-7, 17)(-1953856112, 1953856122)In fact, there are infinitely many solutions and infinitely many pairs of integers to test. Here’s a Sentient program to solve this problem:int a, b;invariant a + b == 10;expose a, b;▲A Sentient program to find integers that sum to 10This article is about Sentient, but many of the concepts apply to constraint solvers in general.We can run this with the --number 0 option, to continuously find solutions:▲Finding multiple solutions with SentientWhen Sentient returns {}, it has exhausted the search space and can’t find any more solutions.After a few seconds this program terminates which seems wrong. Why should a problem that has infinitely many solutions ever terminate? Shouldn’t it run forever?The simple answer is that integers in Sentient aren’t really integers as far as the mathematical definition is concerned. Their magnitude is limited by how many bits represent them. By default this is 8 but can be specified, e.g. int9, int32In many cases this is fine. We can pick a number of bits that’s ‘big enough’ and not worry about it. But other times it’s not fine. We often want to start small and work our way up to larger representations, but that means restarting the program each time.For some problems, solutions are extremely rare (or non-existent) and it could take weeks or months for Sentient to find one. In these cases, it makes sense to start with small representations and progressively rule our search spaces of increasing size.Unfortunately, when a program is restarted, we lose its progress. Regions that were already explored are...