Pucsat: a sat tool based on stalmarck and dpll approaches

Disponível somente no TrabalhosFeitos
  • Páginas : 15 (3643 palavras )
  • Download(s) : 0
  • Publicado : 8 de maio de 2012
Ler documento completo
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 satisfiability 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%.



The satisfiability problem, also known as SAT problem, ischaracterized by its formulation through propositional expressions. It has a theoretical importance once it was the first 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 satisfiability problem has applicability indifferent 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 satisfiability 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 defines 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.


The SAT problem

The satisfiability 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


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 defined 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 satisfied only if all clauses are taken as true. It is not satisfied if, at least, one clause is evaluated to false. It is said that a boolean expression is satisfied if there is at least one boolean assignment to the variables evaluating the CNF expression to true. The problem belongs to a specific class ofdecision problems, i.e., problems that admit only a yes or no answer. Basically, the task involving a SAT solver is finding an assignment of values to the boolean variables in order to satisfy all clauses. Finding such assignment solves the problem.


Tautology - Contradiction

Tautology can be defined 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 defined as any propositional expression which its truth table contains only false values - it is any propositional expression whose logical value is always false.


SAT Solvers Approaches

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

The first 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...
tracking img