Fuqi Jia (贾富琦)

State Key Laboratory of Computer Science
Institute of Software, Chinese Academy of Sciences
#4 South Fourth St., Zhong Guan Cun
Beijing, China 100190
Email: jiafq@ios.ac.cn

Fuqi Jia

Short Bio

I received my Ph.D. in Computer Science and Technology from the University of Chinese Academy of Sciences (UCAS) in 2026, where I conducted my research at State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, under the supervision of Prof. Jian Zhang. From 2024 to 2025, I served as a visiting PhD student at Stanford University, supervised by Clark Barrett. Before that, I received my B.S. degree in Computer Science and Technology from Jilin University (JLU) in 2020.

My research interests include the theory, algorithm and application of automated reasoning, constraint solving and optimization, as well as the integration of symbolic reasoning and machine learning.

Education

University of Chinese Academy of Sciences
Ph.D.
2020-2026
Stanford University
Visiting Ph.D. Student
2024-2025
Jilin University
B.S. Student
2016-2020

Recent News

Publications

(* indicates equal contribution)

AllDiff-LS: Solving Alldifferent Constraints with Efficient Local Search
Rui Han, Minghao Liu, Yuhang Dong, Fuqi Jia, Yiyuan Wang, Feifei Ma, Minghao Yin, Jian Zhang
Frontiers of Computer Science (FCS), 2026
PDF
ConstraintLLM: A Neuro-Symbolic Framework for Industrial-Level Constraint Programming
Weichun Shi, Minghao Liu, Wanting Zhang, Langchen Shi, Fuqi Jia, Feifei Ma, Jian Zhang
Conference on Empirical Methods in Natural Language Processing (EMNLP), 2025
PDF Code
A Complete Algorithm for Optimization Modulo Nonlinear Real Arithmetic
Fuqi Jia, Yuhang Dong, Rui Han, Pei Huang, Minghao Liu, Feifei Ma, Jian Zhang
AAAI Conference on Artificial Intelligence (AAAI), 2025
PDF Code
A Theory-Agnostic SMT Sampling Framework
Fuqi Jia, Clark Barrett, Pei Huang, Feifei Ma and Jian Zhang
Formal Methods in Computer-Aided Design (FMCAD, Student Forum), 2024
PDF Code
Automatic Construction of HD Maps for Simulation-Based Testing of Autonomous Driving Systems
Siqi Wang, Changwen Li, Tiantian Sun, Fuqi Jia, Rongjie Yan, Jun Yan
Theoretical Aspects of Software Engineering (TASE), 2024
PDF Code
Parallel Verification for δ-Equivalence of Neural Network Quantization
Pei Huang, Yuting Yang, Haoze Wu, Ieva Daukantas, Min Wu, Fuqi Jia, Clark Barrett
International Symposium on AI Verification (SAIV), 2024
PDF Code
Investigating the Existence of Holey Latin Squares via Satisfiability Testing
Minghao Liu, Rui Han, Fuqi Jia, Pei Huang, Feifei Ma, Hantao Zhang, Jian Zhang
Pacific Rim International Conference on Artificial Intelligence (PRICAI), 2023
PDF Code
Suggesting Variable Order for Cylindrical Algebraic Decomposition via Reinforcement Learning
Fuqi Jia*, Yuhang Dong*, Minghao Liu, Pei Huang, Feifei Ma, Jian Zhang
Conference on Neural Information Processing Systems (NeurIPS), 2023
PDF Code
Improving Bit-Blasting for Nonlinear Integer Constraints
Fuqi Jia, Rui Han, Pei Huang, Minghao Liu, Feifei Ma, Jian Zhang
ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), 2023
🏅 ACM SIGSOFT Distinguished Paper Award
PDF Code
PSMT: Satisfiability Modulo Theories Meets Probability Distribution
Fuqi Jia*, Rui Han*, Xutong Ma, Baoquan Cui, Minghao Liu, Pei Huang, Feifei Ma, Jian Zhang
IEEE/ACM International Conference on Automated Software Engineering (ASE, NIER Track), 2023
PDF Code
NRAgo: Solving SMT(NRA) Formulas with Gradient-based Optimization
Minghao Liu*, Kunhang Lv*, Pei Huang, Rui Han, Fuqi Jia, Yu Zhang, Feifei Ma, Jian Zhang
IEEE/ACM International Conference on Automated Software Engineering (ASE, Tool Demo Track), 2023
PDF Code
Can Graph Neural Networks Learn to Solve the MaxSAT Problem?
Minghao Liu, Pei Huang, Fuqi Jia, Fan Zhang, Yuchen Sun, Shaowei Cai, Feifei Ma, Jian Zhang
AAAI Conference on Artificial Intelligence (AAAI), Student Abstract and Poster Program, 2023
🏅 Best Student Abstract Honorable Mention Award
PDF Code
ε-weakened Robustness of Deep Neural Networks
Pei Huang*, Yuting Yang*, Minghao Liu, Fuqi Jia, Feifei Ma, Jian Zhang
ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), 2022
PDF Code
Word Level Robustness Enhancement: Fight Perturbation with Perturbation
Pei Huang*, Yuting Yang*, Fuqi Jia, Minghao Liu, FeiFei Ma, Jian Zhang
AAAI Conference on Artificial Intelligence (AAAI), 2022
PDF Code

