Pucsat: a sat tool based on stalmarck and dpll approaches

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 both approaches, 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%.

1

Introduction

The satisfiability problem, also known as SAT problem, is characterized 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 in different 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. The Section 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 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