Post Correspondence Problem (PCP) is a classic example of an undecidable problem, with various heuristic algorithms proposed to tackle its instances. In this study, we focus on solving a particular subset of instances known as \textit{PCP[3,4]}. We introduce a novel algorithm that leverages regular language and automata theory to identify inductive invariants within the transition systems associated with these instances, enabling us to demonstrate the unsolvability of instances. Additionally, we manually found some inductive invariants using an interactive tool developed specifically for this purpose. As a result, we successfully solved all instances except for three. To ensure the correctness of our results, we generated proofs for each instance that can be verified using Isabelle/HOL.