Publications.

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.

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.

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.