SAT-Based Optimization Framework for Electric Vehicle Charging Station Routing Under Real-World Constraints

With the rapid adoption of electric vehicles (EVs), optimizing charging infrastructure and route planning has become increasingly crucial. Traditional methods such as Linear Programming (LP) have been widely used to address these challenges. However, these approaches often struggle with scalability, computational efficiency, and the ability to handle complex logical constraints involving multiple decision factors like distance, time, cost, battery levels, and charging station compatibility. To overcome these limitations, this study proposes a novel Boolean Satisfiability (SAT)-based optimization framework for intelligent EV charging station recommendation. Unlike conventional approaches, the proposed model encodes real-world constraints into Conjunctive Normal Form (CNF) using De Morgan’s Theorem, allowing efficient processing through the CP-SAT solver. This logical transformation enables the systematic representation of intricate relationships between variables, ensuring better compatibility and computational efficiency. The SAT-based framework was applied to intercity EV routing scenarios, where it demonstrated substantial improvements over traditional methods in terms of route optimization, cost reduction, and charging station relevance. Notably, the SAT model was effective in avoiding redundant charging recommendations, selecting only those stations necessary to complete the route while satisfying all energy and infrastructure constraints. Moreover, the solver showed rapid convergence and greater adaptability under varied operational scenarios. In conclusion, this study highlights the effectiveness of SAT-based modeling—particularly its CNF formulation and logical expressiveness—in delivering a scalable, intelligent, and efficient solution for real-time EV route planning and charging station optimization.