Scalable and interactive method of generating and modifying network configurations to enforce compliance with high-level requirements
A system and method provides a solution to the problem of applying end-to-end requirements of connectivity, security, reliability and performance to configure a network and ultimately assign network components to the network. All requirements are modeled as constraints and a constraint solver does the resolution. Not every constraint to be solved is solved by the model-finder. Instead, we “factor away” subsets of a constraint that can be efficiently solved via a special-purpose constraint solver, such as an SQL/Prolog engine, linear programming system, or even an algorithm, leaving behind a constraint that truly requires the power of model-finding, and that is often efficiently solvable by existing model-finders. Such constraints are compiled into quantifier-free constraints that are Boolean combinations of constraints of two forms x=y and x=c where x, y are variables and c is a constant. Such constraints can be efficiently solved by modern SAT-based model-finders. The system intelligently removes the quantifiers instead of having the model-finder remove the quantifiers. An “unsatisfiability-core” analysis efficiently guides the search for configurations to change to restore consistency.
1. A system for generating and modifying network configurations to enforce compliance with high-level requirements comprising:
A processor executing:
adaptation engine for responding to an event by providing a configuration database variable output and a requirement output that needs to be satisfied to respond to the event; and
requirement solver that in response to receiving the outputs from said adaptation engine provides an instantiated configuration database;
when an instantiated configuration database cannot be provided, relaxing the configuration database variable output to the requirement solver and then providing an instantiated configuration database.
2. A system as set forth in claim 1 , wherein said requirement solver comprises a partial evaluator, a model-finder and a SAT solver.
3. A system as set forth in claim 2 , wherein said model-finder is a Kodkod model-finder.
4. A system as set forth in claim 2 , wherein said SAT solver is a ZChaff SAT solver.
5. A system as set forth in claim 2 , wherein said SAT solver is a MiniSat Prover.
6. A system as set forth in claim 2 , wherein said partial evaluator factors away constraints that can be solved by a special purpose constraint solver.
7. A non-transitory program storage device, readable by machine, tangibly embodying a program of instructions executable by the machine to cause the machine to perform a method for generating and modifying network configurations to enforce compliance with high-level requirements, comprising the steps of:
receiving a network configuration database with variable;
receiving a network requirement; partially evaluating said configuration database and requirement for generating quantifier-free constraints;
model finding and SAT solving the quantifier-free constraints for creating a database satisfying requirements and a reconfiguration plan; and
when the database satisfying requirements and a reconfiguration plan cannot be created, relaxing the variable and creating the database satisfying requirements and a reconfiguration plan using the relaxed variable.
8. A method of generating and modifying network configurations to enforce compliance with high-level requirements comprising the steps of:
receiving a network configuration database with variable;
receiving a network requirement; partially evaluating said configuration database and requirement for generating quantifier-free constraints;
model finding and SAT solving the quantifier-free constraints for creating a database satisfying requirements; and
when the database satisfying requirements cannot be created, relaxing the variable and creating the database satisfying requirements using the relaxed variable.