Modern On-Board Diagnostics (OBD-II) systems capture rich multivariate data reflecting real-world vehicle dynamics. Yet, conventional clustering algorithms such as KMeans often produce physically inconsistent operating regimes—such as idle RPMs at highway speeds or throttle levels beyond feasible bounds—because they rely purely on statistical compactness. This paper presents KMeans–SMT, a physics-constrained clustering framework that embeds Satisfiability Modulo Theories (SMT) reasoning into the KMeans optimization loop. The method enforces domain-specific physical relationships, including idle-RPM consistency, gear-ratio coherence, and operational bound validity, ensuring that each cluster centroid corresponds to a physically realizable driving state. Unlike projection- or penalty-based baselines, KMeans–SMT achieves zero constraint violations by construction while maintaining competitive clustering quality. Experiments on real OBD-II datasets ( \(\sim \) 2.7 million samples, downsampled to 80 000) demonstrate that KMeans–SMT attains a Silhouette score of 0.583 with full physical compliance, whereas unconstrained variants exhibit multiple physics-rule violations. These findings highlight how coupling symbolic reasoning with unsupervised learning yields interpretable, physically trustworthy, and safety-aligned clustering for intelligent vehicle analytics and next-generation transportation systems.