COMPUTER-IMPLEMENTED METHOD FOR SOLVING SETS OF LINEAR ARITHMETIC CONSTRAINTS MODELLING PHYSICAL SYSTEMS

Abstract

A computer-implemented method for solving sets of linear arithmetic constraints modelling physical systems by programmed execution of mathematical operations in a processor unit, wherein the programmed execution of mathematical operations decide, given a set of constraints S, whether S has any solution, and if so, find one or more of them.

Claims

1. A computer-implemented method for solving sets of linear arithmetic constraints modelling physical systems, the method comprising using a computer processor unit performing a programmed execution of mathematical operations wherein, being {x.sub.1 . . . x.sub.n} a set of variables, said linear arithmetic constraints are expressions of the form a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n≦a.sub.0, in which the coefficients a.sub.0 . . . a.sub.n are integer numbers, wherein a solution for a set of linear arithmetic constraints S is an expression Sol mapping each variable x of {x.sub.1 . . . x.sub.n} to an integer value Sol(x) such that all constraints are satisfied, that is, for each constraint of the form a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n≦a.sub.0 in S, the integer number a.sub.1.Sol(x.sub.1)+ . . . +a.sub.n.Math.Sol(x.sub.n) is smaller than or equal to a.sub.0; wherein the following notions/terms are used: bound (constraint with a single variable x, that can be written as lower bounds a≦x or upper bounds x≦a) where a is an integer number the negation of a lower bound a≦x is the upper bound x≦a−1 and the negation of an upper bound x≦a is the lower bound a+1≦x; a lower bound a.sub.1≦x and an upper bound x≦a.sub.2 are called conflicting if a.sub.1>a.sub.2; a lower bound a≦x is called new in a given set of bounds B if there is no lower bound a′≦x in B with a′≧a, and an upper bound x≦a is called new in a given set of bounds B if there is no upper bound x≦a′ in B with a′≦a, and a variable x is called defined to the value a in a given set of bounds B, if B contains the bounds a≦x, and x≦a; and a monomial is an expression of the form a x, where a is an integer or a rational number and x is a variable; it called negative if a is negative and positive otherwise; propagation: If C is a linear arithmetic constraint of the form a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n≦a.sub.0 where: the subset of positive monomials of {a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n} is {ax, c.sub.1y.sub.1, . . . , c.sub.py.sub.p}; the subset of negative monomials of {a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n} is {d.sub.1z.sub.1, . . . , d.sub.qz.sub.q}; R is a set of bounds {l.sub.1≦y.sub.1, . . . , l.sub.p≦y.sub.p, z.sub.1≦u.sub.1, . . . , z.sub.q≦u.sub.q}; u is the largest integer such that u≦(a.sub.0−c.sub.1l.sub.1− . . . −c.sub.pl.sub.p−d.sub.1u.sub.1− . . . −d.sub.qu.sub.q)/a, then C and R propagate the upper bound x≦u; If C is a linear arithmetic constraint of the form a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n≦a.sub.0 where: the subset of positive monomials of a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n is {c.sub.1y.sub.1, . . . , c.sub.py.sub.p}; the subset of negative monomials of a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n is {ax, d.sub.1z.sub.1, . . . , d.sub.qz.sub.q}; R is a set of bounds {l.sub.1≦y.sub.1, . . . , l.sub.p≦y.sub.p, z.sub.1≦u.sub.1, . . . , z.sub.q≦u.sub.q}; l is the smallest integer such that l≧(a.sub.0−c.sub.1l.sub.1− . . . −c.sub.pl.sub.p−d.sub.1u.sub.1− . . . −d.sub.qu.sub.q)/a, then C and R propagate the lower bound l≦x, a propagation record is a triple (b, R, C) where b is a bound C is a linear arithmetic constraint and R is a set of bounds such that C and R propagate b, then R being termed the reason set of b and C being termed the reason constraint of b; in a special kind of propagation record called a decision, the components R and C are null, a propagation stack is a data structure having capabilities of a standard stack data structure whose elements are propagation records, with standard operations for pushing and popping elements and for inspecting the topmost element and in addition the nonstandard capability of inspecting non-topmost elements; a bound b is said to be in a propagation stack B if b is the first element of some propagation record of B; similarly a set of bounds R is said to be in a propagation stack B if R is a subset of the set of all first elements of the propagation records of B, a constraint C is said to be learned when it is added to the set of linear arithmetic constraints S; wherein said programmed execution of mathematical operations of the method being automatically performed, by the following steps: 1a) receiving by the computer processor unit the set of linear arithmetic constraints S; 1b) creating using the computer processor unit a propagation stack B that is initially empty; being said propagation stack B stored in the computer processor unit and being automatically modified using the computer processor unit by considering the set of linear arithmetic constraints S by implementing the subsequent steps; 1c) if there is a linear arithmetic constraint C in S and a set of bounds R in B such that C and R propagate a bound b that is new in B, then pushing the propagation record (b, R, C) on top of the stack B; and iterating this pushing while possible; 1d) treating four non-overlapping cases using the computer processor unit: 1d1) if there is no conflicting pair of bounds in B and if, for all i in {i . . . n} the variable x.sub.i is defined in B to a value a.sub.i, then halt outputting the solution Sol such that Sol(x.sub.i)=a.sub.i for each i in i . . . n; 1d2) if there is no conflicting pair of bounds in B and at least one variable is not defined in B, then a propagation record (d, −, −) is pushed on top of B such that d is new in B and d is not conflicting with any other bound in B, said bound d and the propagation record (d, −, −) being termed a decision, and then return to step 1c); 1d3) if there is at least one conflicting pair of bounds b.sub.1 and b.sub.2 in B such that there is no decision in B below b.sub.1 nor below b.sub.2 then halt outputting “no solution”; 1d4) if there is at least one conflicting pair of bounds b.sub.1 and b.sub.2 in B such that there is at least one decision located in B below b.sub.1 or below b.sub.2 then a conflict analysis is performed based on the current propagation stack B and as a consequence of which firstly a number of topmost elements of the propagation stack B are popped and after that a new bound with an associated reason set and reason constraint is pushed on top of the stack and a new linear constraint C is learned, and then return to step 1c).

