17
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ It's useful to keep in mind that when optimizing a low level program for speed and memory usage, there's something to be said for simplicity, e.g. it's extremely easy to represent and manipulate a CNF formula in C or C++. $\endgroup$ – cody Mar 7 '17 at 17:29
  • $\begingroup$ encourage further discussion in Computer Science Chat $\endgroup$ – vzn Mar 7 '17 at 19:08
4
$\begingroup$

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

$\endgroup$
  • $\begingroup$ it looks like further research into AIG has lately gone in the direction of MIGs, Majority Inverter Graphs eg Optimizing Majority-Inverter Graphs With Functional Hashing / Soeken et al (2016), the ref can be mined for further refs $\endgroup$ – vzn Mar 7 '17 at 19:40
  • $\begingroup$ another angle: treewidth is a significant circuit-like "structural property" and has been studied extensively wrt SAT hardness, with ongoing work. this work tends to be more theoretical and havent heard it being used in SAT solvers directly but it seems quite plausible that various SAT solver heuristics are actually intrinsically related to or correlated with treewidth. $\endgroup$ – vzn Mar 8 '17 at 4:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.