### 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 `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.

`|| (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`flag1`

is 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)`

`!flag1`

operator is basically a negation.`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*