You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

Linear Satisfiability Algorithm for 3CNF Formulas of Certain Signaling Networks

Article type: Research Article

Authors: Haus, Utz-Uwea; * | Truemper, Klausb | Weismantel, Robertc; *

Affiliations: [a] Institute for Mathematical Optimization, Otto-von-Guericke University Magdeburg, 39106 Magdeburg, Germany. E-mail: haus@imo.math.uni-magdeburg.de | [b] Department of Computer Science University of Texas at Dallas, Richardson, Texas 75080, USA. E-mail: truemper@utdallas.edu | [c] Institute for Mathematical Optimization, Otto-von-Guericke University Magdeburg, 39106 Magdeburg, Germany. E-mail: weismantel@imo.math.uni-magdeburg.de

Note: [*] Supported by FORSYS grant of the German Ministry of Education and Research.

Keywords: SAT algorithm, 2CNF, 3CNF, closed sum

DOI: 10.3233/SAT190060

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 6, no. 1-3, pp. 13-32, 2010

Received 1 December 2007
|
Revision received 1 September 2008
|
Published: 1 September 2008
Get PDF open access

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.

Show more