Any boolean formula can be represented efficiently as a reversible circuit (i.e. with at most a polynomial increase in the number of gates), with n input bits and n output bits. If it is an n-input, 1-output formula, the corresponding reversible circuit will have 1 'main' output bit and a series of 'garbage' output bits. In the case of SAT, the goal is to find an input string that will give 1 on the main output bit (we don't care what it gives on the garbage outputs). It seems to me that if you took a boolean formula, wrote out its reversible circuit using quantum gates, set the main output bit to 1 (and the garbage outputs to a uniform superposition of all states) then traced back through the circuit from the output to the input (its reversible after all), you'd get a superposition of all possible inputs that satisfy the formula. A simple quantum measurement, and you're done - you get a string that satisfies the formula. Now all you have to do is (classically) check that the string indeed satisfies the formula. If it does, then great. If it doesn't, you can conclude that the formula is unsatisfiable. EDIT: upon thinking about this further, I realized that upon conversion to a reversible circuit, you might also need to include a number of 'garbage' inputs as well, so that when the garbage inputs are set to a specific string the behavior is identical to the irreversible case. In the final quantum measurement, however, there is no way to ensure that the measured string will have the garbage bits set to the string we want, thus our measured string could satisfy the reversible version but not the irreversible version. Is this assessment correct?