Selected Awards & Scholarships

SMT-COMP 2026, Single Query Track, Largest Contribution Award for UNSAT Performance (Solver: Xolver), 2026.07.
SMT-COMP 2026, Single Query Track, Winner of QF_NIRA in Sequential, Parallel, UNSAT and 24s Performance (Solver: Xolver), 2026.07.
Outstanding Graduate of Beijing, 2026.
Outstanding Graduate of UCAS, 2026.
BYD Scholarship, 2025.12.
Outstanding Doctoral Student, Chinasoft 2023, 2023.11.
National Scholarship of China, 2023.10.
First Prize Scholarship of UCAS, 2023.10.
SMT Competition, QF_NIA Single Query / Model Validation Track, 2nd Place (Main Author), 2023.08.
ACM SIGSOFT Distinguished Paper Award, ISSTA 2023, 2023.07.
Best Student Abstract Honorable Mention Award, AAAI 2023, 2023.02.

Presentations

Conference Talk Improving Bit-Blasting for Nonlinear Integer Constraints, ISSTA 2023, Virtual Event.
Conference Talk PSMT: Satisfiability Modulo Theories Meets Probability Distribution, ASE 2023, Luxembourg.
Conference Talk NRAgo: Solving SMT(NRA) Formulas with Gradient-based Optimization, ASE 2023, Luxembourg.
Seminar Talk Satisfiability and Deep Learning, Applied Mathematics Seminar for Youth, Peking University, Beijing, China.
Seminar Talk Solving Reasoning Problems with Neuro-Symbolic Methods, Dagstuhl Seminar 23471, Dagstuhl, Germany.
Seminar Talk Improving SMT Solving via Incorporating More Techniques, Dagstuhl Seminar 23471, Dagstuhl, Germany.
Conference Talk A Theory-Agnostic SMT Sampling Framework (Poster), FMCAD 2024, Prague, Czech Republic.

Professional Service

Conference Reviewer NeurIPS 2025 & 2026, AAAI 2026, IJCAI 2026.

Open Source Projects

Xolver
A Satisfiability Modulo Theories (SMT) solver.
Code
SOMTParser
A C++ SMT/OMT parser library for parsing and processing SMT-LIB / OMT format formulas.
Code
BLAN
A bit-blasting solver for nonlinear integer constraints.
Code
CDCL(OCAC)
A complete algorithm for optimization modulo nonlinear real arithmetic.
Code

Last updated: 08/14/2026