About Me

I'm Zhiwei Zhang (张志伟, [dʒ-weɪ], he[dge wai]ve), a third-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.

Here is my CV .


Rice University Sep 2018 -

Ph.D. in Computer Science
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, Spring 2019
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


* indicates author list has been sorted alphabetically by last name

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

On Continuous Local BDD-Based Search for Hybrid SAT Solving
*Anastasios Kyrillidis, Moshe Vardi, Zhiwei Zhang
In Proceedings of 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
In Proceedings of 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'18) 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.


Momentum-inspired Low-Rank Coordinate Descent for Diagonally Constrained SDPs
*Junhyung Lyle Kim, Jose Antonio Lara Benitez, Mohammad Taha Toghani, Cameron Wolfe, Zhiwei Zhang, Anastasios Kyrillidis
In submission


Invited Talks

"Searching Inside the Box: A Continuous-Local-Search Approach for Hybrid SAT Solving", 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

Conference Talks

"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

"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

"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


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


  • Travel grants: AAAI (2020), DIMACS Workshop-RNLSO (2019)
  • Outstanding graduate, Nanjing University, 2018
  • First Prize, National Elite Program Scholarship (top 10% in Elite Program) CS Dept., Nanjing University, 2017
  • Elite student (top 5% in university) Nanjing University, 2016
  • First Prize in Province (top 3% of all competitors), the Mathematical Competition of Senior High School of China 2013


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

© 2015 Curriculum Vitae All Rights Reseverd | Design by W3layouts