StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

POHow to implement a superoptimizer
text
Body
copied!<p>[Related to <a href="https://codegolf.stackexchange.com/questions/12664/implement-superoptimizer-for-addition">https://codegolf.stackexchange.com/questions/12664/implement-superoptimizer-for-addition</a> from Sep 27, 2013]</p> <p>I am interested in how to write <a href="http://en.wikipedia.org/wiki/Superoptimization" rel="nofollow noreferrer">superoptimizers</a>. In particular to find small logical formulae for sums of bits. This was previously set this as a challenge on codegolf but it seems a lot harder than one might imagine.</p> <p>I would like to write code that finds the smallest possible propositional logical formula to check if the sum of y binary 0/1 variables equals some value x. Let us call the variables x1, x2, x3, x4 etc. In the simplest approach the logical formula should be equivalent to the sum. That is, the logical formula should be true if and only if the sum equals x.</p> <p>Here is a naive way to do that. Say y=15 and x = 5. Pick all 3003 different ways of choosing 5 variables and for each make a new clause with the AND of those variables AND the AND of the negation of the remaining variables. You end up with 3003 clauses each of length exactly 15 for a total cost of 45054. </p> <p>However, if you are allowed to introduce new variables into your solution then you can potentially reduce this a lot by eliminating common subformulae. So in this case your logical formula consists of the y binary variables, x and some new variables. The whole formula would be satisfiable if and only if the sum of the y variables equals x. The only allowed operators are <code>and</code>, <code>or</code> and <code>not</code>.</p> <p>It turns out there is a <a href="http://www.cs.cmu.edu/~wklieber/papers/2007_efficient-cnf-encoding-for-selecting-1.pdf" rel="nofollow noreferrer">clever method</a> for solving this problem when x =1, at least in theory . However, I am looking for a computational intensive method to search for small solutions. </p> <pre><code>How can you make a superoptimizer for this problem? </code></pre> <p>Examples. Take as an example two variables where we want a logical formula that is True exactly when they sum to 1. One possible answer is:</p> <pre><code>(((not y0) and (y1)) or ((y0) and (not y1))) </code></pre> <p>To introduce a new variable into a formula such as <code>z0</code> to represent <code>y0 and not y1</code> then we can introduce a new clause <code>(y0 and not y1) or not z0</code> and replace <code>y0 and not y1</code> by <code>z0</code> throughout the rest of the formula . Of course this is pointless in this example as it makes the expression longer.</p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload