I came across this term called "Satisfiability Modulo Theories", which when I Googled it, was something that is related to various theories on low level languages. How does this help in discovering 0-days? I also saw people using something called "Z3 solver" could somebody give a shorter explanation of what this is?
Satisfiability Modulo Theories (SMT) are mathematical concepts that looks at how something can be computed. These theories relates to things that you will find in many programming languages like real and integer numbers, lists, etc and which are essential to computers.
SMT solvers (like Z3) are computer programs that automatically generate proofs for related mathematical problems. So, if you have a problem statement (a theorem) that you can encode in the input language for such a solver, the solver will return a proof, if possible.
An application area for SMT solvers is an approach called 'symbolic execution'. In symbolic execution, you are less interested in the actual execution run of a computer program, but to explore what are general executions under different inputs. For example, in an actual computation, you would be interested to get a number as a definitive output. In symbolic execution you would be more interested in more general things like what is the type of the output.
Symbolic execution can be used to perform security analyses like taint checking, i.e., trace an input throughout the execution of a program. This helps to discover all kind of vulnerabilities, including zero-day exploits.