| The problem of propositional SATisfiability for formulae in conjunctive normal form is the first known NP-complete problem. Many practical NP-hard problems may be transformed efficiently to SAT. The most widely used SAT solver is the well-known DPLL method. It is based on Unit Propagation, UP for short. DPLL spends 80-90% of its runtime in UP, so if we want to speed-up DPLL then we have to either speed-up UP or reduce the number of used UP steps. This talk is concerned on the second approach. We introduce the n-literal clause set representation. A clause set is the conjunction of disjunctions of literals. A literal is a propositional variable or its negation. This literal notion corresponds to the 1-literal notion in this paper. An n-literal consist of 2^n bits, each bit corresponds to a combination of n (normal) literals. In particular the 2-literal representation is the following which uses 4 bits to represent all the 15 possible basic (basic means cannot be simplified) formulae with 2 variables ([--]:0001, [-+]:0010, [-x]:0011, [++]:0100, [--,++]:0101, [x+]:0110, [-x,x+]:0111, [+-]:1000, [x-]:1001, [-+,+-]:1010, [-x,x-]:1011, [+x]:1100, [+x,x-]:1101, [+x,x+]:1110, [xx]:1111). The idea is that every bit corresponds to a 2-clause (a clause with two concrete literals). For example, the least significant bit corresponds to --. If a bit is 1 then the corresponding 2-clause is subsumed by the represented formula. In this way we get better running result of DPLL using 2-literal representation in case of graph coloring problems and the pigeon-hole problem. |
Last modified: Tuesday, 9 January 2007, 11:49 AM