Boolean matching (BM) is a widely used technique in FPGA resynthesis and architecture evaluation. We present several improvements to the recently proposed SAT-based Boolean matching formulation (SAT-BM-M). The principal improvement was achieved by deriving the SAT formulation using the implicant instead of minterm representation of the function to be matched. This enables our BM formulation to create a SAT problem of size O ( m*2^k ) as opposed to O(2^n) in the original formulation, where n is the number of inputs to the function, k is the size of the LUT, and m is the number of implicants, which is much smaller than 2^n and experimentally found to be around 3n . Using the new BM formulation, and considering 10-input functions, we can show an almost 3x run time improvement and can solve 5.6x more problems than the SAT based BM formulation. Moreover, using this improved Boolean matching formulation, we implemented (as a proof of concept) a FPGA resynthesis tool, called RIMatch, which was able to reduce the number of LUTs produced by ZMap by 10% on the MCNC benchmarks.