1)Making naiveencoder and encoding graph use tuner 2)Adding timeout to the sat solver...