This paper describes how to build a (bounds consistent) global propagator for difference constraints that treats them all simultaneously, and shows how to explain propagations by a global difference constraint propagator, in order to use it within a lazy clause generation solver.
Abstract
Difference constraints of the form $x - y \leq d$ are well studied, with efficient algorithms for satisfaction and implication, because of their connection to shortest paths. Finite domain propagation algorithms, however, typically do not make use of these algorithms, and treat each difference constraint as a separate propagator. Propagation does guarantee completeness of solving, but can be needlessly slow. In this paper we describe how to build a (bounds consistent) global propagator for difference constraints that treats them all simultaneously. SAT modulo theory solvers have included theory solvers for difference constraints for some time. While a theory solver for difference constraints gives the basis of a global difference constraint propagator, we show how the requirements on the propagator are quite different. Crucially, we show how to explain propagations by a global difference constraint propagator, in order to use it within a lazy clause generation solver. We give experiments showing that treating difference constraints globally can substantially improve on the standard propagation approach.
A set of reformulation rules are proposed that allow the use of half-reification of a global constraint with any CP solver that supports the “normal” global constraint propagator, and expand the range of available solvers and constraint models that can be used in XCP techniques or for solving CSPs with compound constraints.
Ignace Bleukx, Hélène Verhaeghe, Dimos Tsouros et al.· Journal of Artificial Intell...· 1 citation
While the integration of linear constraints has significantly expanded the reach of Answer Set Programming (ASP), existing hybrid solvers often rely on disparate semantic underpinnings that lack a unified logical foundation. We address this gap by introducing a many-sorted variant of the Bound-founded Logic of Here-and-There (HTb), providing a versatile framework capable of characterizing equilibrium models across a wide spectrum of alternative semantics for extensions of ASP with linear constraints. We apply this framework to the setting of difference constraints, focusing on the semantic characterization of clingo[DL]. Central to our approach is the formalization of foundedness for numeric variables. By investigating how different hybrid systems - such as clingo[DL], clingcon, and flingo - justify constraint atoms, we uncover the semantic roots of their varying behaviors. This investigation results in a single, consistent framework that not only formalizes the foundations of current systems like clingo[DL] but also facilitates the rigorous study of program simplifications and the future integration of diverse semantic principles.
Pedro Cabalar, Jorge Fandinno, Nicolas Rühling et al.· Electronic Proceedings in Th...· 0 citations
This work presents the first systematic analysis of how leading LCG solvers maintain their SAT encodings, based on source-code inspection and developer correspondence, and proposes a native CDCL framework for CP, replacing SAT literals with atomic constraints, enabling conflict analysis, nogood learning, and nogood propagation directly at the CP level.
The top-down solver TD is a generic fixpoint algorithm that can be used to compute partial post-solutions of equation systems for abstract interpretation. We consider two extensions of the TD to deal with infinite strictly ascending chains. For the TD extended with warrowing, we formally prove that it always returns partial post-solutions, while for the TD extended with widening and narrowing in phases, we prove termination provided that the set of unknowns is finite. By proving the equivalence of the two extensions, we deduce the total correctness of both solvers. For the equivalence to hold, we in particular assume the equation system to have right-hand sides that are both monotonic and have monotonic dependencies. We demonstrate with counterexamples that the violation of any of the assumptions may compromise the equivalence. All proofs have been formalized using the interactive theorem prover Isabelle.
Sarah Tilscher, Alexandra Graß, Helmut Seidl et al.· Journal of automated reasoni...· 0 citations
This paper aims to provide an overview of techniques in termination analysis for programs with numerical variables and transitions defined by linear constraints. This subarea of program analysis is challenging due to the existence of undecidable problems, and this paper systematically explores approaches that mitigate this inherent difficulty. These include foundational decidability results, the use of ranking functions and disjunctive well-founded transition invariants. The paper also discusses non-termination witnesses, used to prove that a program will not halt. The authors examine the algorithmic and complexity aspects of these methods, showing how different approaches offer a trade-off between expressive power and computational complexity. The paper does not discuss how termination analysis is performed on real-world programming languages, nor does it consider more expressive abstract models that include non-linear arithmetic, probabilistic choice or term rewriting systems.
Amir M. Ben-Amram, S. Genaim, Joël Ouaknine et al.· Foundations and Trends® in P...· 1 citation
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