2. The method of claim 1 wherein said conflict analysis further uses a data structure called the CSS, Conflicting Subset, a set data structure storing a subset of the bounds of B, and another data structure called the CC, Conflicting Constraint, wherein the following notions are used: if C.sub.1 is a linear arithmetic constraint a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n≦a.sub.0, and C.sub.2 is a linear arithmetic constraint b.sub.1x.sub.1+ . . . +b.sub.nx.sub.n≦b.sub.0, then a cut between C.sub.1 and C.sub.2 is a linear arithmetic constraint c.sub.1x.sub.1+ . . . +c.sub.nx.sub.n≦c.sub.0 such that c and d are positive natural numbers and c.sub.i=c.Math.a.sub.i+d.Math.b.sub.i for each i in 0 . . . n; and if c.sub.j=0 for some j in 1 . . . n then this cut is said to eliminate the variable x.sub.j, the method comprising the following steps: 2a) if the conflicting pair of bounds is {b.sub.1, b.sub.2} such that b.sub.2 is located in the stack B above b.sub.1, then initializing the CSS to {b.sub.1, b.sub.2} and initializing the CC to the reason constraint of b.sub.2; 2b) if b is the bound in the CSS that is located in the stack B closest to the top of B, then 2b1) popping bounds from the top of stack B until there are no decisions above b in B; 2b2) removing b from the CSS and inserting into the CSS the reason set associated with b; 2b3) performing a cut between the current CC and the reason constraint of b, in such a way that the variable of b is eliminated, thus obtaining a new CC; and if no such a cut exists, then the CC remains unchanged; 2c) if after popping k bounds including at least one decision from the stack B there is a set of bounds R in B such that CC and R propagate a bound b that is new in B, then popping k bounds from the stack B and pushing b on top of B with associated reason set R and reason constraint CC, and halting the conflict analysis; 2d) if the CSS contains more than one bound that is located in B at the height of the topmost decision of B or above then going to step 2b); 2e) if the CSS contains exactly one bound b that is located in B at the height of the topmost decision of B or above: 2e1) if the CSS contains b as its unique element, then popping bounds from the stack B until B contains no decisions and after that pushing on the stack a new bound being the negation of b with an associated empty reason set and the final CC as its reason constraint; then this CC is learned, and 2e2) if the CSS contains more than one bound, then if b.sub.1 is the bound of the CSS different from b such that b.sub.1 is located in the stack B closest to the top of B, above exactly k decisions, then popping bounds from the stack B until B contains exactly k decisions and after that pushing on the stack a new bound being the negation of b, having this new bound as its associated reason set the result of removing b from the CSS, and the final CC as its reason constraint, and then learning this CC.

