Name
Abstract | ||
|---|---|---|
In this paper a new graph based representation of Boolean formulas in conjunctive normal form (CNF) is proposed. It extends the well-known graph representation of binary CNF formulas (2-SAT) to the general case. Every clause is represented as a set of (conditional) implications and encoded with different edges labeled with a set of literals, called context. This representation admits many interesting features. For example, a path from the node labeled with a literal @?x to the node labeled with a literal x gives us an original way to compute the condition under which the literal x is implied. Using this representation, we show that classical resolution can be reformulated as a transitive closure on the generated graph. Interestingly enough, using the SAT graph-based representation three original applications are then derived. The first one deals with the 2-SAT strong backdoor set computation problem, whereas in the second one the underlying representation is used to derive hard SAT instances with respect to the state-of-the-art satisfiability solvers. Finally, a new preprocessing technique of CNF formulas which extends the well-known hyper-resolution rule is proposed. Experimental results show interesting improvements on many classes of SAT instances taken from the last SAT competitions. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1016/j.jalgor.2008.02.001 | J. Algorithms |
Keywords | Field | DocType |
last sat competition,binary cnf formula,2-sat strong backdoor,new graph,sat graph-based representation,new perspective,hard sat instance,cnf formula,sat instance,well-known graph representation,underlying representation,graph representation,satisfiability,conjunctive normal form,transitive closure,preprocessing | Discrete mathematics,Combinatorics,Satisfiability,Boolean satisfiability problem,Conjunctive normal form,Transitive closure,Underlying representation,Graph (abstract data type),Mathematics,Binary number,Computation | Journal |
Volume | Issue | ISSN |
63 | 1-3 | 0196-6774 |
Citations | PageRank | References |
1 | 0.38 | 25 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gilles Audemard | 1 | 640 | 37.66 |
| Saïd Jabbour | 2 | 175 | 12.44 |
| Lakhdar Sais | 3 | 859 | 65.57 |