About Me

I'm Zhiwei Zhang (张志伟, [dʒ-weɪ], he[dge wai]ve), a fifth-year Computer Science Ph.D. student at Rice University working with Prof. Moshe Vardi. I am also co-advised by Prof. Anastasios Kyrillidis . My current research interests are in SAT/MaxSAT Solving, Bridging Discrete and Continuous Optimization and Logic in AI.

Previously, I received my B.S. from Computer Science Dept. in Nanjing University, advised by Prof. Gong Cheng and did some work on Knowledge Graph and Question Answering. I grew up in a beautiful city, Tianshui .

Here is my CV .

I am actively seeking for a post-doc position in formal methods and/or neural-symbolic AI. Please reach out to me if you know any oppurtunities!


Rice University Sep 2018 - May 2024 (expected)

Ph.D. in Computer Science
Machine Learning with Graphs (Seminar), Fall 2021
Cloud Computing, Fall 2021
Parallel Computating, Spring 2020
Optimization: Algorithms, Complixity, and Approximations, Fall 2019
Computer Systems Architecture, Fall 2019
Statistical Machine Learning, Spring 2019
Probilitistic Algorithms and Data Structures, Spring 2019
Automated Program Verification (Seminar), Spring 2019, 2020, 2021
Oral Communication Skills, Spring 2019
Logic in Computer Science, Fall 2018
Topics in Programming Languages and Formal Methods, Fall 2018
Design and Analysis of Algorithms, Fall 2018

Rice University, Sep 2018 - Jan 2020

M.S. in Computer Science
Thesis: Solving Hybrid Boolean Constraints by Fourier Expansions and Continuous Optimization

Nanjing University, Sep 2014 - Jun 2018

B.S. in Computer Science (National Elite Program)


* indicates author list has been sorted alphabetically by last name and Zhiwei Zhang is the main contributor

Journal Papers

Solving Hybrid Boolean Constraints in Continuous Space via Fourier Expansions
*Anastasios Kyrillidis, Anshumali Shrivastava, Moshe Vardi, Zhiwei Zhang
Artificial Intelligence (AIJ), 2021

Conference Papers

Solving Quantum-Inspired Perfect Matching Problems via Tutte's Theorem-Based Hybrid Boolean Constraints
*Moshe Vardi, Zhiwei Zhang
IJCAI 2023
Awarded “Quantum-Graph Best-Paper of 2023” by Max Planck Institute.

On Continuous Local BDD-Based Search for Hybrid SAT Solving
*Anastasios Kyrillidis, Moshe Vardi, Zhiwei Zhang
AAAI 2021
We explore the potential of continuous local search (CLS) in SAT solving by proposing a novel approach for finding a solution of a hybrid system of Boolean constraints. The algorithm is based on CLS combined with belief propagation on binary decision diagrams (BDDs). Our framework accepts all Boolean constraints that admit compact BDDs, including symmetric Boolean constraints and small-coefficient pseudo-Boolean constraints as interesting families. We propose a novel algorithm for efficiently computing the gradient needed by CLS. We study the capabilities and limitations of our versatile CLS solver, GradSAT, by applying it on many benchmark instances. The experimental results indicate that GradSAT can be a useful addition to the portfolio of existing SAT and MaxSAT solvers for solving Boolean satisfiability and optimization problems.

FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints
*Anastasios Kyrillidis, Anshumali Shrivastava, Moshe Vardi, Zhiwei Zhang
AAAI 2020 (oral)
The 2-page version of this paper was also accepted by the Student Abstract Track of AAAI 2020 (finalist of best student abstract) .
We design FourierSAT, an incomplete SAT solver based on Fourier analysis of Boolean functions, a technique to represent Boolean functions by multilinear polynomials. By a reduction from SAT to continuous optimization, we propose an algebraic framework for solving systems consisting of different types of constraints. The idea is to leverage gradient information to guide the search process in the direction of local improvements. Empirical results demonstrate that FourierSAT is more robust than other solvers on certain classes of benchmarks.

