Satisfiability in Boolean Logic (SAT problem) is polynomial

Abstract

Abstract. We find a polynomial algorithm to solve SAT problem in Boolean Logic. Аннотация. Находится полиномиальный алгоритм решающий проблему SAT в Булевой логикуе.

Headnote

Abstract. We find a polynomial algorithm to solve SAT problem in Boolean Logic.

Keywords: Boolean Logic, Satisfiability Problem, SAT algorithm.

Аннотация. Находится полиномиальный алгоритм решающий проблему SAT в Булевой логикуе.

Ключевые слова: булева логика, проблема выполнимости, алгоритм SAT.

(ProQuest: ... denotes formulae omitted.)

Introduction

The satisfiability problem (SAT) in Boolean propositional logic is the question to determine if any given formula F is satisfiable (i.e. if there is a substitution of literals TUE-FALSE instead the propositional letters from given formula F making the formula TRUE). Extended SAT problem is to find a such substitution if the one exists. SAT is an NP-complete problem, and is one of the most intensively studied problems.

As well known SAT was the first known NP-complete problem, that was proved by S.Cook at the University of Toronto in 1971 (cf. [1]) and also independently by L.Levin in 1973 (cf. [2]). Remarkably that before these results, the idea, the concept, of an NP-complete problem did not even exist, so was totally out of consideration. .

That generated a very active area in complexity theory; since the SAT problem is NP-complete, and only algorithms with exponential worst-case complexity are until now known for it, better algorithms for SAT where in grate demand. In particular researchers looked for efficient and scalable algorithms for SAT for formulas in restricted form; and during the 2000s algorithms making dramatic advances in our ability to automatically solve problem was developed (cf. [3,4,10-12]). In this paper we will prove that SAT may be solved in polynomial time.

1. Proof, Deterministic Algorithm with Random Any Choice

We first need to restrict the amount of necessary formulas in our considerations. We will do this restriction by Theorem 1 placed below. Actually this result was known for long ago, for example the author introduced reduced normal forms for inference rules in [5, 6] where he solved Friedman problem about recognition inference rules for intuitionistic propositional logic. This technique was efficiently applied in [5-9] for study inference rules and unification. The point here is that the premises of such rules are exactly the normal reduced forms for just formulas. These approach also possibly was observed even earlier when researchers used reduction formulas for Received 10.07.2021, received in revised form 10.08.2021, accepted 21.08.2021

3-Sat problem and relative subsequent research (cf. [3,4,10-12]). I am not sure about history and priority not being very expert in the SAT area. Though it turned out that Theorem 1 is also very useful for positive solution SAT problem and we present it now.

Definition. We say that Boolean formula F has reduced normal form if

...

where

...

and Bj. € {p, -p}, p € Prop and Prop is a set of letters.

In the sequel we may consider also Aj containing less then 3 disjunct members. Simply for convenience and simplicity in notation we will always refer to 3 disjunct members, thinking that it might be less.

Theorem 1. There is a polynomial algorithm constructing by any given boolean formula G a formula F in reduced normal form which has the following properties. (1) F has all variables of G and some more in amount not bigger then the length of G. (2) F is equivalent to G w.r.t satisfiability. (3) Any substitution a for F satisfying G acting at only variables of G satisfies G, (and vice versa any substitution satisfying G may be computably extended on additional variables of F satisfying it).

Proof. It is a simple statement; as much as I remember I myself proved it first time in my works for constructing reduced normal forms for inference rules in my research to resolve Friedman problem about recognizing admissible rules in intuitionistic logic cf. [6], 1984. A short draft of the proof is as follows. In fact, we simply shall specify the general algorithm described already several times in [5-9] to the language of our logic.

So, let we start. If ф = a о ß, where o is a binary logical operation and both formulas a and ß are not simply variables or unary logical operations applied to variables (which both we call final formulas), take two new variables xa and xß and the formula

...

If one from formulas a or ß is final and another one not, we apply this transformation to the non-final formula. It is clear that f and f1 are equivalent w.r.t. satisfiability.

If ф = -a and a is not a variable, take a new variable xa and the formula

...

Again f and f1 are equivalent w.r.t. satisfiability. We continue this transformation over the resulting formulas

...

until all formulas a3 and Yj in the formula above will be either atomic formulas, i.e. logical operations applied to variables, or variables.

Evidently this transformation is polynomial. Further, we transform the formulas using = in the ones using only disjunctions and conjunctions and negations. After that we obtain formula in form as required for reduced normal forms. The only point is that the conjuncts may continue less that 3 disjunct formulas, we then may double some until 3 members. As the result we get the final formula f2 which evidently has all required properties. Q.E.D.

Now we turn to SAT problem. In the sequel a literal is either a propositional letter or a letter with applied negation (-p for p). Below we will always refer to only 3 disjuncts in F = Ai A A2 A - · · A Ak,, where Aj := Bj1 V Bj2 V Bj3. But we could admit less disjuncts, simply we keep all 3 for simplicity of notation.

Theorem 2. If a formula F has reduced normal form then there is a polynomial algorithm verifying its satisfiability and constructing its some unifier if F is satisfiable.

Proof. Let

...

where

...

and Bj £ {p, -p},p £ Prop where Prop are propositional letters. Assume F has exactly m letters.

It is evident that F is satisfiable iff there is at least one path from Ai to Ak passing through each Aj via some unique Bj2 (in this Aj) not containing contradictory literals along all path.

