We present an advanced SAT-based approach to the task and message allocation problem of distributed real-time systems. In contrast to the heuristic approaches usually applied to this problem, our approach is guaranteed to find an optimal allocation for realistic task systems running on complex target architectures. Our method is based on the transformation of such scheduling problems into nonlinear integer optimization problems. The core of the numerical optimization procedure we use to discharge those problems is a solver for arbitrary boolean combinations of integer constraints. While the determination of the task and message placement is done within the satisfiability checking based solver, checking for feasibility w.r.t real-time requirements is performed in a specialized real-time engine under control of the satisfiability solver. Optimal solutions are obtained by imposing a binary search scheme on top of that solver. Experiments show the applicability of our approach to industrial-size task systems.