Graph Based Representations SAT Solving for Non-clausal Formulas

Boolean satisfiability (SAT) solvers are used heavily in hardware and software verification tools for checking satisfiability of Boolean formulas. Most state-of-the-art SAT solvers are based on the DPLL algorithm and require the input formula to be in conjunctive normal form (CNF). We represent the vhpform of a given NNF formula in the form of two graphs called vpgraph and hpgraph. The input formula is translated into a 2-dimensional format called vertical-horizontal path form (vhpform). In this form disjuncts (operands of V) are arranged orizontally and conjuncts (operands of A) are arranged vertically. The formula is satisfiable if and only if there exists a vertical path through this arrangement that does not contain two opposite literals ( I and The input formula is not required to be in CNF.