Research.

Four directions in algorithms, optimization, and computing.

FourierSAT

Continuous methods for hybrid SAT solving.

Graph constraints, Ising models, and quantum optimization.

Global structure and local geometry, made visible.

CUDA-accelerated algorithms for hard mathematical problems.

Open-source tool directory

A SAT/MaxSAT solver based on continuous local search for hybrid Boolean constraints.

A C++ extension of FourierSAT that accepts pseudo-Boolean constraints and uses BDDs to accelerate gradient computation.

A dynamic-programming-based C++ solver for generalized MaxSAT problems.

An accelerated implementation of the Mixing Method based on semidefinite programming.

Implementations for perfect-matching graph-decision problems with quantum-computing applications.