3. The method of claim 1 wherein said conflict analysis further uses a data structure called the CSS, Conflicting Subset, a set data structure storing a subset of the bounds of B, and another data structure called the CC, Conflicting Constraint, wherein the following notions are used: if C.sub.1 is a linear arithmetic constraint a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n≦a.sub.0, and C.sub.2 is a linear arithmetic constraint b.sub.1x.sub.1+ . . . +b.sub.nx.sub.n≦b.sub.0, then a cut between C.sub.1 and C.sub.2 is a linear arithmetic constraint c.sub.1x.sub.1+ . . . +c.sub.nx.sub.n≦c.sub.0 such that c and d are positive natural numbers and c.sub.i=c.Math.a.sub.i+d.Math.b.sub.i for each i in 0 . . . n; and if c.sub.j=0 for some j in 1 . . . n then this cut is said to eliminate the variable x.sub.j, the method comprising the following steps: 3a) if the conflicting pair of bounds is {b.sub.1, b.sub.2} such that b.sub.2 is located in the stack B above b.sub.1, then initializing the CSS to {b.sub.1, b.sub.2} and initializing the CC to the reason constraint of b.sub.2; 3b) if b is the bound in the CSS that is located in the stack B closest to the top of B, then 3b1) popping bounds from the top of stack B until there are no decisions above b in B; 3b2) removing b from the CSS and inserting into the CSS the reason set associated with b; 3b3) performing a cut between the current CC and the reason constraint of b, in such a way that the variable of b is eliminated, thus obtaining a new CC; and if no such a cut exists, then the CC remains unchanged; 3c) if the CSS contains more than one bound that is located in B at the height of the topmost decision of B or above then going to step 3b); 3d) if the CSS contains exactly one bound b that is located in B at the height of the topmost decision of B or above: 3d1) if the CSS contains b as its unique element, then popping bounds from the stack B until B contains no decisions and after that pushing on the stack a new bound being the negation of b with an associated empty reason set and the final CC as its reason constraint; then this CC is learned, and 3d2) if the CSS contains more than one bound, then if b.sub.1 is the bound of the CSS different from b such that b.sub.1 is located in the stack B closest to the top of B, above exactly k decisions, then popping bounds from the stack B until B contains exactly k decisions and after that pushing on the stack a new bound being the negation of b, having this new bound as its associated reason set the result of removing b from the CSS, and the final CC as its reason constraint, and then learning this CC.

4. The method of claim 2, wherein in step 2d), even if the CSS contains zero or one bound located in B above a decision, being the topmost decision of B, then going to step 2b).

5. The method of claim 2, wherein after each application of step 2b) bounds of the form a≦x are eliminated from the CSS whenever a bound a′≦x with a′>a is in the CSS and bounds of the form x≦a are eliminated from the CSS whenever a bound x≦a′ with a′<a is in the CSS.

6. The method of claim 2, wherein in step 2b) instead of the reason set of b, a set of bounds R is computed and inserted in the CSS, with all elements of R being located below b in B and the reason constraint of b and R also propagating b.

7. The method of claim 2 wherein in step 1c) the reason set is not associated to b nor stored and in step 2b) a set of bounds R is computed and inserted in the CSS, with all elements of R being located below b in B and the reason constraint of b and R also propagating b.

8. The method of claim 1 wherein in step 1c) the linear constraint C is not associated to b and wherein in step 1d4) the conflict analysis is performed omitting steps 2b3) and 2c) involving the CC, and no new constraint is learnt.

9. The method of claim 1 wherein in step 1c) the iteration is performed non-exhaustively.

10. The method of claim 1 wherein the linear arithmetic constraints further include expressions of the form a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n≧a.sub.0, or a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n=a.sub.0, or a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n>a.sub.0, or a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n<a.sub.0 or combinations thereof, where the coefficients a.sub.0 . . . a.sub.n can be arbitrary rational numbers, sets of which are all expressible by sets S of linear constraints of the form b.sub.1x.sub.1+ . . . +b.sub.nx.sub.n≦b.sub.0, with integer coefficients b.sub.0 . . . b.sub.n so that the resulting set of constraints S has the same set of solutions

11. The method of claim 10 further comprising in order to find a solution Sol that minimizes the value of a.sub.1.Sol(x.sub.1)+ . . . +a.sub.n.Math.Sol(x.sub.n) for a given expression a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n, in a first iteration applying steps 1a) to 1e) of the method, and in successive iterations, while new solutions are found, applying steps 1a) to 1e) of the method with an additional constraint a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n≦a.sub.0 where a.sub.0 is a.sub.1.Sol(x.sub.1)+ . . . +a.sub.1.Math.Sol(x.sub.n)−1 and Sol is the solution found in the previous iteration.

12. The method of claim 10 further comprising in order to find a solution Sol that maximizes the value of a.sub.1.Sol (x.sub.1)+ . . . +a.sub.n.Math.Sol(x.sub.n) for a given expression a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n, in a first iteration applying steps 1a) to 1e) of the method, and in successive iterations, while new solutions are found, applying steps 1a) to 1e) of the method with an additional constraint −a.sub.1x.sub.1− . . . −a.sub.nx.sub.n≦a.sub.0 where a.sub.0 is −a.sub.1.Sol (x.sub.1)− . . . −a.sub.n.Math.Sol (x.sub.n)−1 where each time Sol is the solution found in the previous iteration.

13. The method of claim 2, wherein in step 2b) instead of popping and replacing the topmost bound b from the CSS another bound is popped and replaced by its reason set.

14. The method of claim 2 wherein in order to solve Mixed Integer Programs (MIPs), that is, to find a solution where a given subset I of the variables must take integer values and the remaining variables can take arbitrary rational values, it is proposed to use an arbitrary LP solver for finding a solution RSol minimizing the value of an expression a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n, where in RSol all variables are allowed to take rational values, outputting RSol as a solution and halting if RSol(x) is an integer for every variable x of I, and if no such a solution RSol exists, generating an infeasible subset using the LP solver and starting a conflict analysis.

