STP History

The STP constraint solver was written by Vijay Ganesh mostly in 2006 as part of his PhD thesis work at Stanford University under the supervision of Professor David L. Dill. Development froze in the second half of 2007 and most of 2008/2009. There was brief spurt of activity when Mike Katelman (University of Illinois, Urbana-Champaign) worked on the clausal normal form generation phase of STP while at NVIDIA during the summer of 2008. In spring of 2009 Trevor Hansen (University of Melbourne, Australia) took it upon himself to clean up parts of STP code, especially the SMTLIB parser. Vijay restarted work on STP in late summer/fall of 2009, aiming the solver at bio and crypto problems.