Zero-Knowledge Proof-Enabled SAT Co-processor for Blockchain Systems

Abstract

This thesis explores the possibility of building classical SAT solvers in Circom Domain Specific Language to create zero-knowledge proofs (ZKPs) usable in blockchain contexts. I implemented DPLL and Chaff as arithmetic circuits within Circom and analyze them based on constraint count, proving delay, and zk-SNARK verification layers. With this evaluation, the aim is to determine the feasibility of solvers integration into off-chain computation systems and rollup-centric architectures on Ethereum. The findings indicate that incorporating SAT solvers within zero-knowledge circuits is achievable though some degradation in efficiency occurs based on algorithm used and input representation. This research provides a thorough assessment of known SAT methods across an unconventional boundary, linking symbolic logic with blockchain technologies reliant on zk-SNARKs.