15. The method of claim 14, wherein to perform said conflict analysis a data structure called the CSS, Conflicting Subset, a set data structure storing a subset of the bounds of B, and another data structure called the CC, Conflicting Constraint are used, wherein the following notions are used: if C.sub.1 is a linear arithmetic constraint a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n≦a.sub.0, and C.sub.2 is a linear arithmetic constraint b.sub.1x.sub.1+ . . . +b.sub.nx.sub.n≦b.sub.0, then a cut between C.sub.1 and C.sub.2 is a linear arithmetic constraint c.sub.1x.sub.1+ . . . +c.sub.nx.sub.n≦c.sub.0 such that c and d are positive natural numbers and ci=c.Math.a.sub.i+d.Math.b.sub.i for each i in 0 . . . n; and if c.sub.j=0 for some j in 1 . . . n then this cut is said to eliminate the variable x.sub.j, the method comprising the following steps: 15a) initializing the CSS to the subset of bounds of the infeasible subset, and initializing the CC to any other constraint of the infeasible subset; 15b) if b is the bound in the CSS that is located in the stack B closest to the top of B, then 15b1) popping bounds from the top of stack B until there are no decisions above b in B; 15b2) removing b from the CSS and inserting into the CSS the reason set associated with b; 15b3) performing a cut between the current CC and the reason constraint of b, in such a way that the variable of b is eliminated, thus obtaining a new CC; and if no such a cut exists, then the CC remains unchanged; 15c) if after popping k bounds including at least one decision from the stack B there is a set of bounds R in B such that CC and R propagate a bound b that is new in B, then popping k bounds including at least one decision from the stack B and pushing b on top of B with associated reason set R and reason constraint CC, and halting the conflict analysis; 15d) if the CSS contains more than one bound that is located in B up or above the topmost decision of B then going to step 15b); 15e) if the CSS contains exactly one bound b that is located in B up or above the topmost decision of B: 15e1) if the CSS contains b as its unique element, then popping bounds from the stack B until B contains no decisions and after that pushing on the stack a new bound being the negation of b with an associated empty reason set and the final CC as its reason constraint; then this CC is learned, and 15e2) if the CSS contains more than one bound, then if b.sub.1 is the bound of the CSS different from b such that b.sub.1 is located in the stack B closest to the top of B, above exactly k decisions, then popping bounds from the stack B until B contains exactly k decisions and after that pushing on the stack a new bound being the negation of b, having this new bound as its associated reason set the result of removing b from the CSS, and the final CC as its reason constraint, and then learning this CC.

16. The method of claim 14, wherein to perform said conflict analysis a data structure called the CSS, Conflicting Subset, a set data structure storing a subset of the bounds of B, and another data structure called the CC, Conflicting Constraint are used, wherein the following notions are used: if C.sub.1 is a linear arithmetic constraint a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n≦a.sub.0, and C.sub.2 is a linear arithmetic constraint b.sub.1x.sub.1+ . . . +b.sub.nx.sub.n≦b.sub.0, then a cut between C.sub.1 and C.sub.2 is a linear arithmetic constraint c.sub.1x.sub.1+ . . . +c.sub.nx.sub.n≦c.sub.0 such that c and d are positive natural numbers and ci=c.Math.a.sub.i+d.Math.b.sub.i; for each i in 0 . . . n; and if c.sub.j=0 for some j in 1 . . . n then this cut is said to eliminate the variable x.sub.j, the method comprising the following steps: 16a) initializing the CSS to the subset of bounds of the infeasible subset, and initializing the CC to any other constraint of the infeasible subset; 16b) if b is the bound in the CSS that is located in the stack B closest to the top of B, then 16b1) popping bounds from the top of stack B until there are no decisions above b in B; 16b2) removing b from the CSS and inserting into the CSS the reason set associated with b; 16b3) performing a cut between the current CC and the reason constraint of b, in such a way that the variable of b is eliminated, thus obtaining a new CC; and if no such a cut exists, then the CC remains unchanged; 16c) if the CSS contains more than one bound that is located in B up or above the topmost decision of B then going to step 16b); 16d) if the CSS contains exactly one bound b that is located in B up or above the topmost decision of B: 16d1) if the CSS contains b as its unique element, then popping bounds from the stack B until B contains no decisions and after that pushing on the stack a new bound being the negation of b with an associated empty reason set and the final CC as its reason constraint; then this CC is learned, and 16d2) if the CSS contains more than one bound, then if b.sub.1 is the bound of the CSS different from b such that b.sub.1 is located in the stack B closest to the top of B, above exactly k decisions, then popping bounds from the stack B until B contains exactly k decisions and after that pushing on the stack a new bound being the negation of b, having this new bound as its associated reason set the result of removing b from the CSS, and the final CC as its reason constraint, and then learning this CC.

17. The method of claim 1 wherein the coefficients of the linear constraints are rational or floating point numbers and wherein in step 1 d4) the conflict analysis is performed using cuts where c and d are positive rational or floating point numbers.

Description

