Why do all recent SAT solvers work on CNF instead of circuit SAT?

Question

After the release of the AIGER library to handle and-inverter graphs sometime in 2006 (I think), some circuit SAT solvers were released in 2006-2008, and in a few SAT Races/Competitions there were AIG tracks. However since then it seems the focus has been entirely on either SMT or improving clausal SAT solvers.

Intuitively to me concentrating on circuit SAT seems to make a lot of sense: Many if not most problems are more naturally expressed as circuit SAT than CNF; circuits provide structural information that cannot be reverse engineered from CNF, but circuits can always be transformed into CNF; and at least the industrially significant field of logic synthesis seems to be a particularly good fit for AIGs.

So, what happened? Did it turn out that the extra structural information does not help solvers? Was AIG-based SAT solving a failed experiment?

Answer 1

there are a lot of different angles on your question. generally agreed with your premise that looking at "structural information" in a SAT formulation ought to be an excellent research area.

• SAT encoded in CNF has been a standard for decades. it was solidified in the early-to-mid 1990s with the DIMACS format/ competitions.

• what technically is "structural information"? it may be hard to formally nail that concept down and avoid near-tautological circles. there is not really any difference between a SAT CNF encoding and and other encodings that preserve a network structure. this is embodied in the "clause/ variable graph" concepts which very many SAT solvers tend to utilize. in other words, in some rough sense, every significant SAT solver uses "structural information".

• yes, newer directions in research have focused on ASP and SMT solving which nearly actually embody the "structural information" you inquire about.

• Tseytin transformation easily converts a circuit into SAT in P time/ space for input into a standard SAT solver. it is presumably widely used in many contexts esp EE circuit contexts.

• there is some rather isolated research generally along the lines you mention but unfortunately (again along with your premise) it never seemed to develop much into a research trend. dont think that is due to lack of potential but more human factors. two favorite papers[1][2], another is to look at particular instances from areas such as "industrial instances" or "electrical engineering" instances of which there is some specialized research.

• CS purists sometimes tend to want to avoid psychology/ sociology considerations in all the mathematical abstractions, but reasonably its still a factor in computer science. you ask about research trends, which are based on human psychological factors. its possible there is some streetlight effect going on here aka "low hanging fruit". one might say/ consider that even now a few decades old, SAT algorithmic research is somewhat in its infancy, such that big questions like P vs NP seem nowhere in sight, and maybe existing research while still substantial is still just "scratching the surface".

[1] Decomposing satisfiability problems or Using graphs to get a better insight into satisfiability problems, Herwig 2006 (83pp)

[2] The constrainedness knife edge Walsh 1998