Ask HN: GPT for classical CNF-SAT problem

I am wondering if anyone is working on building a large Generative Pre-trained Transformer (GPT) model trained on Boolean CNF Formula equivalences (for example: reduction to unit clauses, tautologies, fallacies etc.,) that may be used to simplify a Boolean CNF Formula and maybe improve SAT solvers.