Sentient: Der Umgang mit Unendlichkeit in Constraint-Solvern

Dieser Artikel befasst sich mit den Herausforderungen, die sich bei der Behandlung von Unendlichkeit in dem Constraint-Solver Sentient stellen. Sentient ist eine Programmiersprache, die Constraint-Erfüllungsprobleme löst, indem sie diese in boolesche Gleichungen übersetzt. Da ganze Zahlen in Computern mit einer endlichen Anzahl von Bits dargestellt werden, kann Sentient nicht direkt mit mathematisch unendlichen ganzen Zahlen umgehen. Der Autor schlägt eine Lösungsmethode basierend auf Approximation vor, indem er die Bitgröße von ganzen Zahlen schrittweise erhöht, um den unendlichen Raum anzunähern. Der Artikel diskutiert die Nutzung des inkrementellen SAT-Solvers IPASIR zur Steigerung der Effizienz und Vermeidung redundanter Suchen. Er untersucht auch die Erweiterung dieses Ansatzes auf komplexere Szenarien, wie z. B. die Behandlung von Arrays und Optimierungsproblemen, und geht schließlich auf die Möglichkeit ein, dass Sentient zukünftig Turing-vollständig werden könnte.