SAF: SAT-Based Attractor Finder in Asynchronous Automata Networks

In this paper, we present a SAT-based Attractor Finder (SAF) which computes attractors in biological regulatory networks modelled as asynchronous automata networks. SAF is based on translating the problem of finding attractors of a bounded size into a satisfiability problem to take advantage of state-of-the-art SAT encodings and solvers. SAF accepts an automata network and outputs attractors in ascending size order until the bound is reached. SAF's main contribution is providing an alternative to existing attractor finders. There are cases where it is able to find some attractors while other techniques fail to do so. We observed such capability on both automata networks and Boolean networks. SAF is simple to use: it is available as a command line tool as well as a web application. Finally, SAF being written in Scala, it can run on any operating system with a Java virtual machine when combined with the SAT solver Sat4j.