Predictor Set Inference using SAT - Logic Synthesis for Genetic Diseases - page 27

Table 2.1 Example 3-Gene
partial state transition table

Current state Next state

x 1 x 2 x 3 y 1 y 2 y 3

0 1 0 1 1 0

1 1 0 0 1 0

1 1 1 1 1 1

2.4 Problem Formulation and SAT Formulation

Given gene expression data (a set of unordered attractor states) as input, we would
like to determine the best predictor set. We first present an outline of our SAT-based
algorithm, and then explain the steps through a simple example.
The algorithm has three main steps.

1. SAT Formula Construction for Predictor Set: In this step, attractor states are
ordered into attractor cycles in all possible ways. For each possible ordering of
attractor states into attractor cycles, all possible predictors are found and a CNF
is generated encoding valid predictor sets.
2. All-SAT: Each attractor ordering from step 1 generates a CNF which is solved
for All-SAT. All satisfying cubes are recorded, where each satisfying cube cor-
responds to a predictor set. The first two steps are repeated for all attractor cycle
orderings.
3. Predictor Set Selection: Statistical analysis on the All-SAT results determines
the most frequent (likely) predictor set for the GRN. This step is explained in
Sect. 2.5 .

To illustrate the SAT-based algorithm, we apply it to a simple example with three
genes ( g 1 , g 2 , g 3 ) and gene expression data with three lines (010, 110, 111). The
present state of these genes is represented by the variables <x 1 , x 2 , x 3 > and the
next state is represented by the variables <y 1 , y 2 , y 3 > . We assume each line was
measured in steady state and therefore is an attractor state.
We order (or arrange) the attractor states into attractor cycles for which there are six
possibilities for our example. One ordering is with each attractor state transitioning
to itself with a self-edge, resulting in three singleton attractor cycles. Two possible
orderings result when all three attractor states form a single attractor cycle of length
three. The last three possible orderings have two attractor cycles, one cycle with
length two and the other cycle of length one. We focus our example on an ordering
with two attractor cycles (010 → 110 → 010 → ... ) and (111 → 111 → ... )as

shown in Table 2.1 .

2.4.1 Partial State Transition Table

For each valid attractor cycle ordering, a partial state transition table is constructed,
containing the attractor states. Table 2.1 shows the partial state transition table for