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.