In the integrated modular avionics (IMA), strict space and time partitioning management ensures that different applications running on the same module can share processing resources. According to the requirements of system hardware resources and applications, the multitype constraints of partition are defined, which makes the partitioning and timedivision access scheduling become complex combinatorial optimization problems. By combining the preprocessing of partition allocation with satisfiability modulo theories (SMT) to solve the scheduling table, it is possible to reduce the number of variables at the time of assertion and partition scheduling, and improve the efficiency of the solution. The preprocessing process uses the maximum clique problems algorithm, and then transfer the rest of the district constraints into the logical expression that SMT can identify, using the formal solution to get the time of each partition scheduling. The feasibility of this method is verified by different numerical examples, and the advantage of the preprocessing process for quickly judging the satisfaction requirement and shortening the solution time is illustrated.