-1
$\begingroup$

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.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

I don't understand why you would want to encode minimality into it. You can obtain the same effect very easily. Run the SAT solver normally, then try setting variables to 0 as long the formula is still satisfied. This will give you a minimal satisfying assignment, if one exists.

Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged .