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

**Páginas:**15 (3643 palavras)

**Publicado:**8 de maio de 2012

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

Tautology - Contradiction

Tautology can be deﬁned as a propositional expression which the result of its truth table contains only truthvalue. In other words, tautology is any propositional expression whose logical value is always true. On the contrary, contradiction can be deﬁned as any propositional expression which its truth table contains only false values - it is any propositional expression whose logical value is always false.

4

SAT Solvers Approaches

This section describes both DPLL and Stalmarck approaches to solveSAT problems. 4.1 The DPLL Methodology (Davis-Putnam-Logemann-Loveland)

The ﬁrst preliminary algorithm (denoted DP) solved SAT problems, but bounded to an exponential space resolution [2]. Improvements in the DP algorithm resulted in the DPLL approach which reduces exponential memory usage. A naive solution to SAT problems is searching value assignments to variables depicted as a binary...

Por favor, assinar para o acesso.