SAT solvers determine whether a logical formula can be satisfied, a foundational problem in computer science. We harness this power to analyze software behavior and surface potential issues that traditional testing may overlook.
Through formal verification and invariant checking, we apply mathematical reasoning to code properties. This approach complements testing by exploring edge cases across the full state space of a program.
Our research focuses on advancing the theoretical and practical boundaries of SAT solving. By developing novel algorithms and heuristics, we push the frontier of what can be formally verified, enabling proofs over systems previously considered too complex to analyze.
We study how constraint propagation, clause learning, and decision strategies interact at scale. Each breakthrough in solver efficiency opens new classes of problems to rigorous mathematical reasoning.
Software verification, cryptographic protocol analysis, trustless autonomous systems. SAT solving supports rigorous analysis where failure is not an option, from smart contract logic and ZK proof systems to distributed consensus.
Our work pushes these boundaries further. By scaling solver performance to institutional-grade instances, we enable formal reasoning at scales that matter, millions of clauses, billions of variables, real-world complexity.