This paper presents an improved version-denoted FAST93-of our method FAST which proves the existence or nonexistence of a solution for a numerical constraint system (S') over a finite and discrete domain D. From a starting point in D, algorithm FAST93 generates a finite sequence of points in D, until either the last point satisfies the system of constraints (S'), or the associated domain F(S') is proved to be empty. In FAST93, each element of this sequence is obtained by solving partially an integer linear programming problem; in case of emptiness of the domain F(S'), only the last problem is solved exactly. Each integer linear program consists in optimizing a positive linear combination of the set of constraints violated by the previous point in the sequence, over the other constraints. Moreover we specify the 0-1 algorithmic tools of a specific version of algorithm FAST93 devoted to the exact solution of the Satisfiability problem (SAT). Comparisons with Hooker-Fedjki’s algorithm over their SAT instances, and with Davis-Putnam’s algorithm over regular combinatorial instances, show the efficiency of our method as far as CPU time is concerned.
