Systems and methods to semantically compare product configuration models

Patent metadata

Field	Value
Publication number	US-11586935-B2
Application number	US-201716469055-A
Country	US
Kind code	B2
Filing date	Apr 11, 2017
Priority date	Apr 11, 2017
Publication date	Feb 21, 2023
Grant date	Feb 21, 2023

Abstract

Systems and methods to semantically compare product configuration models. A method includes receiving a first configuration model and a second configuration model. The method includes generating a first order logic (FOL) representation of the first configuration model and an FOL representation of the second configuration model. The method includes 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. The method includes storing an indication that the first configuration model is equivalent to the second configuration model when the SMT solve for nonequivalence satisfiability is not satisfied.

First claim

What is claimed is:

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 mode

Assignees

• Siemens Ind Software Inc

Inventors

• Neuhäusser Martin Richard
• Schulz Gabor

Classifications

• G06N5/013 Primary

  Automatic theorem proving · CPC title

• G06F30/00 Primary

  Computer-aided design [CAD] · CPC title

• G06N5/04

  Inference or reasoning models · CPC title

• G06F17/16

  Matrix or vector computation {, e.g. matrix-matrix or matrix-vector multiplication, matrix factorization (matrix transposition G06F7/78)} · CPC title

• G06N5/006 Primary

  Physics · mapped topic