index.html 12.8 KB
Newer Older
Pallav Agarwal's avatar
Pallav Agarwal committed
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
<title>Determining legal USE Flag combinations using a CNF SAT Solver - VARSTACK</title>
<div id="fb-root"></div>
<script>(function(d, s, id) {
var js, fjs = d.getElementsByTagName(s)[0];
if (d.getElementById(id)) return;
js = d.createElement(s); js.id = id;
js.src = "//connect.facebook.net/en_US/sdk.js#xfbml=1&version=v2.5";
fjs.parentNode.insertBefore(js, fjs);
}(document, 'script', 'facebook-jssdk'));
var host = "varstack.com";
var hostwww = "www.varstack.com";
if (((host == window.location.host) || (hostwww == window.location.host))
        && (window.location.protocol != 'https:'
            || window.location.toString().match(/http.?:\/\/var/))){
  window.location = window.location.toString().replace(/^http:/, "https:").replace(/https:\/\/varstack/, "https://www.varstack");
}
</script>
<meta name=viewport content="width=device-width, initial-scale=1">
<meta charset="utf-8"/>

<noscript>
    <link href="/css/bootstrap.min.css" rel="stylesheet">
    <link href="/css/highlighting.css" rel="stylesheet">
    <link href="/css/style.css" rel="stylesheet">
    
26
    
Pallav Agarwal's avatar
Pallav Agarwal committed
27
</noscript>
28

Pallav Agarwal's avatar
Pallav Agarwal committed
29 30 31 32 33
<script id="loadcss">function loadCSS(e,n,o,t){"use strict";var d=window.document.createElement("link"),i=n||window.document.getElementsByTagName("script")[0],r=window.document.styleSheets;return d.rel="stylesheet",d.href=e,d.media="only x",t&&(d.onload=t),i.parentNode.insertBefore(d,i),d.onloadcssdefined=function(e){for(var n,o=0;o<r.length;o++)r[o].href&&r[o].href===d.href&&(n=!0);n?e():setTimeout(function(){d.onloadcssdefined(e)})},d.onloadcssdefined(function(){d.media=o||"all"}),d}
loadCSS( "https://maxcdn.bootstrapcdn.com/bootstrap/3.3.5/css/bootstrap.min.css", document.getElementById("loadcss"));
loadCSS( "/css/highlighting.css", document.getElementById("loadcss"));
loadCSS( "/css/style.css", document.getElementById("loadcss"));
    
34
    
Pallav Agarwal's avatar
Pallav Agarwal committed
35 36 37 38 39 40 41 42 43 44
</script>

<!-- HTML5 shim, for IE6-8 support of HTML5 elements -->
<!--[if lt IE 9]>
    <script src="//html5shim.googlecode.com/svn/trunk/html5.js"></script>
    <![endif]-->

    
    <div class="container">
        <div class="row" id="menu">
45 46 47 48
            <div class="col-sm-2 col-xs-2 menu" id="site_title">
                <a href="/" style="color:black;">
                    <img src="/img/logo.png" style="max-height:90%;">
                </a>
Pallav Agarwal's avatar
Pallav Agarwal committed
49
            </div>
50
            <div class="col-sm-6 col-xs-10 menu">
Pallav Agarwal's avatar
Pallav Agarwal committed
51 52 53
                <div class="row" id="top_menu">
                    <ul class="nav nav-pills">
                        <li class="active" id="blog"><a class="color_change" href="/">Blog</a></li>
54 55 56
                        <li class="" id="tips"><a class="color_change" href="/tips/">Tips</a></li>
                        <li class="" id="algo"><a class="color_change" href="/algo/">Behind The Scenes</a></li>
                        <li class="" id="about"><a class="color_change" href="/about_me/">About Me</a></li>
Pallav Agarwal's avatar
Pallav Agarwal committed
57 58 59
                    </ul>
                </div>
            </div>
60 61 62 63 64
            <div class="col-sm-4 col-xs-12 menu">
                <form action="/search/" id='search-form'>
                    <input id="search-box" type="text" name="query" placeholder="Search..">
                </form>
            </div>
