Minghao Liu   (刘明昊) Department of Computer Science University of Oxford Wolfson Building, Parks Road Oxford OX1 3QD, UK Email: minghao.liu@cs.ox.ac.uk [CV] [Google Scholar] [DBLP] [GitHub]

Short Bio

I am currently a Postdoctoral Research Associate at the University of Oxford, under the supervision of Prof. Marta Kwiatkowska (since 2024.10) and Dr. Andrew Cropper (2023.10 – 2024.09). Before that, I received PhD degree in Computer Science and Technology from the University of Chinese Academy of Sciences (UCAS) in 2023, and did my research at State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, under the supervision of Prof. Jian Zhang. I received BSc degree in Computer Science and Technology from Northeast Normal University (NENU) in 2017.

My research interests include the theories, algorithms and applications of automated reasoning, constraint programming and combinatorial optimization, as well as the integration of symbolic reasoning and machine learning.

News

• [2025.09] Our paper on local search for alldifferent constraints has been published by FCS.
• [2025.08] Our paper on LLMs for constraint programming has been accepted by EMNLP 2025.
• [2024.12] Two papers on knowledge refactoring and OMT(NRA) solving have been accepted by AAAI 2025.
• [2024.10] I presented our poster on GNNs for MaxSAT solving, at the Beyond the Symbols vs Signals Debate of the Royal Society, London.
• [2023.12] Our paper on solving nonlinear polynomials with RL has been accepted by NeurIPS 2023.
• [2023.11] Our paper on finding holey Latin squares has been accepted by PRICAI 2023.
• [2023.10] I started the Research Associate position at the University of Oxford.
• [2023.09] Two short papers on SMT(NRA) solving and SMT with probability distribution are accepted by ASE 2023.
• [2023.07] Our paper received the ACM SIGSOFT Distinguished Paper Award at ISSTA 2023.
• [2023.07] Our paper on bit-blasting for SMT(NIA) solving has been accepted by ISSTA 2023.

Selected 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
  
• 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
  
• Scalable Knowledge Refactoring Using Constrained Optimisation
  Minghao Liu, David M. Cerna, Filipe Gouveia, Andrew Cropper
  AAAI Conference on Artificial Intelligence (AAAI), 2025
  
• 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
  
• Suggesting Variable Order for Cylindrical Algebraic Decomposition via Reinforcement Learning
  Fuqi Jia*, Yuhang Dong*, Minghao Liu, Pei Huang, Feifei Ma, Jian Zhang
  Advances in Neural Information Processing Systems (NeurIPS), 2023
  
• 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
  
• 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), 2023
  
• 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), 2023
  
• 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
  
• 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
  
• Improving Simulated Annealing for Clique Partitioning Problems
  Jian Gao, Yiqi Lv, Minghao Liu, Shaowei Cai, Feifei Ma
  Journal of Artificial Intelligence Research (JAIR), 2022
  
• ε-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
  
• 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
  
• Modelling and Solving the Supply Marketing Order Allocation Problem with Time Consistency and Bundle Discounts
  Yupeng Zhou, Minghao Liu, Feifei Ma, Na Luo, Minghao Yin
  Journal of the Operational Research Society (JORS), 2021
  
• Efficient SAT-Based Minimal Model Generation Methods for Modal Logic S5
  Pei Huang, Rundong Li, Minghao Liu, Feifei Ma, Jian Zhang
  International Conference on Theory and Applications of Satisfiability Testing (SAT), 2021
  
• Learning the Satisfiability of Pseudo-Boolean Problem with Graph Neural Networks
  Minghao Liu, Fan Zhang, Pei Huang, Shuzi Niu, Feifei Ma, Jian Zhang
  International Conference on Principles and Practice of Constraint Programming (CP), 2020
  
• Solving the Satisfiability Problem of Modal Logic S5 Guided by Graph Coloring
  Pei Huang, Minghao Liu, Ping Wang, Wenhui Zhang, Feifei Ma, Jian Zhang
  International Joint Conference on Artificial Intelligence (IJCAI), 2019
  
• Investigating the Existence of Orthogonal Golf Designs via Satisfiability Testing
  Pei Huang, Minghao Liu, Cunjing Ge, Feifei Ma, Jian Zhang
  International Symposium on Symbolic and Algebraic Computation (ISSAC), 2019
  
• A Community-Division Based Algorithm for Finding Relations Among Linear Constraints
  Minghao Liu, Feifei Ma, Jun Yan
  International Conference on Knowledge Science, Engineering and Management (KSEM), 2018
  

Selected Awards & Scholarships

• SMT Competition, Nonlinear Real Arithmetic (QF_NRA) Track, 2nd Place, 2022.08
• First Prize Scholarship of UCAS (Top 10%), 2021.10
• Alibaba Guangdong Intelligent Manufacturing Innovation Contest, 3rd Place, 2019.12
• The NENU Medalist (The highest honor for undergraduate students; Top 0.5%), 2017.06
• ACM International Collegiate Programming Contest (ACM-ICPC) Asia Regional, Gold Medal, 2016.09
• National Scholarship of China, 2014.11

Teaching

• Foundations of Theoretical Computer Science, Teaching Assistant
  University of Chinese Academy of Sciences
  Spring 2020 & Spring 2021
• Logic and Proof, Class Tutor
  University of Oxford
  Hilary 2024 & Michaelmas 2024
• Knowledge Representation and Reasoning, Class Tutor
  University of Oxford
  Hilary 2025
• Computer-Aided Formal Verification, Class Tutor
  University of Oxford
  Michaelmas 2025
• Design and Analysis of Algorithms, Practical Demonstrator
  University of Oxford
  Hilary 2024 & Hilary 2025
• Functional Programming, Practical Demonstrator
  University of Oxford
  Michaelmas 2025
• Financial Computing with C++ Part I, Teaching Assistant
  University of Oxford
  Michaelmas 2024 & Michaelmas 2025
• Group Design Practical, Project Supervisor
  University of Oxford
  Hilary 2024 & Hilary 2025

Services

• PC Member: AAAI 2023, 2024, 2025, 2026; ECAI 2024, 2025; ICTAI 2023; SETTA 2025.
• Journal Reviewer: IEEE TNNLS; IEEE TKDE; Information Fusion; CSSE.