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.

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.

Range anxiety among electric vehicle (EV) drivers stems less from battery capacity itself than from the difficulty of trusting a dashboard range estimate and choosing, quickly, among charging options of unequal speed, price and compatibility. The authors' earlier work encoded this choice as a Boolean Satisfiability problem solved once, offline, using a fixed energy-consumption rate on short intra-city routes. This paper extends that formulation to Predictive Constraint-Verified EV Routing (PC-EVR), a system that (i) predicts a vehicle's achievable range from live telemetry using a trained XGBoost regressor rather than a fixed rate, and (ii) re-solves the next charging decision at every real stop as a Weighted Partial MaxSAT instance, using the RC2 core-guided solver, in which a 20% state-of-charge floor is a non-negotiable constraint that filters candidates outright rather than a factor the solver merely weighs in. The range predictor is selected after a controlled, identical-split comparison against Linear Regression, Random Forest and a neural network, and its selection is validated by a dedicated ablation study rather than an offline error metric alone. PC-EVR is benchmarked against two purpose-built greedy baselines (nearest-station, cheapest-station) under identical safety and traffic assumptions, across five real long-distance Indian trips and India's national government charging-station registry of 39,641 stations. The proposed system completes every trip without a single safety-constraint violation while reducing average trip time by approximately 8.7 hours against the nearest-station baseline and 21.6 hours against the cheapest-station baseline. The ablation study further shows that routing quality is insensitive to small prediction-accuracy differences among tree- and network-based models but degrades measurably once accuracy falls below a threshold, a finding with direct implications for range-model selection in future systems.