Pallav Agarwal's avatar
Pallav Agarwal committed
65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
        </div>
        
        <div class="row" id="content">
            <div class="col-md-7 col-md-push-3">
                <div class="row" id="data">
                    <div class="col-md-12">
                        <br />
                        <h3>Determining legal USE Flag combinations using a CNF SAT Solver</h3>
                        <hr />
                        <div class="row text-justify" id="content-holder">
                            <div class="col-md-12">
                                <p>I spent my time doing something rather interesting today.</p>

<p>In my proposal, I had
mentioned that the USE flag combinations to be tested would be:</p>

<blockquote><p>Without any USE flag turned on</p>

<p>With all USE flags turned on</p>

<p>Few random combinations based on default flags,
or inverse of default flags or those generated by tatt.</p></blockquote>

<p>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
<code>REQUIRED_USE="^^ (a b c)"</code> then EXACTLY one flag out of <code>a</code>, <code>b</code>, and <code>c</code> should be
enabled. This doesn't fall under "without USE flags" or "with all USE flags" category.</p>

<p>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.</p>

<p>So, long story short, here's what I did at
100
<a href="https://github.com/pallavagarwal07/SummerOfCode16/blob/dd07d92004b60a00531881773ed6a0a1b41fbd35/Containers/scripts/FlagGenerator/solver.py">SummerOfCode16</a>.</p>
Pallav Agarwal's avatar
Pallav Agarwal committed
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

<p>We have five main kinds of operators.</p>

<ol>
<li><p><code>|| (flag1 flag2 flag3..)</code> operator means that the following bracket would need to have AT LEAST one flag
enabled. This is a simple OR operator between the operands.</p></li>
<li><p><code>flag1? (flag2 flag3 ...)</code> operator means that the following bracket would have to be
true as a whole if <code>flag1</code> is enabled. This is equivalent to the implication operator.</p></li>
<li><p><code>^^ (flag1 flag2 flag3..)</code> 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 <code>a, b, c</code>:<br/></p></li>
</ol>


<center><code>(a & !b & !c) | (!a & b & !c) | (!a & !b & c)</code></center>


<p></p>

<ol>
<li><p><code>!flag1</code> operator is basically a negation.</p></li>
<li><p><code>flag1 flag2</code> operator (whitespace) is basically an AND operation unless the parent
bracket is preceded by <code>||</code> or <code>^^</code>.</p></li>
</ol>


<p>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.</p>

<p>The code I wrote uses <code>satispy</code> to convert constructed SAT formula into CNF form, and
replaces variables by numbers to convert into a format that <code>pycosat</code> can accept.</p>

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

<p>If you have any queries, post them below or open up an issue on github.</p>

<p><i>Thanks for reading</i>
<br /><br /></p>

                            </div>
                        </div>
                    </div>
                </div>
                <hr /><br />
            </div>
            <div class="col-md-3 col-md-pull-7" id="recent">
                <h4>RECENT POSTS</h4>
                <ul class="nav nav-pills nav-stacked">
                    
153 154 155 156
                    <li>
                        <a href="/2017/07/10/How-far-have-I-come-working-at-Google/" class="color_change">An intern's views - How far...</a>
                    </li>
                    
157 158 159 160
                    <li>
                        <a href="/2017/06/07/A-month-end-at-Google/" class="color_change">An intern's views - A month's...</a>
                    </li>
                    
161 162 163 164
                    <li>
                        <a href="/2017/05/07/How-I-got-here/" class="color_change">An intern's views - How I...</a>
                    </li>
                    
165 166 167 168
                    <li>
                        <a href="/2016/09/26/YourHonour-k8s-programming-judge/" class="color_change">YourHonour: A k8s based distributed programming...</a>
                    </li>
                    
Pallav Agarwal's avatar
Pallav Agarwal committed
169
                    <li>
170
                        <a href="/2016/06/09/Bugzilla-Landfills/" class="color_change">Learning from mistakes: Bugzilla Landfills</a>
