Determining legal USE Flag combinations using a CNF SAT Solver
I spent my time doing something rather interesting today.
In my proposal, I had mentioned that the USE flag combinations to be tested would be:
Without any USE flag turned on
With all USE flags turned on
Few random combinations based on default flags, or inverse of default flags or those generated by tatt.
Yesterday, a guy, Harald Timeraider pointed out that some of the USE flag combinations
given by the above rules may not be legal. For example, if an ebuild specifies
REQUIRED_USE="^^ (a b c)" then EXACTLY one flag out of
c should be
enabled. This doesn't fall under "without USE flags" or "with all USE flags" category.
At first I was thinking that for combination os USE flags, I would use the portage API to verify if the USE flag combo was valid and is not, I would randomly generate another combination. But soon, as it always happens, I began to overthink the problem and decided to model the problem as a graph problem. More specifically, as a boolean satisfiability problem.
So, long story short, here's what I did at SummerOfCode16.
We have five main kinds of operators.
|| (flag1 flag2 flag3..)operator means that the following bracket would need to have AT LEAST one flag enabled. This is a simple OR operator between the operands.
flag1? (flag2 flag3 ...)operator means that the following bracket would have to be true as a whole if
flag1is enabled. This is equivalent to the implication operator.
^^ (flag1 flag2 flag3..)operator means that the following bracket will have EXACTLY one flag enabled. The wiki describes it as an XOR operator, which I believe is inaccurate since XOR should allow odd number of operands to be true. For my case, I model it as a 1-from-n operation. For example, for three variables
a, b, c:
(a & !b & !c) | (!a & b & !c) | (!a & !b & c)
!flag1operator is basically a negation.
flag1 flag2operator (whitespace) is basically an AND operation unless the parent bracket is preceded by
Also, because I was having fun and wasn't sure if Portage supported it, I added support for arbitrary amount of nesting, given that the above rules are all followed.
The code I wrote uses
satispy to convert constructed SAT formula into CNF form, and
replaces variables by numbers to convert into a format that
pycosat can accept.
satispy also has support for solving the CNF formula, I went with
for actually solving the CNF formula because it provides an iterator to get as many
solutions as I want. Also the output is a bit easier on the eyes in the form of numbers.
If you have any queries, post them below or open up an issue on github.
Thanks for reading