# Pucsat: a sat tool based on stalmarck and dpll approaches

Disponível somente no TrabalhosFeitos
• Páginas : 15 (3643 palavras )
• Publicado : 8 de maio de 2012

Amostra do texto
PUCSat: A SAT tool based on Stalmarck and DPLL approaches
Silva, F., Braz, F., Zarate, L., and S, M.
Computer Science Department Pontif´ Universidade Cat´lica de Minas Gerais ıcia o Belo Horizonte – MG – Brazil {flavio, fernando, zarate, sxxx}@pucminas.br

Abstract. This work applies an hybrid approach based on the Stalmarck and DPLL methodologies to solve SAT problems. Based on bothapproaches, it was implemented a tool to verify tautologies and propositional satisﬁability problems. The techniques and methodologies involved are described in the article. The Stalmarck rules were extended in order to lower computational costs which, in some cases, reduces the number of implications variables up to 60%.

1

Introduction

The satisﬁability problem, also known as SAT problem, ischaracterized by its formulation through propositional expressions. It has a theoretical importance once it was the ﬁrst problem proved to be NP-complete [1]. Many approaches have been proposed to solve SAT problems as, for example, those ones based on DPLL - currently the basis for most solutions [3]. Intensive researches have been developed once the satisﬁability problem has applicability indiﬀerent areas such as computer science, electronics, engineering, biology, mathematics and others. This article aims to describe some proposals founded in the literature to deal with the satisﬁability problem. Also, it describe an hybrid approach to solve SAT problems based on DPLL and Stalmarck methods. The Section 2 describes the SAT Problem. The Section 3 deﬁnes tautology and contradiction. TheSection 4 presents the DPLL and Stalmarck approaches. The Section 5 describes an hybrid approach to SAT problems, and Section 6 concludes the paper.

2

The SAT problem

The satisﬁability problem (SAT problem) can be stated as: given a boolean expression E, decide if there is some assignment to the variables in E such that E is true. The problem is basically described as a propositional formula(in CNF) which is made up of propositional variables, logical operators ∧, ∨, and the unary

2

operator ¬. One can consider the propositional variables those ones assuming only true or false values. A formula f is said to be in conjunctive normal form (CNF) if deﬁned over clause conjunctions ( c1 ∧ c2 ∧ c3 ∧...∧ cn ). In each clause at most the ¬ or ∨ connectives are presented. The operator ¬can not be repeated (as ¬ ¬) and it is only applied to propositional variables. Note that f is satisﬁed only if all clauses are taken as true. It is not satisﬁed if, at least, one clause is evaluated to false. It is said that a boolean expression is satisﬁed if there is at least one boolean assignment to the variables evaluating the CNF expression to true. The problem belongs to a speciﬁc class ofdecision problems, i.e., problems that admit only a yes or no answer. Basically, the task involving a SAT solver is ﬁnding an assignment of values to the boolean variables in order to satisfy all clauses. Finding such assignment solves the problem.

3