Efficient algorithms for automated reasoning and large language models