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.

  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:

(a & !b & !c) | (!a & b & !c) | (!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


ABOUT THE AUTHOR
Pallav Agarwal Image
My name is Pallav Agarwal. I am an undergrad of the department of Computer Science and Engineering, Indian Institute of Technology Kanpur, India. I love experimenting with tech, and this blog is a way for me to give a little helping hand to other's who are like me (but don't know it yet).

I am ambitious, intelligent, competitve (sometimes too much), loyal and brutally honest. People I respect the most are teachers, which is partially why I myself like to teach too. Apart from programming, I also like travelling, adventure sports and trying new food items. If you like a post, have a query, or just want to chit-chat, let me know here