Computer-assisted proofs
We now have a MATLAB-assisted NP-hardness proof for our problem. We basically came up with a gadget, and could easily prove by hand that in the good case the gadget was feasible, but an NP-hardness proof clearly also requires a proof that in the bad case there's no way of doing well on the gadget. We were completely unable to prove this by hand, since each transmitter could set its power level to something completely different and it was insanely complicated to argue about what the structure had to look like. So Matthew wrote up our gadget in MATLAB and played around with some parameter settings, and it seems to have worked. I find this very strange, as I don't remember seeing any computer-assisted hardness proofs in the past. I'm sure they're out there, but I guess they're pretty rare. CS theory people -- do any results spring to mind?