Design automation and space-time reduction for surface-code logical operations using a SAT-based EDA kernel compatible with general encodings

Fault-tolerant quantum computers (FTQCs) based on surface codes and lattice surgery have been widely studied, and there is strong demand for a framework that can identify logical operations with low space-time cost, verify their functionality and fault tolerance, and demonstrate their optimality within a given search space, much like electronic design automation (EDA) in classical circuit design. In this paper, we propose KOVAL-Q, an EDA kernel that verifies and optimizes surface-code logical operations by formulating them as a satisfiability (SAT) problem. Compared with existing SAT-based frameworks such as LaSsynth, our method can handle logical qubits with more flexible surface-code encodings, both as target configurations and as intermediate states. This extension enables the optimization of advanced layouts, such as fast blocks, and broadens the search space for logical operations. We demonstrate that KOVAL-Q can determine the minimum execution time of fundamental logical operations in given spatial layouts, such as d-cycle logical CNOTs and 2d-cycle patch rotations. Their use reduces the execution time of widely studied FTQC applications by about 10% under a simplified scheduling model. KOVAL-Q consists of three subkernels corresponding to different types of constraints, which facilitates its integration as a submodule into scalable heuristic frameworks. Thus, our proposal provides an essential framework for optimizing and validating core FTQC subroutines.