A tool and method for automatically producing near-optimal code sequences are particularly useful for generating near-optimal code sequences in inner loops, crucial subroutines, and device drivers. As a novel functional and architectural strategy, the invention contemplates applying technologies that would be normally in automatic theorem proving to the problem of automatic code generation. The aspect of the automatic theorem proving is realized by matching followed by planning with satisfiability search. Notably also, the present invention targets a goal-oriented, cycle budget limited code sequence in producing the near-optimal code sequence.