Linear Satisfiability Algorithm for 3CNF Formulas of Certain Signaling Networks

Abstract

A simple model of signal transduction networks in molecular biology consists of CNF formulas with two and three literals per clause. A necessary condition for correctness of the network model is satisfiability of the formulas. Deciding satisfiability turns out to be $NP$ -complete. However, for a subclass that still is of practical interest, a linear satisfiability algorithm and related characterization of unsatisfiability can be established. The subclass is a special case of so-called closed sums of CNF formulas.

Keywords

SAT algorithm 2CNF 3CNF closed sum