EXAMPLES

Example 1

[0112] This example involves the embodiment without reason constraints, without cuts and without learning new constraints. In this example, and in the following one, when a bound b in the stack B has exactly k decisions at or below it in B then b is said to belong to decision level (dl) k

[0113] Consider the following two constraints:

1x+1y+3z≦5

−1x−1y≦−11

[0114] In addition, there are six one-variable constraints stating that all three variables are between −10 and 10. Note that these six constraints propagate the first six bounds with empty reason sets. Below the stack is shown (depicted here growing downwards) after propagating the initial constraints, and taking and propagating three decisions:

TABLE-US-00001 bound reason set −10 ≦ x  { }  x ≦ 10 { } −10 ≦ y  { }  Y ≦ 10 { } −10 ≦ z .sup.  { }  z ≦ 10 { } 1 ≦ x {y ≦ 10} 1 ≦ y {x ≦ 10} z ≦ 1 {1 ≦ x, 1 ≦ y} 7 ≦ y decision  .sup. z ≦ −1 {1 ≦ x, 7 ≦ y} x ≦ 5 decision −1 ≦ z .sup.  decision x ≦ 1  {7 ≦ y, −1 ≦ z} 10 ≦ y  {x ≦ 1}  x ≦ −2 {10 ≦ y, −1 ≦ z}

[0115] Now there is a conflict with initial CSS {1≦x, x≦−2}.

[0116] In the first conflict analysis step, x≦−2 is removed from the CSS and its reason set {10≦y, −1≦z}, inserted obtaining {1≦x, −1≦z, 10≦y}. Since this CSS contains more than one bound of the highest decision level (dl 3), 10≦y is also replaced by its reason, getting {1≦x, −1≦z, x≦1)}. Since there are still two bounds of dl 3, x≦1 is also replaced getting {1≦x, 7≦y, −1≦z}. After this, the conflict analysis process terminates, since this final CSS contains only one bound of dl 3, which in this case is the last decision itself, −1≦z.

[0117] The negation of −1≦z is z≦−2, which is added to dl 1 (the dl of 7≦y) with reason set {1≦x, 7≦y}. Altogether, a backjump is done to:

TABLE-US-00002 bound reason set −10 ≦ x  { }  x ≦ 10 { } −10 ≦ y  { }  y ≦ 10 { } −10 ≦ z .sup.  { }  z ≦ 10 { } 1 ≦ x {y ≦ 10} 1 ≦ y {x ≦ 10} z ≦ 1 {1 ≦ x, 1 ≦ y} 7 ≦ y decision  .sup. z ≦ −1 {1 ≦ x, 7 ≦ y}  .sup. z ≦ −2 {1 ≦ x, 7 ≦ y}

[0118] After one more propagation and two further decisions and their propagations, the following stack is obtained:

TABLE-US-00003 bound reason set −10 ≦ x  { }  x ≦ 10 { } −10 ≦ y  { }  y ≦ 10 { } −10 ≦ z .sup.  { }  z ≦ 10 { } 1 ≦ x {y ≦ 10} 1 ≦ y {x ≦ 10} z ≦ 1 {1 ≦ x, 1 ≦ y} 7 ≦ y decision  .sup. z ≦ −1 {1 ≦ x, 7 ≦ y}  .sup. z ≦ −2 {1 ≦ x, 7 ≦ y} −2 ≦ z .sup.  decision x ≦ 4  {7 ≦ y, −2 ≦ z} 4 ≦ x decision y ≦ 7  {4 ≦ x, −2 ≦ z}  .sup. z ≦ −2 {4 ≦ x, 7 ≦ y}

[0119] It gives the solution where x=4, y=7 and z=−2, since all variables are fully defined to these values.

Example 2

[0120] Consider the following three constraints:

C.sub.0:+1x−3y−3z≦1

C.sub.1:−2x+3y+2z≦−2

C.sub.2:+3x−3y+2z≦−1

and the stack (depicted here growing downwards) with some initial bounds coming from one-variable constraints, and taking and propagating two decisions:

TABLE-US-00004 bound reason set reason constraint −2 ≦ x  { } x ≦ 3 { } 1 ≦ y { } y ≦ 4 { } −2 ≦ z .sup.  { } z ≦ 2 { } 1 ≦ x {1 ≦ y, −2 ≦ z} C.sub.1 y ≦ 2 {x ≦ 3, −2 ≦ z} C.sub.1 z ≦ 0 {x ≦ 3, 1 ≦ y}  C.sub.1 x ≦ 2 decision  .sup. z ≦ −1 {x ≦ 2, 1 ≦ y}  C.sub.1  .sup. z ≦ −2 decision x ≦ 1 {y ≦ 2, z ≦ −2} C.sub.0 2 ≦ y {1 ≦ x, z ≦ −2} C.sub.0 2 ≦ x {2 ≦ y, −2 ≦ z} C.sub.1

