Network-on-Chip　(NoC)　is　a　promising　interconnecting　paradigm　in　the　state-of-the-art　multi-core　architectures.　Its　communication　network　can　increase　the　capacity　of　parallel　data　transfer　such　that　system　performance　is　improved.　In　the　design　of　MPSoC-based　applications,　multiple　objectives　exist,　such　as　minimizing　time　and　energy　consumption,　which　may　conflict　and　certain　trade-off　needs　to　be　evaluated.　Heuristic-based　methods　such　as　evolutionary　algorithms　are　always　adopted　to　find　near-optimal　solutions　for　such　applications.　However,　it　is　hard　to　evaluate　the　accuracy　of　those　solutions.　As　most　of　the　constraints　on　the　mapping　and　scheduling　process　of　NoCs　can　be　described　as　logic　formulas,　we　apply　SMT-based　methods　for　the　multi-objective　optimization　of　NoC-based　MPSoCs.　Moreover,　to　improve　the　scalability　of　the　optimization　problem,　we　propose　to　reduce　the　search　space　with　respect　to　the　symmetry　feature　of　NoC　architecture,　and　to　decompose　the　search　process　according　to　the　feature　of　non-dominated　solutions.　Extensive　experimental　results　from　random　and　real-case　benchmarks　demonstrate　the　accuracy　of　SMT-based　methods　in　finding　all　the　Pareto-fronts,　and　the　efficiency　of　the　proposed　strategies.　©　2019　IEEE.