Evaluating SAT Accelerations for Cryptanalytic Trail Search

SAT-based techniques have become a powerful tool for automated differential and linear trail search in symmetric cryptanalysis. Their practical efficiency, however, depends strongly on both solver behavior and the way pruning information is encoded. In this work, we revisit SAT-based trail search from a solver-centric perspective, focusing on two aspects: lightweight portfolio-style parallelization and an end-to-end evaluation of Matsui-based hybrid acceleration frameworks. First, using Kissat on PRESENT and RECTANGLE, we show that the —-unsat preset usually gives the best overall performance in full-round bound computations, while the —-sat preset does not consistently dominate even on satisfiable instances. Motivated by this, we propose a low-parallelism portfolio strategy that runs the —-sat and —-unsat presets in parallel and stops once either finishes. For PRESENT, RECTANGLE, and GIFT-64, this simple strategy typically reduces runtime to about \(50\%\) – \(70\%\) of the —-default baseline and can be competitive with, or even faster than, the portfolio solver Plingeling on long-running instances. Second, we compare two Matsui-based acceleration frameworks by Sun et al. and Wang et al., explicitly including both SAT-solving time and the MILP overhead in Wang et al.’s two-stage method. Under matched resource constraints, the apparent advantage of the MILP-based approach is substantially reduced and can even disappear. Overall, our results underline the importance of holistic runtime evaluation for hybrid cryptanalytic frameworks and show that simple solver-level strategies can provide practical acceleration for SAT-based trail search.