As Moore's law comes to an end, multiprocessor systems are becoming ubiquitous in today's embedded systems design. In this paper, we address the problem of mapping a Homogeneous Synchronous Dataflow (HSDF) graph onto a multiprocessor platform with the objective of maximizing system throughput. We present two optimization approaches based on branch-and-bound and SAT-solving to explore the design space of all possible actor-to-processor mappings and static order schedules on each processor. In the Logic-Based Benders Decomposition (LBBD) approach, we decompose the problem into a master problem of finding a feasible actor mapping and scheduling, and a sub-problem of deadlock-checking and throughput computation. In the Integrated approach, we integrate branch-and-bound search into the SAT engine to achieve more effective search tree pruning and better scalability. Performance evaluation shows that the Integrated approach outperforms the LBBD approach by a large margin.