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 a, b, and 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.

1. || (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.

2. flag1? (flag2 flag3 ...) operator means that the following bracket would have to be true as a whole if flag1 is enabled. This is equivalent to the implication operator.

3. ^^ (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:
   

1. !flag1 operator is basically a negation.

2. flag1 flag2 operator (whitespace) is basically an AND operation unless the parent bracket is preceded by || or ^^.

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.

Even though satispy also has support for solving the CNF formula, I went with pycosat 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