Optimal network configuration repair
View Patent ↗Changing a network configuration to restore compliance to one requirement may invalidate the network compliance with another requirement. A method changes a configuration to restore compliance to all requirements at minimum cost. The requirements are a hybrid of symbolic, arithmetic and bit-vector constraints, so traditional optimization techniques such as linear programming, that work only for purely arithmetic constraints, do not apply. The requirements are represented as SMT (satisfiability-modulo-theory) constraints on configuration variables, and then a weighted Max-SAT solver is used to compute the optimal configuration changes in order to minimize the cost.
1. A method of changing network configuration modeled as a set of equations of the form x 1 =c 1 , . . . , xk=ck where each xi is a configuration variable of a network component and ci is its current value to restore compliance to all requirements where a requirement is a conjunction of constraints F 1 , . . . , Fm where Fi is a Boolean function of the form R(x 1 , . . . , xk) of configuration variables x 1 , . . . , xk at a minimum cost, comprising the steps of:
specifying each requirement Fi has infinite change cost;
specifying the weight of each constraint xi=ci is equal to its change cost; and
submitting the constraint (xi=ci & . . . & xk=ck) & (F 1 & . . . & Fk) to a MaxSAT solver;
whereby the MaxSAT solver returns a solution that satisfies F 1 & . . . & Fk and finds values of x 1 , . . . , xk with minimum incurred change cost.
2. The method as set forth in claim 1 , wherein the MaxSAT solver is a Yices SMT Solver.
3. The method as set forth in claim 1 , wherein the language for specifying requirements is a Satisfiability Modulo Theories (SMT) language eith Equality of Uninterpreted Function, Linear Arithmetic and Bit Vectors.
4. A computer readable storage medium storing a program of instructions executable by a machine to perform a method for of changing network configuration modeled as a set of equations of the form x 1 =c 1 , . . . , xk=ck where each xi is a configuration variable of a network component and ci is its current value to restore compliance to all requirements where a requirement is a conjunction of constraints F 1 , . . . , Fm where Fi is a Boolean function of the form R(x 1 , . . . , xk) of configuration variables x 1 , . . . , xk at a minimum cost, comprising the steps of:
specifying each requirement Fi has infinite change cost;
specifying the weight of each constraint xi=ci is equal to its change cost; and
submitting the constraint (xi=ci & . . . & xk=ck) & (F 1 & . . . & Fk) to a MaxSAT solver;
whereby the MaxSAT solver returns a solution that satisfies F 1 & . . . & Fk and finds values of x 1 , . . . , xk with minimum incurred change cost.