Yogev Shalmon Barzel

I am a PhD student in the Faculty of Data and Decision Sciences at the Technion — Israel Institute of Technology, advised by Alexander Nadel and Ofer Strichman.

My research focuses on SAT solvers and their applications. These days I am building GPAP, a GPU engine for Boolean constraint propagation:

GPAP GPU-Parallel (partial) Assignment Propagation

Boolean constraint propagation on the GPU: thousands of independent partial assignments, each propagated to its own fixpoint in a single kernel launch. A foundation for SAT on the GPU, and an open-source library to build on.

Code arXiv Docs

I am currently a PhD Student Researcher at NVIDIA, working in Formal Verification Development alongside my PhD — not a summer internship, but an ongoing student position. Previously, I worked as a research student at Intel Corporation in Haifa, Israel, where my work on Boolean matching (EBat) was productized as part of Intel’s library mapping flow. My work has been published at the International Conference on Theory and Applications of Satisfiability Testing (SAT) and at Formal Methods in Computer-Aided Design (FMCAD), and received the Best Student Paper Award at SAT 2025.