Systems and methods to semantically compare product configuration models

1. A method performed by a data processing system, comprising:

determining whether configuration models of two different engineering tools or different versions of a configuration model of a same engineering tool are equivalent, including by:

receiving a first configuration model and a second configuration model, wherein the first configuration model and the second configuration model each model constraints for physical characteristics of a product;

generating a first order logic (FOL) representation of the first configuration model and an FOL representation of the second configuration model;

performing a satisfiability modulo theories (SMT) solve for nonequivalence satisfiability on the FOL representation of the first configuration model and the FOL representation of the second configuration model; and

when the SMT solve for satisfiability is not satisfied, storing an indication that the first configuration model is equivalent to the second configuration model.

2. The method of claim 1 , wherein when the SMT solve for nonequivalence satisfiability is satisfied, storing an indication that the first configuration model is not equivalent to the second configuration model.

3. The method of claim 1 , wherein when the SMT solve for nonequivalence satisfiability is satisfied, performing an SMT solve for variants in the first configuration model that are not present in the second configuration model, and storing variants identified by the SMT solve for variants in the first configuration model that are not present in the second configuration model.

4. The method of claim 1 , wherein {right arrow over (v)}=(v 1 , v 2 , . . . , v n ) is used to denote a vector of configuration options that uniquely determine the first configuration model.

5. The method of claim 1 , wherein φ represents the FOL representation of the first configuration model,

ψ represents the FOL representation of the second configuration model, and

performing a satisfiability modulo theories (SMT) solve for nonequivalence satisfiability comprises searching for a satisfying assignment for ¬(φ→ψ) or ¬(ψ→φ).

6. The method of claim 1 , wherein φ represents the FOL representation of the first configuration model,

ψ represents the FOL representation of the second configuration model, and

performing an SMT solve for variants comprises checking the satisfiability of φ∧¬ψ and ψ∧¬φ.

7. A data processing system having at least a processor and an accessible memory,

the data processing system configured to determine whether configuration models of two different engineering tools or different versions of a configuration model of a same engineering tool are equivalent, including by:

receiving a first configuration model and a second configuration model, wherein the first configuration model and the second configuration model each model constraints for physical characteristics of a product;

generating a first order logic representation of the first configuration model and an FOL representation of the second configuration model;

performing a satisfiability modulo theories (SMT) solve for nonequivalence satisfiability on the FOL representation of the first configuration model and the FOL representation of the second configuration model; and

when the SMT solve for satisfiability is not satisfied, storing an indication that the first configuration model is equivalent to the second configuration model.

8. The data processing system of claim 7 , wherein the data processing system is further configured to, when the SMT solve for nonequivalence satisfiability is satisfied, store an indication that the first configuration model is not equivalent to the second configuration model.

9. The data processing system of claim 7 , wherein the data processing system is further configured to, when the SMT solve for nonequivalence satisfiability is satisfied, perform an SMT solve for variants in the first configuration model that are not present in the second configuration model, and store variants identified by the SMT solve for variants in the first configuration model that are not present in the second configuration model.

10. The data processing system of claim 7 , wherein {right arrow over (v)}=(v 1 , v 2 , . . . , v n ) is used to denote a vector of configuration options that uniquely determine the first configuration model.

11. The data processing system of claim 7 , wherein φ represents the FOL representation of the first configuration model,

ψ represents the FOL representation of the second configuration model, and

performing a satisfiability modulo theories solve for nonequivalence satisfiability comprises searching for a satisfying assignment for ¬(φ→ψ) or ¬(ψ→φ).

12. The data processing system of claim 7 , wherein φ represents the FOL representation of the first configuration model,

ψ represents the FOL representation of the second configuration model, and

performing an SMT solve for variants comprises checking the satisfiability of φ∧¬ψ and ψ∧¬φ.

13. A non-transitory machine-readable medium encoded with executable instructions that, when executed, cause a data processing system to determine whether configuration models of two different engineering tools or different versions of a configuration model of a same engineering tool are equivalent, including by:

receiving a first configuration model and a second configuration model, wherein the first configuration model and the second configuration model each model constraints for physical characteristics of a product;

generating a first order logic representation of the first configuration model and an FOL representation of the second configuration model;

performing a satisfiability modulo theories (SMT) solve for nonequivalence satisfiability on the FOL representation of the first configuration model and the FOL representation of the second configuration model; and

when the SMT solve for satisfiability is not satisfied, storing an indication that the first configuration model is equivalent to the second configuration model.

14. The non-transitory machine-readable medium of claim 13 , further encoded with executable instructions to, when the SMT solve for nonequivalence satisfiability is satisfied, store an indication that the first configuration model is not equivalent to the second configuration model.

15. The non-transitory machine-readable medium of claim 13 , further encoded with executable instructions to, when the SMT solve for nonequivalence satisfiability is satisfied, perform an SMT solve for variants in the first configuration model that are not present in the second configuration model, and store variants identified by the SMT solve for variants in the first configuration model that are not present in the second configuration model.

16. The non-transitory machine-readable medium of claim 13 , wherein {right arrow over (v)}=(v 1 , v 2 , . . . , v n ) is used to denote a vector of configuration options that uniquely determine the first configuration model.

17. The non-transitory machine-readable medium of claim 13 , wherein φ represents the FOL representation of the first configuration model,

ψ represents the FOL representation of the second configuration model, and

performing a satisfiability modulo theories solve for nonequivalence satisfiability comprises searching for a satisfying assignment for ¬(φ→ψ) or ¬(ψ→φ).

18. The non-transitory machine-readable medium of claim 13 , wherein φ represents the FOL representation of the first configuration model,

ψ represents the FOL representation of the second configuration model, and

performing an SMT solve for variants comprises checking the satisfiability of φ∧¬ψ and ψ∧¬φ.