[0121] Now there is a conflict with initial CSS {x≦1, 2≦x}. In the first conflict analysis step, 2≦x is removed from the CSS and its reason set {2≦y, −2≦z} inserted, obtaining the CSS {−2≦z, x≦1, 2≦y}, with two bounds of this decision level (dl 2).

[0122] In the second conflict analysis step, 2≦y is replaced by its reason set {1≦x, z≦−2} obtaining the new CSS {−2≦z, 1≦x, z≦−2, x≦1} which does not allow yet to backjump since it still contains two bounds of dl 2. But now a cut is attempted between the initial CC, which is C.sub.1, and the reason constraint of 2≦y, which is C.sub.0, in such a way that y is eliminated. Here this cut exists, with c=d=1, and the new constraint C.sub.3:

[0123] −1x−1z≦−1 is obtained and learned. This new constraint allows one to backjump to dl 1, since there it propagates 2≦x. At that point, after three more propagations,

TABLE-US-00005 bound reason set reason constraint −2 ≦ x  { } x ≦ 3 { } 1 ≦ y { } y ≦ 4 { } −2 ≦ z .sup.  { } z ≦ 2 { } 1 ≦ x {1 ≦ y, −2 ≦ z} C.sub.1 y ≦ 2 {x ≦ 3, −2 ≦ z} C.sub.1 z ≦ 0 {x ≦ 3, 1 ≦ y}  C.sub.1 x ≦ 2 decision  .sup. z ≦ −1 {x ≦ 2, 1 ≦ y}  C.sub.1 2 ≦ x {z ≦ −1} C.sub.3 −1 ≦ z .sup.  {x ≦ 2} C.sub.3 2 ≦ y {2 ≦ x, z ≦ −1} C.sub.0 2 ≦ x {2 ≦ y, −1 ≦ z} C.sub.1
another conflict exists with CSS {x≦2, 3≦x}, which after the first step becomes {x≦2, −1≦z, 2≦y}, all three of this decision level (dl 1). After the second step (replacing 2≦y) the CSS becomes {x≦2, z≦−1, 2≦x, −1≦z}, all in dl 1. As before, the performed cut between C.sub.1 and C.sub.0 (the initial CC and the reason constraint of 2≦y) eliminates the variable y, obtaining −1x−1z≦−1.

[0124] After the third step (replacing −1≦z), the CSS becomes {x≦2, z≦−1, 2≦x}, all in dl 1. The CC does not change because no cut eliminating z exists with C.sub.3.

[0125] After the 4th step (replacing 2≦x), the CSS becomes {x≦2, z≦−1}, both in dl 1. Again the CC does not change because no cut eliminating z exists with C.sub.3.

[0126] After the 5th step (replacing z≦−1), the CSS becomes {1≦y, x≦2}, with only one literal of dl 1. The backjump with this CSS can take us to the dl of 1≦y (dl 0) and add there the negation of x≦2, which is 3≦x.

[0127] The result of the cut on CC with C.sub.1 eliminating z gives us −4x+3 y≦−4. The backjump with this cut can also take us to the dl of 1≦y (dl 0), propagating 2≦x. Since this is weaker than the bound 3≦x obtained from the CSS, here the CSS one has been chosen. After two more propagations, the procedure returns ‘no solution’ since the conflicting pair of literals y≦2 and 3≦y appear at dl 0:

TABLE-US-00006 bound reason set reason constraint −2 ≦ x  { } x ≦ 3 { } 1 ≦ y { } y ≦ 4 { } −2 ≦ z .sup.  { } z ≦ 2 { } 1 ≦ x {1 ≦ y, −2 ≦ z} C.sub.1 y ≦ 2 {x ≦ 3, −2 ≦ z} C.sub.1 z ≦ 0 {x ≦ 3, 1 ≦ y}  C.sub.1 3 ≦ x {1 ≦ y} C.sub.4 −1 ≦ z .sup.  {3 ≦ x, y ≦ 2}  C.sub.0 3 ≦ y {3 ≦ x, −1 ≦ z} C.sub.0

Data Structures and Algorithms

[0128] The method proposed in this invention heavily relies on the efficiency of its implementation, for which new data structures and algorithms are given.

[0129] There is an array, the Bounds Array, indexed by variable number, that can return in constant time the current upper and lower bounds for that variable. Property 1: It always stores, for each variable x.sub.i, the positions pl.sub.i and pu.sub.i in the stack of its current (strongest) upper bound and lower bound, respectively, with pl.sub.i=0 (pu.sub.i=0) if x, has no current lower (upper) bound.

[0130] The data structure for the stack is another array containing at each position three data fields: a bound, a natural number pos, and an info field containing, among other information, the reason set and the reason constraint. Property 2: The value pos is always the position in the stack of the previous bound of the same type (lower or upper) for this variable, with pos=0 for initial bounds.

[0131] When pushing a new bound on the stack, and when popping a bound from the stack (during backjumping), it is easy to maintain properties 1 and 2 in constant time.

TABLE-US-00007 TABLE 1 Bounds array Height in stack of current bound Lower: upper x.sub.1 1 2 x.sub.2 0 0 . . . . . . x.sub.7 40  31  . . . . . .