We will try to construct such a path now. We do it by induction on j in Aj so we do it by induction on к in Ai A A2 A · · · A Ak. Let k = 1 then we have the path.

Inductive step. Assume that n steps are already done and (1) all sets Imp(Bni) are constructed and any Imp(Bni) contains absolutely all possible literals g (in given m letters) to which we cannot make step from Bni that is g is any literal contradicting to some lateral in any possible not contradictory paths leading from any disjunct from Ai to Bni. (2) The sets To(Bni) contain all Bn-ij which themselves are reached by non-contradictory (no matter which) paths from Ai and from which we (non-contradictory) moved in Bni. Note that we do not store (record or memorize) paths themselves - we just fix (record) their existence by marking all Bn-ij from which we made final steps to (Bni). (That is why we summarize things (steps, actions) while the procedure but do not multiply them.)

Of course we assume all sets To(Bii) to be {Bi2} and for n =1 all is ready, and for all i, Imp(Bii) = {-Bii} if Bİ2 is a letter and Imp(Bii) = {Bi2} otherwise.

Now we turn to the inductive step itself, we try to move to (n + 1)-th conjunct from An, to make (n + 1)-th step. Assume that n steps are done and we arrived to Bni (which informally means by not-contradictory path; which in our formalism only means that To(Bni) = 0, or n = 1) and all Imp(Bnj) and To(Bnj) are constructed. Consider any Bn+ij. Define immediately

...

and

...

are unions of all Bni which do not contradict Bn+ij and where To(Bnj) are not empty (which, by the way, means that Bn i are reached by some non-contradictory paths, and, recall the inductive assumption, - sets Imp(Bnı) are already successfully constructed).

It is clear that Imp(Bn+ij) is the set containing all literals to which we cannot step form Bn+ij further at all, even, in particular, to literals which occurs An+2. Consider all Bn+2l from level n + 2; if any of them occurs in Imp(Bn+ij) we cross out such Bn+ij from further consideration. And if that indeed holds for all Bn+il the procedure stops and formula F is not satisfiable.

If we can continue, recall that earlier we put in To(Bn+ij) all Bni from which we arrived to Bn+ij. The step (n+1) is completed.

If we came to some Bkj the formula F is satisfiable otherwise not. And the sets To(Bn+ij) give us a satisfying substitution, if we will move from Bkj back to Ai via sets To(Bkj) subsequently using To(Bnj) towards Ai. The trick here is that we do not do any choice at all; during moving we just take any Bkj from To(Bn+1.) (and we have at most 3 options for that each choice) and move towards A1.

The interesting thing here is that we do not do choice at all - we can take subsequently any from any occurring in Bnj moving to the origin Ai. That looks as not deterministic algorithm but in fact it is the one, a good one, since we can take any disjunct from at most 3 possible options and any of them will lead us to success.

The amount of steps in this algorithm is polynomial: the general amount of steps used in our inductive procedure in constructing Imp(Bnj) and To(Bn+1.) is at most k. And in the inductive step itself from n to n + 1 for constructing Imp(Bn+1j) and To(Bn+1.), the amount of steps is at most 3 x [3 x (2m)2] (m is the number of letters in formula) for computing intersections Imp(Bn1) П Imp(Bn2) П Imp(Bn3)]. Q.E.D.

This research is supported by High Schools of Economics (HSE) Moscow; supported by the Krasnoyarsk Mathematical Center and financed by the Ministry of Science and Higher Education of the Russian Federation (Grant No. 075-02-2020-1534/1).

References

References

[1] S.Cook, The complexity of theorem proving procedures, Proceedings of the Third Annual CAM Symposium on Theory of Computing, 1971, 151-158.

[2] L.A.Levin, Universal sequential search problems, Problemy Peredachi Informatsii, 9(1973), no. 3, 115-116 (in Russian); Translated into English by B.A.Trakhtenbrot, A survey of Russian approaches to perebor (brute-force searches) algorithms, Annals of the History of Computin, 6(1984), no. 4, 384-400.

[3] B.Selman, D.Mitchell, H.Levesque, Generating Hard Satisfiability Problems, Artificial Intelligence, 81(1996), no. 1, 1729.

[4] T.J.Schaefer, (1978) The complexity of satisfiability problems, Proceedings of the 10th Annual CAM Symposium on Theory of Computing, San Diego, California, 216226.

[5] V.Rybakov, Admissible Rules in Pretabular Modal Logic, Algebra and Logic, 20(1981), 291-307.

[6] V.Rybakov, Criterion for Admissibility for Rules in the Modal System S4 and Intuitionistic Logic, Algebra and Logic, 23(1984), no. 5, 291-307.

[7] V.V.Rybakov, Logical equations and admissible rules of inference with parameters in modal provability logics, Studia Logica, 49(1990), no. 2, 215-239

[8] V.V.Rybakov, Problems of substitution and admissibility in the modal system Grz and in intuitionistic propositional calculus Annals of Pure and Applied Logic, 50(1990), no. 1, 71-106.

[9] V.V.Rybakov, Admissibility of Logical Inference Rules, Vol. 136, 1st Edition, Elsevier, 1997.

[10] F.Massacci, L.Marraro, Logical Cryptanalysis as a SAT Problem, Journal of Automated Reasoning, 24(2000), no. 1, 165203.

[11] Marijn J.H.Heule, Hans van Maaren, Look-Ahead Based SAT Solvers, Handbook of Satisfiability, IOS Press, 2009, 155184.

[12] C.Moore, S.Mertens, The Nature of Computation, Oxford University Press, 2011.