کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
429301 687181 2008 17 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
SAT graph-based representation: A new perspective
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
SAT graph-based representation: A new perspective
چکیده انگلیسی

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.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Algorithms - Volume 63, Issues 1–3, January–July 2008, Pages 17-33