While Large Language Models (LLMs) perform well on arithmetic word problems, they remain brittle to adversarial perturbations like irrelevant distractors or contradictory facts. To address this, we introduce ReThink, a training-free neuro-symbolic framework that formulates adversarial arithmetic reasoning as a Weighted MaxSAT/MaxSMT problem. ReThink uses a four-stage pipeline: it explicitly decomposes problems to strip noise, encodes the mathematical core as confidence-weighted soft constraints in the Z3 theorem prover, and cross-verifies the formal solution against a parallel Chain-of-Thought (CoT) path. This formulation can sacrifice lower-weight conflicting statements while satisfying higher-weight constraints. Evaluated on a balanced 2,400-example subset of GSM-Plus, ReThink with GPT-4.1 achieves 81.62% adversarial accuracy, outperforming CoT, PAL, and Self-Verification. It narrows the robustness gap to 14.69 percentage points while achieving 96.31% clean accuracy.