Article ID Journal Published Year Pages File Type
428716 Information Processing Letters 2009 4 Pages PDF
Abstract

For propositional formulas we present a new transformation into satisfiability equivalent 3-CNF formulas of linear length. The main idea is to represent formulas as parallel-serial graphs. This is a subclass of directed acyclic multigraphs where the edges are labeled with literals and the AND operation (respectively, the OR operation) is expressed as parallel (respectively, serial) connection.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics