To add to this for the author and other readers: SAT restricted to an individual instance is always constant time.