On: The Silent (R)evolution of SAT

[doetoe]

I'm not an expert in any of these, but in the past few years, in addition to the success of LLM's for natural language processing, I have repeatedly read about the impressive advances in SAT solvers and in proof assistants. Given how impressive LLM's are in spite of their inability to reliably perform reasoning tasks or follow instructions with logical strictness, I wonder how much more impressive it could get if such systems got integrated

[sanxiyn → doetoe]

You will enjoy "Maieutic Prompting: Logically Consistent Reasoning with Recursive Explanations". It prompts LLM to generate tree of explanations and run MAX-SAT solver over it: https://arxiv.org/abs/2205.11822

[doetoe → sanxiyn]

Thanks, I'll check it out!