Common generated instruction selections are based on tree pattern matching, but modern and custom architectures feature instructions, which cannot be covered by trees. To overcome this limitation, we are the first to employ graph transformation, the natural generalization of tree rewriting. Currently, the only approach allowing us to pair graphbased instruction selection with linear time complexity is the mapping to the Partitioned Boolean Quadratic Problem (PBQP). We present formal foundations to verify this approach and therewith identify two problems of the common method and resolve them. We confirm the capabilities of PBQP-based instruction selection by a comparison with a finely-tuned hand-written instruction selection. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification--Correctness proofs; D.3.4 [Programming Languages]: Processors--Compilers,Retargetable Compilers General Terms Algorithms, Theory, Verification