Pallav Agarwal's avatar
Pallav Agarwal committed
171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193
                    </li>
                    
                </ul>
                <h4>RECENT TIPS</h4>
                <ul class="nav nav-pills nav-stacked">
                    
                    <li>
                        <a href="/2016/05/06/Ultimate-control-over-mobile-browser/" class="color_change">Ultimate control over Mobile Browser with...</a>
                    </li>
                    
                    <li>
                        <a href="/2016/04/27/SSH-keys/" class="color_change">Easy sharing of SSH keys</a>
                    </li>
                    
                    <li>
                        <a href="/2015/08/01/SSH-from-Windows/" class="color_change">Using SSH from Windows 10 without...</a>
                    </li>
                    
                    <li>
                        <a href="/2015/07/27/Boost-Python-Performance/" class="color_change">Cython: Boost Python Code Performance</a>
                    </li>
                    
                    <li>
194 195 196 197 198 199 200 201 202
                        <a href="/2015/07/01/Vim-Mappings/" class="color_change">Quick intro to custom Vim Mappings...</a>
                    </li>
                    
                </ul>
                <h4>TAGGED POSTS</h4>
                <ul class="nav nav-pills nav-stacked">
                    
                    <li>
                        <a href="/2016/05/13/Reference-Sheets-and-Useful-Links/" class="color_change">Reference Sheets and Useful Links</a>
Pallav Agarwal's avatar
Pallav Agarwal committed
203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222
                    </li>
                    
                </ul>
                <br />
                <br />
            </div>
            <div class="col-md-2">
            </div>
            <div class="row">
                <div class="col-md-7 col-md-offset-3 col-xs-10 col-xs-offset-1">
                    <div class="row">
                            <div class="col-xs-4">
                                <div class="fb-like" data-href="//www.varstack.com" data-layout="standard" data-action="like" data-show-faces="true" data-share="true"></div>
                            </div>
                            <div class="col-xs-8 text-right">
                                <script src="https://ajax.googleapis.com/ajax/libs/jquery/2.1.3/jquery.min.js"></script>
                                <script src="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.5/js/bootstrap.min.js"></script>
                                <script src="/js/script.js"></script>
                                
                                
223
                                
Pallav Agarwal's avatar
Pallav Agarwal committed
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
                            </div>
                    </div>
                    <br/>
                </div>
                <div class="col-md-7 col-md-offset-3 col-xs-10 col-xs-offset-1">
                    <div id="disqus_thread"></div>
                    <script type="text/javascript" async>
/* * * CONFIGURATION VARIABLES * * */
var disqus_shortname = 'varstack';

/* * * DON'T EDIT BELOW THIS LINE * * */
(function() {
    var dsq = document.createElement('script'); dsq.type = 'text/javascript'; dsq.async = true;
    dsq.src = '//' + disqus_shortname + '.disqus.com/embed.js';
    (document.getElementsByTagName('head')[0] || document.getElementsByTagName('body')[0]).appendChild(dsq);
})();
(function(i,s,o,g,r,a,m){i['GoogleAnalyticsObject']=r;i[r]=i[r]||function(){
    (i[r].q=i[r].q||[]).push(arguments)},i[r].l=1*new Date();a=s.createElement(o),
    m=s.getElementsByTagName(o)[0];a.async=1;a.src=g;m.parentNode.insertBefore(a,m)
})(window,document,'script','//www.google-analytics.com/analytics.js','ga');

ga('create', 'UA-21768487-2', 'auto');
ga('send', 'pageview');
                    </script>
                    <noscript>Please enable JavaScript to view the <a href="https://disqus.com/?ref_noscript" rel="nofollow">comments powered by Disqus.</a></noscript>
                </div>
            </div>
        </div>
    </div>


    <div class="modal fade" id="imagemodal" tabindex="-1" role="dialog" aria-labelledby="myModalLabel" aria-hidden="true">
        <div class="modal-dialog">
            <div class="modal-content">
                <div class="modal-header">
                    <button type="button" class="close" data-dismiss="modal">
                        <span aria-hidden="true">&times;</span>
                        <span class="sr-only">Close</span>
                    </button>
                    <h4 class="modal-title" id="myModalLabel">
                        Image Preview
                    </h4>
                </div>
                <div class="modal-body">
                    <img src="" id="imagepreview" style="max-height: 100%; max-width: 100%;">
                </div>
            </div>
        </div>
    </div>