index.html 12.8 KB
 Pallav Agarwal committed May 12, 2016 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 ``````Determining legal USE Flag combinations using a CNF SAT Solver - VARSTACK
`````` Pallav Agarwal committed Sep 26, 2016 28 `````` `````` Pallav Agarwal committed May 12, 2016 29 30 31 32 33 ``````

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 `````` Pallav Agarwal committed Aug 20, 2016 100 ``````SummerOfCode16.

`````` Pallav Agarwal committed May 12, 2016 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 ``````

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.

RECENT POSTS

RECENT TIPS

TAGGED POSTS

`````` Pallav Agarwal committed Sep 26, 2016 223 `````` `````` Pallav Agarwal committed May 12, 2016 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 ``````

``````