Looking for Signs: Reasoning About FOBNNs Using SAT

TL;DR

This paper introduces a SAT-based method for analyzing First-Order Boolean Networks with Non-deterministic updates, enabling practical reasoning about their transition graphs and fixed points, thus advancing their empirical study.

Contribution

It presents a sound, efficient SAT encoding of FOBNNs' transition relations, facilitating practical analysis and comparison with reaction network semantics.

Findings

SAT encoding enables reasoning on large FOBNN models

Efficient computation of fixed points in FOBNNs

Enhanced understanding of FOBNNs' relation to reaction networks

Abstract

First-Order Boolean Networks with Non-deterministic updates (FOBNN) compute a boolean transition graph representing the absence and presence of species over time. The utility of FOBNNs has been justified by their theoretical soundness with respect to the Euler simulation of the differential equations. However, we lack practical means to work with FOBNNs and an empirical evaluation of their properties. We present a sound and efficient reduction of the first-order FOBNN transition relation to a propositional logic formula. This makes it possible to use modern SAT solvers to reason on the full transition graph, even for large models. We use this encoding to assess the feasibility and efficiency of practical reasoning with FOBNNs. To do so, we focus on the computation of fixed points. We also compare the transition graphs obtained via FOBNNs to those computed by the classic boolean semantics of reaction networks. Overall, our encoding opens new directions for the analysis of FOBNNs and deepens the understanding of their relationship with reaction networks.