I’m studying HORN-SAT problems and I have a specific question about the minimal model.

Given a HORN-SAT problem with multiple solutions, I understand that the minimal model is the one with the smallest number of variables set to true.

For example, in a HORN-SAT problem with five variables (A, B, C, D, E), suppose the minimal model is found to be A=1 and C=1, leaving B, D, and E as free variables that can take either 0 or 1.

Is it required that any solution to the problem has A=1 and C=1, as dictated by the minimal model?

My question is: Must all solutions to the HORN-SAT problem contain the minimal model as a subset? In other words, if the minimal model requires certain variables to be 1, then these variables must be 1 in all satisfying solutions ?

I’d appreciate any references or explanations to understand this better.