SMTrap: Cost-Effective DoS Attacks Against Large Reasoning Models via SMT Conflict Guidance

Existing LRM-DoS methods rely heavily on model feedback to synthesize attack queries, requiring either repeated queries to the target model or training a dedicated attack model. These expensive operations severely weaken attack leverage. In this paper, we propose search amplification, a novel, model-feedback-free LRM-DoS paradigm. It employs the conflict count derived from an Satisfiability Modulo Theories (SMT) solver as a low-cost external signal to guide the synthesis of inference-heavy Constraint Satisfaction Problem (CSP) instances. Our key observation is that LRMs depend on trial-and-backtracking search when solving CSPs, where higher SMT conflict counts on a given CSP instance positively correlate with more extensive LRM backtracking search and substantially longer output trajectories. Building on this finding, we propose textscSMTrap, a lightweight, CPU-only framework. Guided by SMT conflict counts, textscSMTrap generates inference-heavy CSP queries without model queries, attack-model training, or GPU computation. Evaluations across seven frontier models demonstrate the state-of-the-art LRM-DoS capability of textscSMTrap, producing DoS effects multiple times stronger than existing baselines. To mitigate the threat of textscSMTrap, we demonstrate a tool-based mitigation that significantly cuts token usage.