Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
428716 | Information Processing Letters | 2009 | 4 Pages |
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