TABLE-US-00008 TABLE 2 Stack 1 0 ≦ x.sub.1 0 info 2 x.sub.1 ≦ 8.sup.  0 info . . . 13 0 ≦ x.sub.7 0 info 14 x.sub.7 ≦ 9.sup.  0 info . . . 23 2 ≦ x.sub.7 13  info . . . 31 x.sub.7 ≦ 6.sup.  14  info . . . 40 5 ≦ x.sub.7 23  info . . .

[0132] Another important data structure allows for efficient bound propagation. For each variable x, there are two occurs lists. The positive occurs list for x contains all pairs (I.sub.C, a) s.t. C is a linear constraint where x occurs with positive coefficient a. The negative occurs list contains the same for occurrences with a negative coefficient a. Here I.sub.C is an index to the constraint header of C in the array of constraint headers. Each constraint header contains an integer F.sub.C called a filter, and a (pointer to) the constraint C itself. The filter F.sub.C is maintained cheaply, in such a way that C can only propagate if F.sub.C>0, thus avoiding many useless (cache-) expensive inspections of the actual constraint C. This is done as follows.

[0133] Let C be a constraint of the form a.sub.1x.sub.1+ . . . +a.sub.nx.sub.n≦a.sub.0. Let l.sub.i≦x.sub.i and x.sub.i≦u.sub.i be the current lower and upper bounds (if any) for x.sub.i. Each expression a.sub.ix.sub.i in C can have a minimal value m.sub.i, which is a.sub.i.Math.l.sub.i if a.sub.i>=0, and a.sub.i.Math.u.sub.i otherwise.

[0134] Here m.sub.i is undefined if there is no such bound l.sub.i (or u.sub.i). Initially, if some m.sub.i is undefined, then F.sub.C is set to a special value undefined and otherwise to −a.sub.0+m.sub.1+ . . . +m.sub.n+max.sub.i, {abs(a.sub.i.Math.(u.sub.i-l.sub.i))} where max and abs denote the maximum and absolute value functions, respectively. After that, F.sub.C is said to be precise: the constraint C propagates if and only if, undefined≠F.sub.C>0. Property 3: At all timepoints, F.sub.C=undefined or F.sub.C is an upper approximation of the precise one.

[0135] To preserve property 3, these filters need to be updated when new bounds are pushed onto the stack, and need to be restored when backjumping.

[0136] Let a new lower bound k≦x be pushed onto the stack. Let the previous lower bound for x (if any) be k′≦x. For each pair (I.sub.C, a) in the positive occurs list of x, using I.sub.C, access is done to the F.sub.C and increase it by abs (a.Math.(k−k′)). If there was no previous lower bound, then F.sub.C was undefined and is now set to 1. If F.sub.C becomes positive, the constraint C is visited because it may propagate some new bound. After each time a constraint C is visited, F.sub.C is set to its precise value.

[0137] Let a new upper bound x≦k be pushed on the stack. Then exactly the same is done, where x≦k′ is the previous upper bound for x (if any), and using the negative occurs list. In order to be able to restore the filters when backjumping, each time an F.sub.C value is increased by an amount d, a pair (F.sub.C, d) is pushed onto a filter backtrack stack, and when it is moved from undefined to 1 a pair (F.sub.C, undefined) is pushed.

[0138] For each decision that is taken, i.e., when pushing the i+1th decision on the stack, in a separate data structure a natural number h.sub.i is recorded, h.sub.i being the height of the filter backtrack stack before taking decision i+1. Then, when backjumping to a stack with k decisions, each pair (F.sub.C, d) in the filter backtrack stack above height h.sub.k is popped, and its F.sub.C is decreased by d if d≠undefined, and restored to undefined if d=undefined.

[0139] Following a particular application case in which the proposed method is applied will be explained.

[0140] A steel factory needs to plan its next week, 168 hours in which it has to carry out N tasks (orders).

[0141] Each task i in 1 . . . N has a duration of d.sub.i consecutive (whole) hours and requires, during all its d.sub.i hours of activity, the exclusive use of one or more units of R different resources. For example, a certain task may occupy two mechanics, one operator, three cranes and two trucks. If during a certain hour several tasks are active simultaneously, they cannot share the resources they use.

[0142] For each resource j and each hour h in 1 . . . 168, let the integer used.sub.j,h denote the total number of units of resource j used during hour h and let peak.sub.j=max(used.sub.j,1, . . . used.sub.j,168) be the (integer) peak usage of resource j during the week. The problem is to schedule all tasks, i.e., for each task i determine a starting time, while minimizing the total resource cost C=c.sub.1.Math.peak.sub.—1≦, + . . . +c.sub.R.Math.peak.sub.R, where each c.sub.j is a cost associated to resource j.

[0143] In practice the planned period of course needs not be 168 time units, and typically there are many more constraints, usually involving logical relationships, such as precedences between (groups of) tasks, temporary unavailability of resources, earliest or latest starting times for tasks, storage capacities for intermediate products, etc.

[0144] This problem is well known to have a large impact on costs and benefits in industry. Finding good solutions can be extremely hard.

[0145] A standard notation for it uses two sets of N.Math.168 binary variables starts.sub.i,h (“task i starts on hour h”) and isactive.sub.i,h (“task i is active on hour h”) for all i and h.

[0146] It uses constraints expressing that starts.sub.i,h implies isactive.sub.i,h (i.e., −starts.sub.i,h+isactive.sub.i,h≧0) and also starts.sub.i,h implies isactive.sub.i,h+1, etc., for its whole duration d.sub.i. Also, each task i starts exactly once: starts.sub.i,1+ . . . +starts.sub.i,168=1. In addition, for each resource j and hour h, we have used.sub.j,h=units_needed.sub.1,j.Math.isactive.sub.1,h+ . . . +units_needed.sub.N,j−isactive.sub.N,h, where units_needed.sub.i,j is the number of units of j needed by task i. Finally, for each resource j there are 168 constraints peak.sub.j≧used.sub.j,1 . . . peak.sub.j≧used.sub.j,168.

[0147] A state-of-the-art methodology is the one used in MIP solvers, by solving a collection of LP relaxations of the given constraints, i.e., temporarily “forgetting” that certain variables must take integer values. Rational (possibly non-integer) solutions are sought for by means of (variants of) simplex or interior point methods. Such “forgetful” or “blind” intermediate non-integer solutions may be meaningless for our problem, since they may say, e.g., that a certain binary variable active.sub.i,h is 0.7, or that 3.54 units of resource j are used during some hour h.

[0148] Additional steps are then performed to turn these intermediate solutions into an integer one. For example, branch-and-cut methods maintain a tree of subproblems pending to be explored, with their rational solutions. Given a leaf node with variable x getting a non-integer solution 3.54, one can branch, i.e., split the problem into two subproblems, one with x≦3 and one with x≧4, or compute and add a new constraint (by a cut), precluding the non-integer solution 3.54 for x.

[0149] Such MIP solvers are well known to perform extremely poorly on pure SAT problems, where all variables are binary and constraints are (purely logical) clauses, and where conflict-driven clause-learning (CDCL) techniques are vastly superior and hence the method of choice in practice.

[0150] Here it is claimed a similar superiority of this invention, also a SAT-like method, for this industrial scheduling problem, which also has many binary variables and other relatively small-domain integer ones, as well as an essentially logical constraint structure as in pure SAT.

[0151] The proposed method explores the search space as CDCL does in SAT: by taking decisions (in our case each decision, as stated in step 1d2, is a heuristically guided guess of an upper or lower bound for a given variable) and efficiently inferring and adding the implied information by propagating these decisions. And, again as in CDCL, when a conflict appears (i.e., two contradictory bounds), a conflict analysis procedure allows one to backjump to an earlier search state, enrich it by an additional bound and its propagations, and possibly learning a new constraint.

[0152] Together with [5], the proposed method is the first of this nature able to handle integer variables and constraints, but with the advantage over [5] that in the proposed method arbitrary decisions can be taken. Indeed it performs much better than [5], as revealed by the experiments of the publication [9] (which also reports superiority over the main commercial MIP solvers on other ILP problems from the well-known standard MIPLIB).

[0153] As it happens in methods for SAT (cf. section “Background of the invention”), it is rather obvious that the proposed method performs a systematic search over the possible solutions. This involves only trivial mathematics. Again as for SAT, the key aspects of the proposed method are the engineering of novel data structures (propagation record, propagation stack, reason set, reason constraint) and the novel heuristics for guiding the search and for learning new constraints. Such techniques for SAT are disclosed in U.S. Pat. No. 7,418,369.

[0154] Applied to the industrial scheduling problem, the proposed method uses heuristics for taking good decisions (typically, as in SAT, on variables involved in many recent conflicts). For example, it will guess an upper bound on the total resource cost C or on some of the individual variables peak.sub.h. Meaningful new bounds will then be propagated (unlike what happens in LP relaxations; present propagation takes into account that variables must be integer). Similarly, meaningful strong new constraints are quickly learned, stating that certain combinations of tasks cannot take place simultaneously, etc.

[0155] These newly learned constraints again strengthen the propagation power and prevent future similar conflicts.

[0156] Being able to take arbitrary decisions is essential (step 1d2 of claim 1) to the proposed method. In [5] one can only decide a given variable to be equal to its current upper bound or to its current lower bound; in practice, one needs to guess it to belong to, say, the lower (or upper) halve of the interval between its current upper and lower bounds, an idea akin to binary search.

[0157] While preferred embodiments of the invention have been shown and described herein, it will be understood that such embodiments are provided by way of example only. Numerous variations, changes and substitutions will occur to those skilled in the art without departing from the spirit of the invention. Accordingly, it is intended that the appended claims cover all such variations as fall within the spirit and scope of the invention.