How to encode maximality/minimality constraints in SAT or its variants such as MaxSAT or MinSAT? For example, let us say (x1 OR x2) AND (x2 OR x3 OR x4) AND (x4 OR x5) is a formula. I want its solutions to be the assignments that satisfy all clauses by setting 'minimal' number of variables to 1. This is different from having minimum number of variables set to 1, since the assignment (1, 0, 1, 0, 1) is minimal, but not minimum.