Towards Answering Geography Questions in Gaokao: A Hybrid Approach
Zhiwei Zhang, Lingling Zhang, Hao Zhang, Weizhuo He, Zequn Sun, Gong Cheng, Qizhi Liu, Xinyu Dai, Yuzhong Qu
In Proceedings of the 2018 China Conference on Knowledge Graph and Semantic Computing (CCKS) 2018.
Answering geography questions in a university’s entrance exam (e.g., Gaokao in China) is a new AI challenge. In this paper, we analyze the difficulties in problem understanding and solving, suggesting the necessity of developing novel methods. We present a pipeline approach which mixes information retrieval techniques with knowledge engineering and exhibits an interpretable problem solving process. Our implementation integrates question parsing, semantic matching, and spreading activation over a knowledge graph to generate answers. We report its promising performance on a representative sample of 1,863 questions used in real exams. Our analysis of failures reveals a number of open problems to be addressed in the future.


Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs
Yunuo Cen, Zhiwei Zhang, Xuanyao Fong
In submission
Quantum-Inspired Perfect Matching under Vertex-Color Constraints
*Moshe Vardi, Zhiwei Zhang
In submission
Understanding Boolean Function Learnability on Deep Neural Networks: PAC Learning Meets Neurosymbolic Models
Marcio Nicolau, Anderson Tavares, Zhiwei Zhang , Joao Flach, Luis Lamb, Moshe Vardi.
In submission
DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving
*Anastasios Kyrillidis, Moshe Vardi, Zhiwei Zhang
In submission
Momentum-inspired Low-Rank Coordinate Descent for Diagonally Constrained SDPs
Junhyung Lyle Kim, Jose Antonio Lara Benitez, Mohammad Taha Toghani, Cameron Wolfe, Zhiwei Zhang (alphabetical order), Anastasios Kyrillidis
In submission


Invited/Conference Talks

"Quantum Inspired Perfect Matching Problems"

Recorded Talk for the Award, Nov 22, 2023
Stanford University, Sept 11, 2023
IJCAI 2023, Macau, Aug 25, 2023
Southeastern Louisiana University, Mar 21, 2023

"Searching Inside the Box: A Continuous-Local-Search Approach for Hybrid SAT Solving"

National University of Singapore, May 18, 2023
UCLA, Nov. 23 , 2022
Simons Institute, Berkeley, Workshop of Theoretical Foundations of SAT/SMT Solving, March 17, 2021
"Hybrid SAT Solving by Continuous Optimization", MURI Meeting, Nov 20, 2020

"On Continuous Local BDD-Based Search for Hybrid SAT Solving"

AAAI 2021, virtual conference, Feb, 2021

"FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints"

AAAI 2020 (session: Satisfiability), New York Feb 9, 2020

Group Meeting/Class Presentations

"Resolution and Conflict Driven Clause Learning", COMP 607, Rice University Feb 12, 2023

"Computing Discrepancy (Based on Chuchu Fan's Thesis)", COMP 607, Rice University Feb 12, 2022

"Visualizing High-Dimensional Boolean Functions" ("2021-22 Best Research Presentation of The Year" (People's Choice)) , Graduate Student Research Seminar, Rice University Nov 22, 2021

"DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving, LAPIS meeting, Rice University Aug 11, 2021

"Logical Neural Networks" (Based on the IBM Research paper), LAPIS meeting, Rice University Mar 23, 2021

"The Satisfiability Problem: A Brief Tutorial on SAT Algorithms", COMP 607, Rice University Feb 12, 2021

"Correct-by-synthesis reinforcement learning with temporal logic constraints (Based on Min Wen's Thesis)", COMP 607, Rice University Feb 12, 2020

"Hadamard-Walsh-Fourier Transform: History and applications", LAPIS meeting, Rice University May 20, 2020

"Solving Hybrid Boolean Constraints Continuously", Graduate Student Research Seminar, Rice University Oct 7, 2019

"Fourier Analysis on Boolean Functions and its Applications", LAPIS meeting, Rice University Oct 18, 2018

"Moser’s Algorithmic LLL", LAPIS meeting, Rice University Sep 06, 2018



Guest lecturer of COMP 409/509: Logic in Computer Science, Rice University 2023 Fall

TA of Computer Science/Data Science Bridge course, Rice University 2021 Summer

TA of COMP 545: Advanced topics in optimization, Rice University 2020 Spring

TA of COMP 582: Design and Analysis of Algorithms, Rice University 2019 Fall

TA of COMP 408/548: Verified Programming, Rice University 2019 Spring

TA of Problem Solving(III), Nanjing University 2017 Fall


  • Music: singing, playing piano
  • (e)Sports: table tennis, badminton, Dota, FIFA

© 2015 Curriculum Vitae All Rights Reseverd | Design by W3layouts