Boolean matching is one of the enabling techniques for technology mapping and logic resynthesis of Field Programmable Gate Array (FPGA). SAT-based Boolean matching (SAT-BM) has been proposed, but the computational complexity prohibits its practical deployment. In this paper, we leverage the symmetries in Boolean functions and target FPGA architectures to prune the solution space. Besides the exploration of symmetries, we also propose a few techniques to reduce the replication runtime for SAT instance generation using the incremental SAT reasoning engine. In terms of the overall runtime, our SAT-BM obtains up to 226X speedup compared to the original SAT-BM algorithm, making SAT-BM more practical.