Algoritmo Purl De Lógica

A Polynomial Algorithm for Some Special
Satisfiability Problems
J.R.Portillo1
1

2

and J.I.Rodrigues2

Universidad de Sevilla.
josera@us.es
Universidade do Algarve.
jirodrig@ualg.pt

Abstract. We introduce a new polynomial class of Satisfiability (purl).
To determine whether a formula is satisfiable, we introduce the algorithm RemoveLiterals which runs in polynomial time for everyinstance of purl. This algorithm exploits the removable literal concept.
Under which, a propositional formula and the resultant removing a removable literal from a clause are equivalent.
This new class was found when we were studying an orthogonal graph
drawing open problem. Reducing this geometric problem to sat the resultant propositional formulae are in 3-sat, which is in general annpcomplete problem. We also show that this problem is solvable in polynomial time proving that propositional formulae are in purl.
Besides it has been developed to solve a specific problem, this is a general
method. It can be applied successfully to solve many distinct problems.
Testing it, we have solved the map labeling us-s(m)-4p open problem,
which is also presented in this work.
There are someopen problems arising with this new polynomial sat
class. One of the most significant is characterizing general structural
properties of formulae.

1

Introduction

sat problem is a core problem in mathematical logic and computing theory with
practical applications in many fields.
The Satisfiability problem (sat) is to determine whether exists a satisfying
true assignment for a givenpropositional formula, usually in Conjunctive Normal Form (cnf). Since Cook proof of np–completeness for sat [1], many studies
of complexity to testing satisfiability for particular classes of propositional formulae have been done. A good survey of algorithms for sat can be found in [2].
Moreover, it is known the existence of some classes of sat which can be solved
in polynomial time, such as 2-sat,Horn, q-Horn, extended-Horn and slur [3].
In this work we introduce a new class of propositional formulae solvable in
polynomial time. It has been found when studying a geometric open problem,
Partially supported by pai project fqm-0164 and bfm 2001-2474.
Partially supported by fse, prodep 5.3/alg/194.019/01.

which is presented in Section 3. The key of that result is the removableliteral
concept and the well known lineal algorithm for unit clause resolution.
Let B = {0, 1} be the set of values of a boolean variable and S a cnf formula
on n variables x1 , . . . xn . An element a ∈ B n is an assignment of values to all
variables (true assignment). A formula S is satisfiable by a if S (a) = 1. Otherwise
the formula is falsified. Given a propositional formula, the 1-neighborhoodof a
clause, N b(C ), is the set of all assignments satisfying only one literal of this
clause. Furthermore, if this formula is satisfiable then there is a solution a ∈ B n ,
which lies in the 1-neighborhood of a clause [4]. Conversely, if S is not satisfiable,
for any assignment a ∈ B n , S (a) = 0.
Given a clause C ∈ S , a literal, u ∈ C , is called removable if any assignment
in the1-neighborhood of C satisfying u, a ∈ N b(u, C ), falsifies the propositional formula. A clause with a removable literal can be simplified removing
that literal from it. For a general cnf formula, detecting a removable literal is
an np-complete problem.
Propagation of unit clauses is a well known lineal algorithm used to solve
2-sat instances, usually denoted by PropUnit. At each step, it resolves aunit
clause with the rest of the formula. This algorithm halts when there are no more
clauses or unit clauses left, or when an empty clause is achieved. For commodity
an adapted version from Dalal and Etheringthon [5] is presented. The notation
used in this work is also adopted, where {} represents an empty formula, which
is satisfiable and { }, a formula with an empty clause, which is not...