Very interesting. For me the key question is whether this kind of agent can generalize to real SAT application domains, not only benchmark instances. In problems like timetabling, encoding choices, auxiliary variables, and branching strategy can matter a lot. If it can help there too, this is a very meaningful direction.