P EQ NP

A Site Devoted to Demonstrating the Proof that P Equals NP to the Computer Science Community

The following is a hyperlink to a pDrive storage account that contains all of the files that pertain to this software project so that people from the general public can view it:

NPCOMP Files Repository


An Improvement on the Solution of Circuit Satisfiability Applicable to Solving the Question of Whether P=NP


Leonard Gojer, B.S. Computer Science, University of Texas, Dallas, Prateek Swamy, B.S. Computer Science


Abstract – The prior consensus among computer scientists for the past 50 years or more has been that the

NP-Complete problems have no polynomial order time solutions. An important part of that existing body

of Computer Science theory is that the “Circuit Satisfiability” problem has no polynomial order time

solution. The author here presents a new algorithm for the Circuit Satisfiability problem which can be

proven to run in polynomial order time, thereby reversing the consensus of the premise that P<>NP and

replacing it with the premise that P=NP.


Keywords: computational complexity, polynomial order time, exponential time, NP-Complete problems


I. INTRODUCTION


The curriculum of modern computer science classifies mathematical algorithms according to their

computational complexity, among other characteristics suc as the department of Calculus or Discrete

Math that they would reside in, in order to facilitate the activities of researchers who might come across

the algorithms when searching through the science literature. The NP-Complete problems is a class of

mathematical optimization problems which have been categorized by computer scientists of the past

according to the scientific conclusion that they cannot be solved in polynomial order time. This was

originally concluded by Claude Shannon in the 1950’s when he analyzed the BDD algorithm. (X) This

label of NP-complete is to warn future computer scientists who might encounter the material that they

will not achieve efficiency in implementing the algorithms that are labeled as NP-Complete. And is to

encourage those scientists to not consider the NP-Complete solutions to algorithms unless as a worst case

solution to the problems at hand, but to instead consider algorithms that are not NP-Complete first in the

creative design process of designing a new program. Algorithms in computer science are established by

the systematic research of computer scientists who dedicate time to experimenting with the mathematical

possibilities that could be constructed in the computer and then recording their findings and theorizing

about th complexity of what they have found. The algorithm presented here is an example of the product of

such research, which was performed by myself during the years 2000-2005. Consider that in the development of

modern mathematics, formulas are recorded in the textbooks when they have been deemed to be worthy

of being recorded due to the time savings that they represent when they are used by mathematicians.

Many famous theorems in mathematics, such as in the Calculus were originally discovered in the prior

centuries and they have been passed down to the students of the present time because they have been

found to be continuously useful in modern circumstances, rather than discarding them. This algorithm is

worth keeping and using for the same reason, it represents a big savings in time and money for the

programmers and computer owners who use it.


There are six categories of problems in the computer science literature that are classified as

NPComplete. They are respectively:


• The Circuit Satisfiability Problem

• The Traveling Salesman Problem

• The Subgraph Isomorphism Problem

• The Graph Coloring Problem

• The Subset Sum Problem

• The Vertex Cover Problem (2)


In “Guide to the Theory of NP-Completeness”, which was originally written in 1971, Gary and Johnson

illustrate the fact that all of these problems are considered transformations of each other in the

theory of computation. The Circuit Satisfiability problem, along with the other variations of NP-Complete

problems, is a problem that in its prima fascia form consists of what is called an “optimization” problem,

which is a type of problem that concerns itself with finding the optimal arrangement of the data to either

maximize a given function of the data items in the problem or minimize it, (depending on what the

circumstances from the real world are). An example of a maximization problem would be to maximize

profits from some economic function. An example of a minimization problem might be to minimize the

material or costs of some project. The significance of finding a polynomial order time solution to the

Circuit Satisfiability problem is that it allows computer software to be created that uses it to solve some

important engineering problems, such as, for example, the design of electrical logic circuits in IC chips

within a time constraint that saves an increasing amount of time and labor as the size of the problem

increases. In this particular example, it allows computer scientists to create very large chips which

dramatically outperform the existing IC chips which represents a very large economic payback for the

electrical engineers when the design is very large. Many people in the past have tried to create polynomial

order time solutions of the Circuit Satisfiability problem and have concluded that the problem has no polynomial

order time solution. They have published their mathematical work in the literature since the 1950’s

to the present. It becomes important in this paper to explain what was done differently in this solution to

facilitate that it works to make the explanation clear.


Today, existing algorithms for solving the Circuit Satisfiability problem are Genetic Algorithms which

apply the concept of Genetic programming in AI. This is because a Brute Force method of solution to the

optimization problem performed without any inspired mathematical knowledge takes an exponential

order running time to perform, (1) this was stated by Claude Shannon in the 1950’s along with Donald

Knuth, who wrote “The Art of Computer Programming”. Genetic algorithms work by the mechanism of

probability theory as it concerns the patterns in the data. An example of a genetic algorithm for solving a

problem might be the following, to create a stock market indicator which would be optimized to the

successful for a long period of time in the historical past. The genetic algorithm would start with an original

hypothesis that was generated randomly and then proceed to revise it over and over again until it passed the

test of some statistical criteria of how close it comes to perfection. Each time that it revised it, it would

utilize the Genetic algorithm paradigm which is a sophisticated method of making good guesses for generating the

next attempt at the solution. The process would halt when the criteria of satisfaction was satisfied.


Existing algorithms for solving the Circuit Satisfiability problem using the Genetic Algorithm approach

thus start with a randomly generated solution which may or not be the final solution, (usually it probably

isn’t) and then refine the solution iteratively using the idea of “good guesses” that are based on the

Genetic Algorithm methodology, which uses the idea of elaborate hypothesis composition formulas.

That means that existing solutions to the SAT problem based on using Genetic algorithms have the

characteristic that most of the time, they probably finish in polynomial order time, but in a few bad

instances, they take exponential time to run. This happens when they reach an inefficient pathway by

mistake, or rather by random chance.


II. RELATED WORK


Most existing work that is prevalent in the computer science literature today either tries to find a better

genetic algorithmic technique for the SAT algorithm or else tries to prove that the P=NP problem cannot

be solved with a polynomial order time solution . A few of these prominent computer scientists agree that

P = NP. A survey of the existing work that was compiled in a web article shows that 50% of the computer

scientists of a group of about 20 computer scientists concluded that P<>NP and the other 50% concluded

that P=NP, providing some very creative arguments on both sides of the issue.


Another example of what is done in the public arena is to have public contests that are run to encourage

people to find better genetic algorithms for the SAT algorithm. For example, there is a contest that is held

regularly on the internet where programmers are invited to try to make faster algorithms for the SAT

algorithm; it is called “SAT Live!” and the contest is held every year with prizes being given away. (4)

Some computer scientists have also taken the P=NP side of the issue and have concluded in a manner

similar to the authors of this paper that P=NP because Integer Linear Programming, (which is one of the

NP-Complete Problems, and which has been shown to be another form of the SAT algorithm), can be

solved in polynomial order time. (3) The TSP can be solved with Integer Linear Programming.


III. OUR RECURSIVE ALGORITHM FOR SAT


The algorithm of this paper is based on a novel use of the idea of recursion with respect to the processing

of binary trees. The idea is to first parse the Boolean expression in question into the form of an Abstract

Syntax Tree, (similar to what happens in the internal mechanism of a compiler, such as the C# compiler

or C++ compiler), and then to process the nodes and leaves of the binary tree according to a process that

is recursive. The recursive property has the characteristic that subtrees can be checked for the question of

whether or not they are SAT, (satisfiable), using the exact same algorithm, and that the question of

whether the total tree is SAT, (satisfiable), is solved by the prior determination of the question of SAT for

the subtrees.


The fundamental proposition of this new algorithm is: P is SAT if either:

- P consists of a a Not (Q) and Q is not SAT

- P consists of an (Q or R), and Q is SAT or R is SAT

- P consists of an (Q and R) and (Q is SAT) and (R is SAT) and the solution of (Q is SAT) is not the

inverse of the solution of (R is SAT). This statement is relatively easy to state in an OOP programming

language such as C++ or C#. What is needed is a function that is called:


Bool isSAT(SATProposition P)

{

Bool tmp = false;

If (isaNot(P)) { tmp = !(restof(P)); }

If (isanOr(P)) { tmp = isSAT(leftPtr(P)) or isSAT(rightPtr(P)); }

If (isanAnd(P)) { tmp = isSAT(leftPtr(P)) and isSAT(rightPtr(P)) and

notInverses(leftPtr(P),rightPtr(P)); }

Return tmp;

}


It becomes relatively trivial to carry out the implementation of the above described algorithm, once it has

been properly stated that way in a programming language, such as C#. (Actually would be better for this coding

project because C# does not allow pointers in the same way that C++ does). It can then be shown that when the SAT

expression is of height 1, that the running time of the algorithm is a k (constant), running time, because

there is no step of recursion.


Next, it can be shown that the running time of the algorithm for cases that are of height greater than 1 is

some composite function of O(n log n), because that is the running time of a process that enumerates the

leaves of the binary tree with recursion. The only thing that remains in the computation of the Big O (running

itme), of the algorithm is to know what the running time of the internal process of the algorithm inside

of that is. The easy cases are close to a constant order. The hard cases are close to the running time of

O(n^2). The reason for that is because the hard cases depend on an internal algorithm called the “Equivalence

Algorithm” which is a subroutine of the notInverse(P1,P2) Algorithm that is used in the solution of

SAT.


The purpose of the “Equivalence Algorithm” is to check if two propositions are the exact same

proposition and return true if they are. This is an important issue in theory of the NP complete problems

because in the prior literature, Equivalence was considered the same isse as the BDD algorithm which

proports that P <> NP, so solving Equivalence in P time is a secondary proof of the thesis of this paper.


That result is used by the notInverse Algorithm in the following manner:


Bool notInverse(SATProposition P1, SATProposition P2)

{

Bool tmp = true;

If (Equivalent(P1,!P2) or Equivalent(!P1,P2))

{

tmp = false;

}

Return tmp;

}


First Attempt at Solution Involved Using Graph Isomorphism


In the first attempted solution of the SAT algorithm, the process of checking to see whether two sub-

Propositions are equivalent involves a complicated algorithm which is based on calling Graph

Isomorphism as a subroutine. First, the two trees of the expressions are rewritten in the form of

graph adjacency matrices. Then, the two adjacency matrices are compared with a graph isomorphism algorithm.

It has been proven in the historical past that graph isomorphism can run in polynomial order time. There

are now many algorithms to choose from. One such algorithm devised and proven in the year 2009 by Ashay

Dharwadker and John-Tagore Tevet is discussed here. There are other algorithms for graph isomorphism in

the computer science literature that run in polynomial order time. I myself devised on in the year 2001

which I think is similar but not identical to the one by Dharwadker and Tevet, but I am going to talk

about theirs, since theirs is more formally proven in the mathematical literature of computer science.

The algorithm works by manipulating the rows of the adjacency matrix until the canonical form is

reached. It is a relatively complex algorithm which for the purpose of this paper will be treated simply as

a black box that works to solve it. Their algorithm is proven to run in O(3*N^2 + 3*N). (5).

So, the composite running time of the total algorithm of this paper is: O(N log(N))*O(3*N^2 + 3*N)

which comes out be O(3*N^3*log(N) + 3*N^2*log(N)) which is less than O(N^4) and is therefore in P.


Second Attempt at Solution Performed Without Using Graph Isomorphism In the second attempt at solving the

SAT algorithm, it is since discovered that it is not actually needed to invoke the concept of Graph Isomorphism.

The reason for this is because in the process of checking whether two propositions are identical, (the

"Equivalence Algorithm"), it is discovered that there is no need for a total test of equivalence of the two

expressions. The only thing that is needed is to check and see if the two expressions are or are not identically

spelled. The other mathematical case of "equivalence" - which would be for the case where two expressions are

identical but not spelled out the same way - is simply not needed to successfully compute the answer to SAT

and the result of P = NP. I will give the following explanation for this: The scenario breaks

down into eight different mathematical cases. The first case is for the scenario that the two expressions are

SAT but not equivalent to each other, (yielding SAT = T). The second seven cases are for the scenarios where

the two expressions have any other of the possible combinations of SAT and Equivalence not found in

the first case.


Basic Claim of the Improved Algorithm:


Case 1: F = P and Q and (P !EQ !Q), and (P = SAT) and (Q = SAT). Result: SAT = T

Case 2: F = P and Q and (P EQ Q), and (P = SAT) and (Q = SAT). Result: SAT = F

Case 3: F = P and Q and (P EQ Q), and (P = SAT) and (Q != SAT). Result: SAT = F

Case 4: F = P and Q and (P EQ Q), and (P = !SAT) and (Q = SAT). Result: SAT = F

Case 5: F = P and Q and (P EQ Q), and (P = !SAT) and (Q = !SAT). Result: SAT = F

Case 6: F = P and Q and (P !EQ Q), and (P = SAT) and (Q = !SAT). Result: SAT = F

Case 7: F = P and Q and (P !EQ Q), and (P != SAT) and (Q = SAT). Result: SAT = F

Case 8: F = P and Q and (P !EQ Q), and (P != SAT) and (Q != SAT). Result: SAT = F


Expanded Proof of the Basic Claim Given Above:


Case 1: F = P and Q and (P !EQ !Q), and (P = SAT) and (Q = SAT). Result: SAT = T

if (P !EQ !Q) can be solved in P time, then the claim is upheld.


Case 2: F = P and Q and (P EQ !Q), and (P = SAT) and (Q = SAT). Result: SAT = F

if (P EQ !Q) can be solved in P time, then the claim is upheld.


Case 3: F = P and Q and (P EQ !Q), and (P = SAT) and (Q != SAT). Result: SAT = F

if (Q != SAT) can be solved in P time, then the claim is upheld.


Case 4: F = P and Q and (P EQ !Q), and (P = !SAT) and (Q = SAT). Result: SAT = F

if (P != SAT) can be solved in P time, then the claim is upheld.


Case 5: F = P and Q and (P EQ !Q), and (P = !SAT) and (Q = !SAT). Result: SAT = F

if (P != SAT) or (Q != SAT) can be solved in P time, then the claim is upheld.


Case 6: F = P and Q and (P !EQ !Q), and (P = SAT) and (Q = !SAT). Result: SAT = F

if (Q != SAT) can be solved in P time, then the claim is upheld.


Case 7: F = P and Q and (P !EQ !Q), and (P != SAT) and (Q = SAT). Result: SAT = F

if (P != SAT) can be solved in P time, then the claim is upheld.


Case 8: F = P and Q and (P !EQ !Q), and (P != SAT) and (Q != SAT). Result: SAT = F

if (P != SAT) or (Q != SAT) can be solved in P time, then the claim is upheld.


That conclusion has to be sustained if and only that the problem of

whether (P !EQ !Q) can be solved in P time. The proof of that is as follows:


Lemma 1: If P is literally the same as Q, then SAT can be solved in P time, because the

time to check for literal equivalence is in P. (O(n)).


Lemma 2: If P is not literally the same as Q, but it is canonically equivalent to Q,

then SAT can still be solved in P time, because of the following delineation of the

mathematical cases involved:


Case 1: The result is intended to be (SAT = T).


A. P will check as SAT

B. Q will check as SAT

C. (P !EQ !Q) will not check, and the result will confirm as SAT


Case 2: The result is intended to be (SAT = F).


A. P may or may not check as SAT and the result will confirm that the SAT algorithm is

correct.


B. Q may or may not check as SAT and the result will confirm that the SAT algorithm is

correct.


C. (P !EQ !Q) will divide into four cases:


(P = Q) (literally), The result will check.

(P = Q) (not literally, but canonically). The result will check.

(P != Q) (literally). The result will also check.

(P != Q) (not literally, but canonically). The result will check.

The resulting algorithm will tend to run in a running time of approximately O(n log n).


Here is still another algorithm that can be used to demonstrate that the equivalence algorithm

can run in P time. It proceeds by the method that an two expressions being tested for equivalence

can either be of the following nine cases:


1. A is an Not and B is an Not.

2. A is an Not and B is an And.

3. A is an Not and B is an Or.

4. A is an And and B is an Not.

5. A is an And and B is an And.

6. A is an And and B is an Or.

7. A is an Or and B is an Not.

8. A is an Or and B is an And.

9. A is an Or and B is an Or.


The proof then depends on expounding on those cases. The running time is no worse than the worst case,

which is when both A and B are Ands.


The following algorithm explains what to do for that scenario:


1. Let A = C and D, and let B = E and F.

2. Then compare C with E for equivalence recursively. If they are not equivalent, terminate with

Equivalence = False.

3. If they are equivalent, then compare D with F. If they are not equivalent then terminate with

Equivalence = False. If they are equivalent, then terminate with Equivalence = True.

4. Then compare C with F for equivalence recursively. If they are not equivalent, terminate with

Equivalence = False.

5. If they are equivalent, then compare D with E. If they are not equivalent then terminate with

Equivalence = False. If they are equivalent, then terminate with Equiivalence = True.


The proof that that algorithm runs in polynomial time is as follows:


1. The comparison of the two sides, A and B depends on the matching up of the items in the bottom

leaves of the trees that make the expressions. The problem of comparing the two sides of the

trees depends on twisting the various possible matchings of the trees until one successful

matching is found. If two trees are both consisting of And expressions, then the following

table of the Big O computation can be constructed:


1. For two trees of height 1, the running time is O(2). = O(k).

2. For two trees of height 2, the running time is O(4) = O(2k),

because there can be four configurations of the matchings.

3. For two trees of height 3, the running time is O(16) = O(8k),

because the there can be sixteen configurations of the matchings.

4.

5.

6.

7.


Now, at this point, I need to discuss with you the readers what is the formal mathematical proof of the

above algorithm which has been stated here.


There are two propositions to the proof of the algorithm which work together to prove this thesis.


The first proposition is that:

#1 – The above mentioned algorithm solves the problem of SAT, irrespective of whether or not it

terminates in Polynomial Order Time.


The second proposition is that:


#2. - The above mentioned algorithm does in fact terminate in Polynomial Order Time, irrespective of

whether or not it correctly solves the SAT problem.


When those two propositions are formally proven and that placed together, the conclusion is that P=NP.


The proof of the first proposition is as follows:


#1 – The cases for Not’s and Or’s are tautologies. This is because they don’t make any sophisticated

arguments of recursion.


#2 – The case for And’s are more complex and consists of a group of tautologies that work together to

create the larger proposition of the proof on And’s. This proving work requires an extensive enumeration

of a large number of sub-propositions.


• A and Not A is Not Satisfiable.

• If A = Set of Literals and Not A = Set of (total set – A), then again A and Not A is Not Satisfiable.

• If A = B then A and B is Satisfiable.

• If A <> B then (A and B) is sometimes Satisfiable and sometimes Not Satisfiable.

• If A and B has one variable not in common then A <> B.

• If A and B has one variable not in common then either A <> Not B or Not A <> B.

• Case 2 of D is equal to Case B.


The proof for the second proposition that the algorithm runs in P time is as follows:


#1 – The proposition can be stated in a high level language such as Pascal or C# that runs on a Von

Neuman architecture machine with a stack and a heap inside the internals of the software

architecture. The running time is thus no worse than O((log(2) of N)^2) But that running time is no

worse than O(n^2) which is a polynomial.


#2 – The proposition also has the characteristic that it runs on a hypothetical construct which is an AST

in the form of an infinite binary tree. This is exactly the idea of the machine. The processing of the

AST occurs inside the high level C#-like language.


#3 – The proposition has the added characteristic that the memory accesses of the AST occur in k

(constant) Order Time.


#4 – It therefore follows that the running time of the enumeration of the binary tree has an outer algebraic

construct of O(n log n), (the time to traverse an AST), times the Big O of the inner construct, which is

a black box in the theory of “Structured Programming”.


#5 – The internal running time of the black box is no worse than O(n^2) when the memory accesses of the

internal mechanism that operates the black box run in k (constant) order time.


V. PROGRAMMING OF THE ALGORITHM


We created a piece of software called “NPCOMP” whose purpose is to implement the above mentioned

algorithms in the C# Programming Language. Our intent was to not only demonstrate that it solves the

SAT problem in polynomial order time but that it could also be used to further a real world application of

the idea which we chose to be the problem of logic circuit layout for computer architecture. This is one

of many applications which could have been chosen to make a demo example that solves a real world

problem. The SAT algorithm is one small component of this software. Currently, the software is under

development.


V. CONCLUSION AND FUTURE WORK


Our intent is to deliver the software solution to the general public as a desirable application. The payoff

of this work is when SAT is applied to the MaxSAT algorithm as a subroutine. This is how the internal

mechanism of the logic circuit design software works. It is designed to minimize the physical size of the

logic circuitry to save electricity and also run faster when the circuit is smaller. MaxSAT is a special

case of SAT that invokes SAT as a subroutine. MaxSAT may be used to solve for Linear Programming or

Integer Linear Programming by a process that treats the solution with Binary Coded Decimal numbers.

MaxSAT takes the SAT algorithm and puts it to use as a more real world type of optimization problem

suitable for turning NPCOMP into a host of various software packages that ca be implemented for all of

the various cases of the NP-Complete Problems. Here is the general outline of the design of the coding for

MaxSAT. (It is not pseudo-code, but it is written as an English language description).


1. Let there be a function which counts the size of the final solution SAT expression. An example of such

a function is to add up all of the nodes in the binary tree with an additional weight per node based on the

size of that node’s leaves. There are more than one of these functions possible in the general case of the

design of electrical circuits, but this one is the most common and the most needed.


2. State the size as the result of the addition of several Boolean numbers where each of these numbers is

the individual size elements in #1.


3. State the addition of the Boolean numbers a collection of Boolean SAT problems, one for each of the

Boolean digits in the binary number that stands for the total size.

4. Solve the bits as SAT problems in the order of the highest order bit to the lowest order bit. You are

solving for the values of the literals in the original SAT expression and trying to derive the values that

stand for the individual nodes variables in the original SAT expression.


5. To minimize the number of the circuit, try to solve the bit as a 0 first, and then proceed to the next bit,

Taking 1 as the solution only in the worst case. This means that the variables bound in the prior bit

become activated in the next SAT solution bit problem.


6. After resolving which nodes are SAT or not SAT in the original expression, go back and prune out

those nodes which are either 100% SAT, (replace them with T for True), or 100% !SAT, (replace them with F

for False). This yields the final expression for the original SAT expression minimized to the maximum extent

which it can be minimized.


7. If the original expression is either 100% SAT or 100% !SAT, record that fact to minimize the solution

that chosen literal value of T or F.


REFERENCES


1. Knuth, Donald, “The Art of Computer Programming” Volume 1 – Fundamental Algorithms,

Addison Wesley, 1968

2. Gary, Michael R. and Johnson, David S., “Guide to the Theory of NP-Completeness”, W. S.

Freeman and Co., 1979

3. Woeginger, G.J., “P versus NP”, http://www.win.tue.nl/~gwoegi/Pversus-NP.htm, Sept. 26, 2016

4. SATLive.org, “SAT Live!”, http://www.satlive.org/, June 29, 2017

5. Dharwadker, Ashay and Tevet, John-Tagore, “The Graph Isomorphism Algorithm”,

http://www.dharwadker.org/tevet/isomorphism/main.html, 2009




The following is a proposed paper for discussing the mechanism of the "Equivalence Algorithm" developed by myself to address the problem of showing that P=NP.


Outline of Paper on Equivalance Algorithm

1. Gojer SAT Algorithm Runs in P-Time

1. Runs on a Turing Machine

2. Show that the Turing Machine is Equal to an Array of Lists (Status of Memory)

3. The Length of One List <= P

4. The Width of One List (# of Lists) <= P

2. Gojer SAT Algorithm Solves SAT

1. Runs on a Turing Machine

2. Proof by Induction

1. Show correct for Trivial Case

2. Show that the cases above the Trivial Case Can be Placed into a Structure

3. Show that each and every path through the structure can be proven by induction

3. Gojer Algorithm Can Be Proven with a Genetic Algorithm

1. Generate Randomly Produced Axioms of Logic

2. Create a Nearness Function

3. Use the Goal Problem Solver Paradigm

4. Create a Function that Estimates the Feasibility of the Genetic Algorithm to Solve the Solution

Second Iteration of the Proof:

1. Two identical expressions can be tested for equivalance in P time

2. Two non-identical expressions might be equivalent if one can be successfully transformed into the other

3. The textbook solutions run in exponential time

4. A boolean expression can be codified in the Calculus (of Newton)

5. The Calculus can be used to test for equivalence.

6. The new algorithm can be shown to run in P time

1. The Unit Step Function can be codified in the Calculus

2. The AND function can be codified in the Calculus

3. The OR function can be codified in the Calculus

4. A complex boolean expression can be codified using a tree algorithm to express it with those axioms

7. Manipulations fall on a derivation tree if the list of manipulations is finite

8. The expression for an equivalance test can be derived with N generation functions

9. The Unit Step Function can be used to say (There exists solution <= N size)

1. "Int(0,inf,summation clause on integer solution)"

10. That expression is no longer than K (size of input) steps so P=NP


The following is the original Pascal program p1.pas which implements the P=NP Solution except for the fact that it does not contain the coding for the "Equivalence Algorithm" - so that it would not constitute a perfect solution to P=NP, but it successfully encodes the basic outline of the algorithm in terms of the three grammatical cases of ST problems.




{---------------------------------------------------------------------}

{ p1.pas - Solution of the Circuit Satisfiability Problem }

{ (c) 2008 by Leonard Gojer }

{ }

{---------------------------------------------------------------------}

{ }

{ circuit Satisfiability is a problem member of the NP-Complete }

{ Problems, which is about the computional complexity of certain }

{ common problems in computer science. }

{ }

{ Since this is a solution of one part, by definition it is a }

{ theoretical solution of the entire problem. }

{ }

{ The circuit satisfiability problem concerns itself with the }

{ problem of finding the allowable input values to a boolean }

{ expression to make it true within a polynomial order time. }

{ }

{ It was previously believed to take a factorial or exponential }

{ order time, but this algorithm demonstrates a polynomial order }

{ solution. }

{ }

{ The algorithm proceeds as follows: first, the expression is parsed. }

{ The intermediate results are placed into an abstract syntax tree, }

{ which is stored in a flat-file database. }

{ }

{ Second, the expression is analyzed by a recursive algorithm. }

{ This special algorithm is based on the premise that: if the }

{ expression is not satisfiable, then it must contain a logical }

{ contradiction of the form - "A and NOT A". which includes all }

{ contradictions of the form - "Expression A and NOT Expression A." }

{ }

{ The algorithm is shown to be a polynomial order algorithm by the }

{ fact that it's program loops can be inspected methodically. }

{ }

{ The outer loop is no worse than N * (Height of the Expression) }

{ where the height of the expression is log N. Therefore, the }

{ outer loop is no worse than N*log N. }

{ }

{ The inner loop is no worse than 4 * (Height of the Expression) }

{ because the "equivalence" algorithm is designed as such. }

{ But also add N to the expression for the inner loop to account for }

{ the variable search in the variable table. }

{ }

{ Therefore, the total order of the algorithm is no worse than }

{ N * log (4 * ( log N + N) ) }

{ }

{ Which is within O(n^3) }

{ }

{---------------------------------------------------------------------}

{ }

{ PROGRAM ORGANIZATION: }

{ }

{ The subroutines of the code to the solution are roughly divided }

{ into three groups: the flat-file database for the binary trees; }

{ the parser, and the satisfiability analyzer. }

{ }

{ The parser and satisfiability routine are inspired by the design }

{ of compilers as set forth in the traditional compiler design texts. }

{ }

{ In addition, there is a "console" routine, which allows the user }

{ to execute batch runs, and also convert cnf expressions to the }

{ form used by this program. }

{ }

{ REMARKS CONCERNING THE PRIOR VERSION OF THIS PROGRAM: }

{ }

{ The first version of this program that was produced and copy- }

{ writed claimed that it was the working solution of the NP-complete }

{ problems, and it almost was, because it had many of the features }

{ of this program, but it was lacking in certain structural }

{ facets that make this the true first working solution of the }

{ NP-complete problems. }

{ }

{ Specifically, these parts of the program pertain to the current }

{ idea of the s-equivalence and c-equivalence of boolean expressions. }

{ These two terms stand for "simple equivalence" and "complex }

{ equivalence." It is this difference that makes this program now }

{ "completely" correct, in the sense that if it doesn't solve every }

{ case given to it, it should solve a very large number of cases. }

{ }

{ A detailed explanation of the algorithm requires several pages of }

{ text. }

{ }

{---------------------------------------------------------------------}

program p1;

const

dfname = 'data1.txt'; { main data file for algorithm }

exmax = 10000; { maximum number of records }

vmax = 1000; { maximum number of variables }

debugp = false; { 1st debugging flag }

debugp1 = false; { parse debugging flag }

debugs1 = false; { sat debugging flag }

type

dbrec = record { main type for data file }

key : integer; { key index of records }

data : string; { text of records }

left : integer; { left ptr of records }

right : integer; { right ptr of records }

literal : integer; { literal code flag for record }

entrance1 : integer; { entrance code flag of record }

exit1 : integer; { exit code flag for records }

end;

texttype = record { main type for input data }

size : integer; { number of records in input }

data : array[1..exmax] of char; { main data var for input }

end;

vartabletype = record { type for variable list }

size : integer; { size of data }

data : array[1..vmax] of string; { data to variable list }

exit : array[1..vmax] of integer;{ exit value to variable list }

end;

var

str1 : string; { temporary string #1 }

str2 : string; { temporary string #2 }

str3 : string; { temporary string #3 }

str4 : string; { temporary string #4 }

file1 : file of dbrec; { file ptr to dfname }

rec1 : dbrec; { temporary file var to dfname }

rec2 : dbrec; { temporary file var to dfname }

ptr : integer; { temporary ptr var }

tptr : integer; { temporary ptr var }

dbptr : integer; { temporary ptr var }

fid : text; { file var for input }

ffid : text; { file var for batch input }

expression1 : texttype; { var for input data }

str2a : string; { temporary string 2a }

illegalcode : integer; { flag for illegal input }

rootptr : integer; { ptr at root of expression }

vartable1 : vartabletype; { variable table }


{---------------------------------------------------------------------}

{ Forward Declarations: }

{---------------------------------------------------------------------}


{ to find empty records in data file structure }

procedure getfree1(var ptr : integer); forward;


{ to flip bits in the logic }

function flip(i1 : integer) : integer; forward;



{---------------------------------------------------------------------}

{ The following Procedures are file-db related: }

{ }

{ The first few routines are "elementary" operations on the db, such }

{ as initializing, reading and writing one record at a time. }

{ The next set of routines in this set are to add and/or list entire }

{ trees of boolean expressions, calling the elementary operations as }

{ subroutines. }

{ }

{ initfile }

{ listrec }

{ insertrec }

{ insertrec2 }

{ insertrec3 }

{ deleterec }

{ changerec }

{ changerec2 }

{ changerec3 }

{ listall }

{ getrec1 }

{ findeol }

{ add2treelist }

{ listtree }

{ listtreesub }

{---------------------------------------------------------------------}


{---------------------------------------------------------------------}

{ InitFile - to initialize the data file }

{---------------------------------------------------------------------}

procedure initfile;

begin

assign(file1,dfname);

rewrite(file1);

rec1.key := 1;

rec1.data := '';

rec1.left := 0;

rec1.right := 0;

rec1.literal := 0;

rec1.entrance1 := 0;

rec1.exit1 := 0;

write(file1,rec1);

close(file1);

end;

{---------------------------------------------------------------------}

{ Str2Int - to convert strings to integers }

{---------------------------------------------------------------------}

procedure str2int(str1 : string; var int1 : integer);

var

i1 : integer; { loop counter variable }

begin

int1 := 0;

for i1 := 1 to length(str1) do

begin

int1 := int1*10 + ord(str1[i1]) - ord('0');

end;

end;


{---------------------------------------------------------------------}

{ ListRec - to list one record in data file }

{---------------------------------------------------------------------}

procedure listrec(recno : integer);

var

i1 : integer; { loop counter variable }

begin

assign(file1,dfname);

reset(file1);

for i1 := 1 to recno do

read(file1,rec1);

writeln('Key: ',rec1.key);

writeln('Data: ',rec1.data);

writeln('Left: ',rec1.left);

writeln('Right: ',rec1.right);

writeln('Literal: ',rec1.literal);

writeln('Entrance: ',rec1.entrance1);

writeln('Exit: ',rec1.exit1);

close(file1);

end;


{---------------------------------------------------------------------}

{ InsertRec - to insert one record in the data file }

{---------------------------------------------------------------------}

procedure insertrec(recno : integer; str4 : string; entrance : integer);

var

i1 : integer; { loop counter variable }

count1 : integer; { counter variable }

begin

assign(file1,dfname);

reset(file1);

read(file1,rec1);

count1 := rec1.key;

if (recno > count1) then

begin

close(file1);

assign(file1,dfname);

reset(file1);

for i1 := 1 to count1 do

read(file1,rec1);

rec1.key := 0;

rec1.data := '';

rec1.left := 0;

rec1.right := 0;

rec1.literal := 0;

if (recno = rootptr) then

begin

rec1.entrance1 := 1;

if (rec1.data = '.not.') then

begin

rec1.exit1 := 1;

end;

if (rec1.data <> '.not.') then

begin

rec1.exit1 := 0;

end;

end;

if (recno <> rootptr) then

begin

if (rec1.data <> '.not.') then

begin

if (entrance = 0) then

begin

rec1.entrance1 := 0;

rec1.exit1 := 0;

end;

if (entrance = 1) then

begin

rec1.entrance1 := 1;

rec1.exit1 := 1;

end;

end;

if (rec1.data = '.not.') then

begin

if (entrance = 0) then

begin

rec1.entrance1 := 0;

rec1.exit1 := 1;

end;

if (entrance = 1) then

begin

rec1.entrance1 := 1;

rec1.exit1 := 0;

end;

end;

end;

for i1 := 1 to (recno - count1 - 1) do

write(file1,rec1);

rec1.key := recno;

rec1.data := str4;

write(file1,rec1);

close(file1)

end

else

begin

close(file1);

end;

assign(file1,dfname);

reset(file1);

read(file1,rec1);

rec2 := rec1;

close(file1);

assign(file1,dfname);

reset(file1);

if (recno - count1 >= 0) then

rec2.key := rec2.key + (recno - count1);

write(file1,rec2);

close(file1);

end;


{---------------------------------------------------------------------}

{ InsertRec2 - to insert one record in data file }

{---------------------------------------------------------------------}

procedure insertrec2(recno,recno2,recno3 : integer; str4 : string; entrance : integer);

var

i1 : integer; { loop counter variable }

count1 : integer; { counter variable }

begin

assign(file1,dfname);

reset(file1);

read(file1,rec1);

count1 := rec1.key;

if (recno > count1) then

begin

close(file1);

assign(file1,dfname);

reset(file1);

for i1 := 1 to count1 do

read(file1,rec1);

rec1.key := 0;

rec1.data := '';

rec1.left := 0;

rec1.right := 0;

rec1.literal := 0;

for i1 := 1 to (recno - count1 - 1) do

read(file1,rec1);

rec1.key := recno;

rec1.left := recno2;

rec1.right := recno3;

rec1.data := str4;

if (recno = rootptr) then rec1.entrance1 := 1;

if (rec1.data <> '.not.') then

begin

if (entrance = 0) then

begin

rec1.entrance1 := 0;

rec1.exit1 := 0;

end;

if (entrance = 1) then

begin

rec1.entrance1 := 1;

rec1.exit1 := 1;

end;

end;

if (rec1.data = '.not.') then

begin

if (entrance = 0) then

begin

rec1.entrance1 := 0;

rec1.exit1 := 1;

end;

if (entrance = 1) then

begin

rec1.entrance1 := 1;

rec1.exit1 := 0;

end;

end;

write(file1,rec1);

close(file1)

end

else

begin

close(file1);

assign(file1,dfname);

reset(file1);

for i1 := 1 to (recno - 1) do

read(file1,rec1);

rec1.key := recno;

rec1.data := str4;

rec1.left := recno2;

rec1.right := recno3;

rec1.literal := 0;

if (recno = rootptr) then rec1.entrance1 := 1;

if (rec1.data = '.not.') then

begin

if (entrance = 0) then

begin

rec1.entrance1 := 0;

rec1.exit1 := 1;

end;

if (entrance = 1) then

begin

rec1.entrance1 := 1;

rec1.exit1 := 0;

end;

end;

if (rec1.data <> '.not.') then

begin

if (entrance = 0) then

begin

rec1.entrance1 := 0;

rec1.exit1 := 0;

end;

if (entrance = 1) then

begin

rec1.entrance1 := 1;

rec1.exit1 := 1;

end;

end;

write(file1,rec1);

close(file1);

end;

assign(file1,dfname);

reset(file1);

read(file1,rec1);

rec2 := rec1;

close(file1);

assign(file1,dfname);

reset(file1);

if (recno - count1 >= 0) then

rec2.key := rec2.key + (recno - count1);

if (recno > rec2.key) then rec2.key := recno;

write(file1,rec2);

close(file1);

end;


{---------------------------------------------------------------------}

{ InsertRec3 - to insert one record in data file (for literals) }

{---------------------------------------------------------------------}

procedure insertrec3(recno,recno2,recno3 : integer; str4 : string; entrance : integer);

var

i1 : integer; { loop counter variable }

count1 : integer; { counter variable }

begin

assign(file1,dfname);

reset(file1);

read(file1,rec1);

count1 := rec1.key;

if (recno > count1) then

begin

close(file1);

assign(file1,dfname);

reset(file1);

for i1 := 1 to count1 do

read(file1,rec1);

rec1.key := 0;

rec1.data := '';

rec1.left := 0;

rec1.right := 0;

rec1.literal := 0;

for i1 := 1 to (recno - count1 - 1) do

read(file1,rec1);

rec1.key := recno;

rec1.left := recno2;

rec1.right := recno3;

rec1.data := str4;

if (recno = rootptr) then rec1.entrance1 := 1;

if (rec1.data = '.not.') then

begin

if (entrance = 0) then

begin

rec1.entrance1 := 0;

rec1.exit1 := 1;

end;

if (entrance = 1) then

begin

rec1.entrance1 := 1;

rec1.exit1 := 0;

end;

end;

if (rec1.data <> '.not.') then

begin

if (entrance = 0) then

begin

rec1.entrance1 := 0;

rec1.exit1 := 0;

end;

if (entrance = 1) then

begin

rec1.entrance1 := 1;

rec1.exit1 := 1;

end;

end;

write(file1,rec1);

close(file1)

end

else

begin

close(file1);

assign(file1,dfname);

reset(file1);

for i1 := 1 to (recno - 1) do

read(file1,rec1);

rec1.key := recno;

rec1.data := str4;

rec1.left := recno2;

rec1.right := recno3;

rec1.literal := 1;

if (recno = rootptr) then rec1.entrance1 := 1;

if (rec1.data = '.not.') then

begin

if (entrance = 0) then

begin

rec1.entrance1 := 0;

rec1.exit1 := 1;

end;

if (entrance = 1) then

begin

rec1.entrance1 := 1;

rec1.exit1 := 0;

end;

end;

if (rec1.data <> '.not.') then

begin

if (entrance = 0) then

begin

rec1.entrance1 := 0;

rec1.exit1 := 0;

end;

if (entrance = 1) then

begin

rec1.entrance1 := 1;

rec1.exit1 := 1;

end;

end;

write(file1,rec1);

close(file1);

end;

assign(file1,dfname);

reset(file1);

read(file1,rec1);

rec2 := rec1;

close(file1);

assign(file1,dfname);

reset(file1);

if (recno - count1 >= 0) then

rec2.key := rec2.key + (recno - count1);

if (recno > rec2.key) then rec2.key := recno;

write(file1,rec2);

close(file1);

end;



{---------------------------------------------------------------------}

{ DeleteRec - to delete one record from data file }

{---------------------------------------------------------------------}

procedure deleterec(recno : integer);

var

i1 : integer; { loop counter variable }

count1 : integer; { counter variable }

begin

assign(file1,dfname);

reset(file1);

read(file1,rec1);

count1 := rec1.key;

if (recno <= count1) then

begin

close(file1);

assign(file1,dfname);

reset(file1);

for i1 := 1 to (recno - 1) do

read(file1,rec1);

rec1.key := 0;

rec1.data := '';

rec1.left := 0;

rec1.right := 0;

rec1.literal := 0;

rec1.entrance1 := 0;

rec1.exit1 := 0;

write(file1,rec1);

end;

close(file1);

end;


{---------------------------------------------------------------------}

{ ChangeRec - to change one record in data file }

{---------------------------------------------------------------------}

procedure changerec(recno : integer; str4 : string);

var

i1 : integer; { loop counter variable }

count1 : integer; { counter variable }

begin

assign(file1,dfname);

reset(file1);

read(file1,rec1);

count1 := rec1.key;

if (recno <= count1) then

begin

close(file1);

assign(file1,dfname);

reset(file1);

for i1 := 1 to recno do

read(file1,rec1);

rec2 := rec1;

close(file1);

assign(file1,dfname);

reset(file1);

for i1 := 1 to (recno - 1) do

read(file1,rec1);

rec1 := rec2;

rec1.key := recno;

rec1.data := str4;

if (rec2.exit1 = 0) then rec1.entrance1 := 0;

if (rec2.exit1 = 1) then rec1.entrance1 := 0;

write(file1,rec1);

end;

close(file1);

end;


{---------------------------------------------------------------------}

{ ChangeRec2 - to change one record in data file (by pointer rel.) }

{---------------------------------------------------------------------}

procedure changerec2(recno,recno2 : integer);

var

i1 : integer; { loop counter variable }

count1 : integer; { counter variable }

begin

assign(file1,dfname);

reset(file1);

read(file1,rec1);

count1 := rec1.key;

if (recno <= count1) then

begin

close(file1);

assign(file1,dfname);

reset(file1);

for i1 := 1 to recno do

read(file1,rec1);

rec2 := rec1;

close(file1);

assign(file1,dfname);

reset(file1);

for i1 := 1 to (recno - 1) do

read(file1,rec1);

rec1 := rec2;

rec1.key := recno;

rec1.left := recno2;

if (rec2.exit1 = 0) then rec1.entrance1 := 0;

if (rec2.exit1 = 1) then rec1.entrance1 := 1;

write(file1,rec1);

end;

close(file1);

end;


{---------------------------------------------------------------------}

{ ChangeRec3 - to change one record in data file }

{---------------------------------------------------------------------}

procedure changerec3(recno : integer; key1 : integer; data1 : string; left1 : integer; right1 : integer; literal1 : integer; entrance1 : integer; exit1 : integer);

var

i1 : integer; { loop counter variable }

count1 : integer; { counter variable }

begin

assign(file1,dfname);

reset(file1);

read(file1,rec1);

count1 := rec1.key;

if (recno <= count1) then

begin

close(file1);

assign(file1,dfname);

reset(file1);

for i1 := 1 to recno do

read(file1,rec1);

rec2 := rec1;

close(file1);

assign(file1,dfname);

reset(file1);

for i1 := 1 to (recno - 1) do

read(file1,rec1);

rec1 := rec2;

rec1.key := recno;

rec1.data := data1;

rec1.left := left1;

rec1.right := right1;

rec1.literal := literal1;

rec1.entrance1 := entrance1;

rec1.exit1 := exit1;

write(file1,rec1);

end;

close(file1);

end;


{---------------------------------------------------------------------}

{ ListAll - to list all records in data file }

{---------------------------------------------------------------------}

procedure listall;

var

count : integer; { counter variable }

begin

assign(file1,dfname);

reset(file1);

writeln;

writeln('List of Records in Data');

writeln;

count := 0;

while not eof(file1) do

begin

count := count + 1;

read(file1,rec1);

if (rec1.key <> 0) or (rec1.data <> '') or (rec1.left <> 0) or (rec1.right <> 0) or

(rec1.literal <> 0) or (rec1.entrance1 <> 0) or (rec1.exit1 <> 0) then

begin

if (count = 1) then

begin

writeln('Number of Records: ',rec1.key);

writeln

end

else

begin

writeln('Key : ',rec1.key);

writeln('Data : ',rec1.data);

writeln('Left : ',rec1.left);

writeln('Right : ',rec1.right);

writeln('Literal : ',rec1.literal);

writeln('Entrance : ',rec1.entrance1);

writeln('Exit : ',rec1.exit1);

writeln;

end;

end;

end;

close(file1);

end;


{---------------------------------------------------------------------}

{ GetRec1 - to retrieve one record in data file }

{---------------------------------------------------------------------}

procedure getrec1(recno : integer; var key : integer; var data1 : string; var left,right,literal,entrance1,exit1 : integer);

var

i1 : integer; { loop counter variable }

count1 : integer; { counter variable }

begin

assign(file1,dfname);

reset(file1);

read(file1,rec1);

count1 := rec1.key;

close(file1);

if (recno <= count1) then

begin

assign(file1,dfname);

reset(file1);

for i1 := 1 to recno do

read(file1,rec1);

key := rec1.key;

data1 := rec1.data;

left := rec1.left;

right := rec1.right;

literal := rec1.literal;

entrance1 := rec1.entrance1;

exit1 := rec1.exit1;

close(file1)

end

else

begin

key := 0;

data1 := '';

left := 0;

right := 0;

literal := 0;

entrance1 := 0;

exit1 := 0;

end;

end;


{---------------------------------------------------------------------}

{ FindEol - to find the end of file }

{---------------------------------------------------------------------}

procedure findeol(recno : integer; var eolrecno : integer);

var

key : integer; { temporary key variable }

data1 : string; { temporary data variable }

left : integer; { temporary left ptr variable }

right : integer; { temporary right ptr variable }

literal : integer; { temporary literal flag variable }

entrance1 : integer; { temporary entrance value variable }

exit1 : integer; { temporary exit value variable }

begin

getrec1(recno,key,data1,left,right,literal,entrance1,exit1);

while (recno = key) do

begin

recno := left;

getrec1(recno,key,data1,left,right,literal,entrance1,exit1);

end;

end;


{---------------------------------------------------------------------}

{ Add2TreeList - to add to the list of trees }

{---------------------------------------------------------------------}

procedure add2treelist(recno,recno2 : integer);

var

key : integer; { temporary key variable }

data1 : string; { temporary data variable }

left : integer; { temporary left ptr variable }

right : integer; { temporary right ptr variable }

literal : integer; { temporary literal flag variable }

entrance1 : integer; { temporary entrance value variable }

exit1 : integer; { temporary exit value variable }

eolrecno : integer; { end of line record number }

aftereolrecno : integer; { after end of line record number }

begin

getrec1(recno,key,data1,left,right,literal,entrance1,exit1);

eolrecno := 0;

if (key = recno) then

begin

findeol(recno,eolrecno);

end;

getfree1(aftereolrecno);

if (eolrecno <> 0) then

changerec2(eolrecno,aftereolrecno);

insertrec2(aftereolrecno,recno2,0,'',entrance1);

end;


{---------------------------------------------------------------------}

{ ListTree - to list a tree }

{---------------------------------------------------------------------}

procedure listtree(recno : integer);

var

key : integer; { temporary key variable }

data1 : string; { temporary data variable }

left : integer; { temporary left ptr variable }

right : integer; { temporary right ptr variable }

literal : integer; { temporary literal flag variable }

entrance1 : integer; { temporary entrance value variable }

exit1 : integer; { temporary exit value variable }

begin

getrec1(recno,key,data1,left,right,literal,entrance1,exit1);

writeln('Rec: ',data1);

if (left <> 0) then listtree(left);

if (right <> 0) then listtree(right);

end;


{---------------------------------------------------------------------}

{ ListTreeSub - to list the subtree of a tree }

{---------------------------------------------------------------------}

procedure listtreesub(recno : integer);

var

key : integer; { temporary key variable }

data1 : string; { temporary data variable }

left : integer; { temporary left ptr variable }

right : integer; { temporary right ptr variable }

literal : integer; { temporary literal flag variable }

entrance1 : integer; { temporary entrance value variable }

exit1 : integer; { temporary exit value variable }

begin

getrec1(recno,key,data1,left,right,literal,entrance1,exit1);

writeln('Listing Tree:');

listtree(recno);

if (left <> 0) then listtreesub(left);

if (right <> 0) then listtreesub(right);

end;


{---------------------------------------------------------------------}

{ }

{ Next, what follows is the parsing algorithm, which is composed of }

{ several subroutines that optionally access debugging routines. }

{ }

{ The parsing algorithm is a recursive algorithm that typical from }

{ the theory of compiler design. }

{ }

{ The following procedures are parsing related: }

{ }

{ The parser is based on the following grammatical hierarchy: }

{ }

{ () - parenthesis }

{ .and. - "and" expression }

{ .or. - "or" expression }

{ .not. - "not" expression }

{ [ABC..0..789] - "literal" composed of letters followed by numbers }

{ and/or letters }

{ }

{ In addition there are routines for the batch processing of regular }

{ as well as cnf expressions. }

{ }

{ parsefile2 }

{ listtreesubf }

{ getexpression1 }

{ haszeropcount }

{ hasnot }

{ findstring }

{ hasand }

{ hasor }

{ pushnot }

{ pushand }

{ pushor }

{ computestartend }

{ computestartend2 }

{ hasliteral }

{ getliteral }

{ pushliteral }

{ illegal }

{ parseexpression1 }

{ parsefile }

{ parseexpression2 }

{ cnf2text }

{ str2int }

{ parse1 }

{ batchcnf2text }

{---------------------------------------------------------------------}


{---------------------------------------------------------------------}

{ ParseFile2 - to parse a tree into a tree structure }

{---------------------------------------------------------------------}

procedure parsefile2(recno : integer);

var

key : integer; { temporary key variable }

data1 : string; { temporary data variable }

left : integer; { temporary left pointer variable }

right : integer; { temporary right pointer variable }

literal : integer; { temporary literal flag variable }

entrance1 : integer; { temporary entrance value variable }

exit1 : integer; { temporary exit value variable }

ptrf : integer; { pointer into file }

ptrl : integer; { left pointer }

ptrr : integer; { right pointer }

begin

getrec1(recno,key,data1,left,right,literal,entrance1,exit1);

getfree1(ptrf);

ptrl := 0;

ptrr := 0;

if (left <> 0) then

begin

getfree1(ptrl);

end;

if (right <> 0) then

begin

getfree1(ptrr);

end;


{---------------------------------------------------------------------}

if debugp then writeln('Rec: ',data1);

{---------------------------------------------------------------------}


insertrec2(ptrf,ptrl,ptrr,data1,entrance1);

if (left <> 0) then parsefile2(left);

if (right <> 0) then parsefile2(right);

end;


{---------------------------------------------------------------------}

{ ListTreeSubf - to list trees and subtrees to the master data struc. }

{---------------------------------------------------------------------}

procedure listtreesubf(recno : integer);

var

key : integer; { temporary key variable }

data1 : string; { temporary data variable }

left : integer; { temporary left ptr variable }

right : integer; { temporary right ptr variable }

literal : integer; { temporary literal flag variable }

entrance1 : integer; { temporary entrance value variable }

exit1 : integer; { temporary exit value variable }

begin

getrec1(recno,key,data1,left,right,literal,entrance1,exit1);


{---------------------------------------------------------------------}

if debugp then writeln('Listing Tree:');

{---------------------------------------------------------------------}


parsefile2(recno);

add2treelist(3,recno);

if (left <> 0) then listtreesubf(left);

if (right <> 0) then listtreesubf(right);

end;


{---------------------------------------------------------------------}

{ The satisfiability analysis is a recursive procedure invented by }

{ the author, and the purpose of this code is to check that it is }

{ correct and demonstrate as such to the general public. }

{ }

{ The following procedures are parts of the satisfiability analysis }

{ process: }

{ }

{ The main routine is called "satisfiable," it is a function that }

{ returns 1 or 0. It is a recursively defined function that was not }

{ expressed adequately by the previous version of this program. But }

{ now, I believe that it is stated correctly to get a very large }

{ number, if not all cases right. }

{ }

{ The feature that was missing from the previous program was the }

{ routines for finding the equivalence of boolean expressions. These }

{ new routines were checked to verify that they are polynomial order }

{ routines, and since they are subroutines of the main routine, it }

{ must therefore be that the order of the entire program is within a }

{ polynomial, even if the exact polynomial is difficult to derive. }

{ }

{ sequivalence }

{ simpleequivalence }

{ copy2db }

{ makeandintoor }

{ cequivalence }

{ complexequivalence }

{ flip }

{ haschildren }

{ satisfiable }

{ satisfiability }

{ p1batch }

{---------------------------------------------------------------------}


{---------------------------------------------------------------------}

{ Sequivalence - returns 0 or 1 for two subtrees equal }

{---------------------------------------------------------------------}

function sequivalence(recno1,recno2 : integer) : integer;

var

key1 : integer; { temporary key variable }

data1 : string; { temporary data variable }

left1 : integer; { temporary left ptr variable }

right1 : integer; { temporary right ptr variable }

literal1 : integer; { temporary literal flag variable }

entrance1 : integer; { temporary entrance value variable }

exit1 : integer; { temporary exit value variable }

key2 : integer; { temporary key variable #2 }

data2 : string; { temporary data variable #2 }

left2 : integer; { temporary left ptr variable #2 }

right2 : integer; { temporary right ptr variable #2 }

literal2 : integer; { temporary literal flag #2 }

entrance2 : integer; { temporary entrance value #2 }

exit2 : integer; { temporary exit value #2 }

result1a : integer; { intermediate result variable }

result1b : integer; { intermediate result variable }

result2a : integer; { intermediate result variable }

result2b : integer; { intermediate result variable }

result1 : integer; { intermediate result variable }

result2 : integer; { intermediate result variable }

result : integer; { intermediate result variable }

begin

if (recno1 <> 0) and (recno2 <> 0) then

begin

getrec1(recno1,key1,data1,left1,right1,literal1,entrance1,exit1);

getrec1(recno2,key2,data2,left2,right2,literal2,entrance2,exit2);

if (data1 = data2) then

begin

if (left1 <> 0) and (left2 <> 0) then

result1a := sequivalence(left1,left2);

if (left1 = 0) and (left2 <> 0) then

result1a := 0;

if (left1 <> 0) and (left2 = 0) then

result1a := 0;

if (left1 = 0) and (left2 = 0) then

begin

result1a := 0;

if (data1 = data2) then result1a := 1;

end;

if (right1 <> 0) and (right2 <> 0) then

result1b := sequivalence(right1,right2);

if (right1 = 0) and (right2 <> 0) then

result1b := 0;

if (right1 <> 0) and (right2 = 0) then

result1b := 0;

if (right1 = 0) and (right2 = 0) then

begin

result1b := 0;

if (data1 = data2) then result1b := 1;

end;

result1 := 0;

if (result1a = 1) and (result1b = 1) then result1 := 1;

if (left1 <> 0) and (right2 <> 0) then

result2a := sequivalence(left1,right2);

if (left1 = 0) and (right2 <> 0) then

result2a := 0;

if (left1 <> 0) and (right2 = 0) then

result2a := 0;

if (left1 = 0) and (right2 = 0) then

begin

result2a := 0;

if (data1 = data2) then result2a := 1;

end;

if (right1 <> 0) and (left2 <> 0) then

result2b := sequivalence(right1,left2);

if (right1 = 0) and (left2 <> 0) then

result2b := 0;

if (right1 <> 0) and (left2 = 0) then

result2b := 0;

if (right1 = 0) and (left2 = 0) then

begin

result2b := 0;

if (data1 = data2) then result2b := 1;

end;

result2 := 0;

if (result2a = 1) and (result2b = 1) then result2 := 1;

result := 0;

if (result1 = 1) or (result2 = 1) then result := 1;

end;

if (data1 <> data2) then result := 0;

sequivalence := result;

end

else

begin

if (recno1 <> 0) or (recno2 <> 0) then sequivalence := 0;

end;

end;


{---------------------------------------------------------------------}

{ SimpleEquivalence - master routine to s-equivalence }

{---------------------------------------------------------------------}

procedure simpleequivalence(recno1,recno2 : integer; var result1 : integer);

begin

result1 := sequivalence(recno1,recno2);

end;


{---------------------------------------------------------------------}

{ Copy2db - to copy a subtree to another subtree }

{---------------------------------------------------------------------}

procedure copy2db(recno1 : integer; recno2 : integer);

var

key : integer; { temporary key variable }

data1 : string; { temporary data variable }

left : integer; { temporary left ptr variable }

right : integer; { temporary right ptr variable }

literal : integer; { temporary literal flag variable }

entrance1 : integer; { temporary entrance value variable }

exit1 : integer; { temporary exit value variable }

recnol : integer; { temporary left record ptr }

recnor : integer; { temporary right record ptr }

begin

getrec1(recno1,key,data1,left,right,literal,entrance1,exit1);

if (left <> 0) then getfree1(recnol);

if (right <> 0) then getfree1(recnor);

changerec3(recno2,recno2,data1,recnol,recnor,literal,entrance1,exit1);

writeln('Rec: ',data1);

if (left <> 0) then

begin

copy2db(left,recnol);

end;

if (right <> 0) then

begin

copy2db(right,recnor);

end;

end;


{---------------------------------------------------------------------}

{ MakeAndIntoOr - to copy an AND, converting it to an OR }

{---------------------------------------------------------------------}

procedure makeandintoor(recno1,recno2 : integer);

var

key1 : integer; { temporary key value variable }

data1 : string; { temporary data value variable }

left1 : integer; { temporary left ptr variable }

right1 : integer; { temporary right ptr variable }

literal1 : integer; { temporary literal value variable }

entrance1 : integer; { temporary entrance value variable }

exit1 : integer; { temporary exit value variable }

recno3 : integer; { record ptr }

recno4 : integer; { record ptr }

begin

getrec1(recno1,key1,data1,left1,right1,literal1,entrance1,exit1);

if (data1 = '.and.') then

begin

insertrec(recno2,'.or.',entrance1);

getfree1(recno3);

getfree1(recno4);

left1 := recno3;

right1 := recno4;

key1 := recno2;

literal1 := 0;

entrance1 := 1;

exit1 := 1;

data1 := '.or.';

changerec3(recno2,key1,data1,left1,right1,literal1,entrance1,exit1);

copy2db(recno1,recno3);

copy2db(recno1,recno4);

end;

end;


{---------------------------------------------------------------------}

{ Cequivalence - returns 0 or 1 depending on complex equivalence }

{---------------------------------------------------------------------}

function cequivalence(recno1,recno2 : integer) : integer;

var

key1 : integer; { temporary key value variable }

data1 : string; { temporary data value variable }

left1 : integer; { temporary left ptr variable }

right1 : integer; { temporary right ptr variable }

literal1 : integer; { temporary literal flag variable }

entrance1 : integer; { temporary entrance value variable }

exit1 : integer; { temporary exit value variable }

key2 : integer; { temporary key value variable #2 }

data2 : string; { temporary data value variable #2 }

left2 : integer; { temporary left ptr variable #2 }

right2 : integer; { temporary right ptr variable #2 }

literal2 : integer; { temporary literal flag variable #2 }

entrance2 : integer; { temporary entrance variable #2 }

exit2 : integer; { temporary exit variable #2 }

result : integer; { result of equivalence }

recno3 : integer; { record ptr }

begin

getrec1(recno1,key1,data1,left1,right1,literal1,entrance1,exit1);

getrec1(recno2,key2,data2,left2,right2,literal2,entrance2,exit2);

if (data1 = '.and.') and (data2 = '.or.') then

begin

getfree1(recno3);

makeandintoor(recno1,recno3);

result := sequivalence(recno3,recno2);


{---------------------------------------------------------------------}

if debugs1 then writeln('debug 1');

{---------------------------------------------------------------------}


end;

if (data1 = '.or.') and (data2 = '.and.') then

begin

getfree1(recno3);

makeandintoor(recno2,recno3);

result := sequivalence(recno1,recno3);


{---------------------------------------------------------------------}

if debugs1 then writeln('debug 2');

{---------------------------------------------------------------------}


end;

if (data1 = '.and.') and (data2 = '.and.') then

begin

result := sequivalence(recno1,recno2);


{---------------------------------------------------------------------}

if debugs1 then writeln('debug 3');

{---------------------------------------------------------------------}


end;

if (data1 = '.or.') and (data2 = '.or.') then

begin

result := sequivalence(recno1,recno2);


{---------------------------------------------------------------------}

if debugs1 then writeln('debug 4');

{---------------------------------------------------------------------}


end;

if (data1 <> '.and.') and (data1 <> '.or.') and (data2 <> '.and.') and (data2 <> '.or.') then

begin

if (data1 = data2) then result := 1;

end;

if (recno1 = 0) or (recno2 = 0) then result := 1;

if (recno1 = 0) and (recno2 = 0) then result := 0;

cequivalence := result;

end;



{---------------------------------------------------------------------}

{ Complexequivalence - master routine to complex equivalence }

{---------------------------------------------------------------------}

procedure complexequivalence(recno1,recno2 : integer; var result1 : integer);

begin

result1 := cequivalence(recno1,recno2);

end;


{---------------------------------------------------------------------}

{ P1Console - the console routine for examining the data structure }

{---------------------------------------------------------------------}

procedure p1console(str1,str2,str3,str4 : string);

var

recno : integer; { record ptr }

recno1 : integer; { record ptr }

recno2 : integer; { record ptr }

result1 : integer; { temporary result }

entrance : integer; { entrance value of node }

begin

if (str2 = 'i') then

begin

str2int(str3,recno);

insertrec(recno,str4,entrance);

end;

if (str2 = 'd') then

begin

str2int(str3,recno);

deleterec(recno);

end;

if (str2 = 'c') then

begin

str2int(str3,recno);

changerec(recno,str4);

end;

if (str2 = 'l') then

begin

str2int(str3,recno);

listrec(recno);

end;

if (str2 = 'a') then

begin

listall;

end;

if (str2 = 'x') then

begin

initfile;

end;

if (str2 = 'it') then

begin

str2int(str3,recno);

str2int(str4,recno2);

add2treelist(recno,recno2);

end;

if (str2 = 'lt') then

begin

str2int(str3,recno);

listtree(recno);

end;

if (str2 = 'ls') then

begin

str2int(str3,recno);

listtreesub(recno);

end;

if (str2 = 'lsf') then

begin

str2int(str3,recno);

listtreesubf(recno);

end;

if (str2 = 'se') then

begin

str2int(str3,recno1);

str2int(str4,recno2);

simpleequivalence(recno1,recno2,result1);

if (result1 = 1) then writeln('Equivalent under Simple Equivalence');

if (result1 = 0) then writeln('Not Equivalent under Simple Equivalence');

end;

if (str2 = 'ce') then

begin

str2int(str3,recno1);

str2int(str4,recno2);

complexequivalence(recno1,recno2,result1);

if (result1 = 1) then writeln('Equivalent under Complex Equivalence');

if (result1 = 0) then writeln('Not Equivalent under Complex Equivalence');

end;

if (str2 = 'ao') then

begin

str2int(str3,recno1);

getfree1(recno2);

makeandintoor(recno1,recno2);

end;

if (str2 = 'h') then

begin

writeln;

writeln('Program p1.pas - Solution of Circuit Satisfiability. (c) 2008 by Leonard Gojer');

writeln('------------------------------------------------------------------------------');

writeln('How to Use Commands:');

writeln('------------------------------------------------------------------------------');

writeln('i - insert one record into binary tree db');

writeln('d - delete one record from binary tree db');

writeln('c - create one record in binary tree db');

writeln('l - list one record from binary tree db');

writeln('a - list all records in binary tree db');

writeln('x - initialize binary tree db');

writeln('it - insert extra tree into binary tree db');

writeln('lt - list extraneous tree from binary tree db');

writeln('ls - list all subtrees at a node in the binary tree db');

writeln('lsf - list all subtrees at a node in the binary tree (to the db file)');

writeln('se - run a test for simple equivalence');

writeln('ce - run a test for complex equivalence');

writeln('ao - convert an "and" expression into an "or" expresion. (in db)');

writeln('h - display this help screen');

writeln('------------------------------------------------------------------------------');

writeln;

end;

end;


{---------------------------------------------------------------------}

{ FindEmpty - to find an empty record in the data structure }

{---------------------------------------------------------------------}

procedure findempty(var ptr1 : integer; var success1 : boolean);

var

count : integer; { counter variable }

begin

assign(file1,dfname);

reset(file1);

success1 := false;

ptr1 := 0;

count := 0;

while not eof(file1) do

begin

count := count + 1;

read(file1,rec1);

if (rec1.key = 0) then

begin

success1 := true;

ptr1 := count;

end;

end;

close(file1);

if (ptr1 = 0) then

begin

assign(file1,dfname);

reset(file1);

read(file1,rec1);

ptr1 := rec1.key + 1;

close(file1);

end;

end;


{---------------------------------------------------------------------}

{ FindEmpty2 - to find an empty record in the data structure }

{---------------------------------------------------------------------}

procedure findempty2(nptr : integer; var ptr1 : integer; var success1 : boolean);

var

count : integer; { counter variable }

begin

assign(file1,dfname);

reset(file1);

success1 := false;

ptr1 := 0;

count := 0;

while not eof(file1) do

begin

count := count + 1;

read(file1,rec1);

if (rec1.key = 0) and (count <> nptr) then

begin

success1 := true;

ptr1 := count;

end;

end;

close(file1);

if (ptr1 = 0) then

begin

assign(file1,dfname);

reset(file1);

read(file1,rec1);

ptr1 := rec1.key + 1;

close(file1);

end;

end;


{---------------------------------------------------------------------}

{ MakeEmpty - to find an empty record in the data structure }

{---------------------------------------------------------------------}

procedure makeempty(var ptr1 : integer);

var

i1 : integer; { loop counter variable }

count : integer; { counter variable }

begin

assign(file1,dfname);

reset(file1);

read(file1,rec1);

rec2 := rec1;

count := rec1.key;

close(file1);

assign(file1,dfname);

reset(file1);

for i1 := 1 to count do

read(file1,rec1);

rec1.key := 0;

rec1.data := '';

rec1.left := 0;

rec1.right := 0;

rec1.literal := 0;

rec1.entrance1 := 0;

rec1.exit1 := 0;

write(file1,rec1);

close(file1);

ptr1 := count + 1;

assign(file1,dfname);

reset(file1);

if (ptr1 > 0) then

rec2.key := ptr1

else

begin

writeln('error:');

readln;

end;

write(file1,rec2);

close(file1);

end;


{---------------------------------------------------------------------}

{ MakeEmpty2 - to find an empty record in the data file (w/ ptr) }

{---------------------------------------------------------------------}

procedure makeempty2(nptr : integer; var ptr1 : integer);

var

i1 : integer; { loop counter variable }

count : integer; { counter variable }

begin

assign(file1,dfname);

reset(file1);

read(file1,rec1);

rec2 := rec1;

count := rec1.key;

close(file1);

if (nptr = count) and (nptr = ptr1) then

begin

assign(file1,dfname);

reset(file1);

while not eof(file1) do

read(file1,rec1);

rec1.key := 0;

rec1.data := '';

rec1.left := 0;

rec1.right := 0;

rec1.literal := 0;

rec1.entrance1 := 0;

rec1.exit1 := 0;

write(file1,rec1);

close(file1);

assign(file1,dfname);

reset(file1);

rec1.key := count + 1;

write(file1,rec1);

close(file1);

count := count + 1;

end;

assign(file1,dfname);

reset(file1);

for i1 := 1 to count do

read(file1,rec1);

rec1.key := 0;

rec1.data := '';

rec1.left := 0;

rec1.right := 0;

rec1.literal := 0;

rec1.entrance1 := 0;

rec1.exit1 := 0;

write(file1,rec1);

close(file1);

ptr1 := count + 1;

assign(file1,dfname);

reset(file1);

if (ptr1 > 0) then

rec2.key := ptr1

else

begin

writeln('error:');

readln;

end;

write(file1,rec2);

close(file1);

end;


{---------------------------------------------------------------------}

{ GetFree1 - to find an empty record in the data structure }

{---------------------------------------------------------------------}

procedure getfree1(var ptr : integer);

var

ptr1 : integer; { ptr variable }

success1 : boolean; { true if empty record found }

begin

findempty(ptr1,success1);

if not success1 then makeempty(ptr1);

ptr := ptr1;

end;


{---------------------------------------------------------------------}

{ GetFree2 - to find an empty record in the data structure }

{---------------------------------------------------------------------}

procedure getfree2(nptr : integer; var ptr : integer);

var

ptr1 : integer; { ptr variable }

success1 : boolean; { true if empty record found }

begin

findempty2(nptr,ptr1,success1);

if not success1 then makeempty2(nptr,ptr1);

ptr := ptr1;

end;


{---------------------------------------------------------------------}

{ GetExpression1 - to get an expression from the data input file }

{---------------------------------------------------------------------}

procedure getexpression1(str1 : string; var expression1 : texttype);

var

i1 : integer; { loop counter variable }

ch : char; { char of text }

begin

assign(fid,str1);

reset(fid);

expression1.size := 0;

for i1 := 1 to exmax do expression1.data[i1] := ' ';

while not eof(fid) do

begin

if not eoln(fid) then

begin

read(fid,ch);

expression1.size := expression1.size + 1;

expression1.data[expression1.size] := ch;

end;

if eoln(fid) then

readln(fid);

end;

close(fid);

end;


{---------------------------------------------------------------------}

{ HasZeroPCount - returns true if parentheses are internally balanced }

{---------------------------------------------------------------------}

function haszeropcount(expression1 : texttype; start,enda : integer) : boolean;

var

tmp : boolean; { temporary boolean flag }

count : integer; { counter variable }

i1 : integer; { loop counter variable }

begin

tmp := false;

count := 0;

for i1 := start to enda do

begin

if (expression1.data[i1] = '(') then count := count + 1;

if (expression1.data[i1] = ')') then count := count - 1;

if (i1 > start) and (i1 < enda) and (count = 0) then tmp := true;

end;

haszeropcount := tmp;

end;


{---------------------------------------------------------------------}

{ HasParenthesis - returns true if parenthesis expression }

{---------------------------------------------------------------------}

function hasparenthesis(var expression1 : texttype; start,enda : integer) : boolean;

var

tmp : boolean; { temporary boolean flag }

begin

tmp := false;

if (expression1.data[start] = '(') and (expression1.data[enda] = ')') then

tmp := true;

if haszeropcount(expression1,start,enda) then tmp := false;

hasparenthesis := tmp;

end;


{---------------------------------------------------------------------}

{ HasNot - returns true if NOT expression }

{---------------------------------------------------------------------}

function hasnot(var expression1 : texttype; start,enda : integer) : boolean;

var

tmp : boolean; { temporary boolean flag }

str1 : string; { piece of text }

begin

tmp := false;

str1 := expression1.data[start] + expression1.data[start+1] + expression1.data[start+2] + expression1.data[start+3] + expression1.data[start+4];

if (str1 = '.not.') then tmp := true;

hasnot := tmp;

end;


{---------------------------------------------------------------------}

{ FindString - to find a string within a string }

{---------------------------------------------------------------------}

procedure findstring(str1 : string; var expression1 : texttype; start1,enda : integer; var posstr : integer);

var

found : boolean; { true if string found in string }

i1 : integer; { loop counter variable }

str2 : string; { string within string }

i2 : integer; { loop counter variable }

begin

posstr := 0;

found := false;

for i1 := start1 to (enda - length(str1) + 1) do

begin

str2 := '';

for i2 := 1 to length(str1) do

str2 := str2 + expression1.data[i1+i2-1];

if not found and (str1 = str2) then

begin

found := true;

posstr := i1;

end;

end;

end;


{---------------------------------------------------------------------}

{ Hasand - returns true if AND expression }

{---------------------------------------------------------------------}

function hasand(var expression1 : texttype; start,enda : integer) : boolean;

var

tmp : boolean; { temporary boolean variable }

count : integer; { counter variable }

start1 : integer; { start of and side 1 }

end1 : integer; { end of and side 1 }

start2 : integer; { start of and side 2 }

end2 : integer; { end of and side 2 }

i1 : integer; { loop counter variable }

zerofound : boolean; { true if none found }

begin

count := 0;

start1 := 0;

end1 := 0;

start2 := 0;

end2 := 0;

tmp := false;

zerofound := false;

for i1 := start to enda do

begin

if (expression1.data[i1] = '(') then count := count + 1;

if (expression1.data[i1] = ')') then count := count - 1;

if (expression1.data[i1+1] = '.') and (expression1.data[i1+2] = 'a') and (count <= 1) and not zerofound then

begin

start1 := start;

end1 := i1;

start2 := i1 + 5;

end2 := enda;

tmp := true;

end;

if (expression1.data[i1+1] = '.') and (expression1.data[i1+2] = 'o') and (count = 0) then

begin

start1 := 0;

end1 := 0;

start2 := 0;

end2 := 0;

tmp := false;

zerofound := true;

end;

end;

if (enda - start < 4) then tmp := false;

hasand := tmp;

end;


{---------------------------------------------------------------------}

{ HasOR - returns true if OR expression }

{---------------------------------------------------------------------}

function hasor(var expression1 : texttype; start,enda : integer) : boolean;

var

tmp : boolean; { temporary boolean flag variable }

count : integer; { counter variable }

start1 : integer; { start of or side 1 }

end1 : integer; { end of or side 1 }

start2 : integer; { start of or side 2 }

end2 : integer; { end of or side 2 }

i1 : integer; { loop counter variable }

zerofound : boolean; { true if none found }

begin

count := 0;

start1 := 0;

end1 := 0;

start2 := 0;

end2 := 0;

tmp := false;

zerofound := false;

for i1 := start to enda do

begin

if (expression1.data[i1] = '(') then count := count + 1;

if (expression1.data[i1] = ')') then count := count - 1;

if (expression1.data[i1+1] = '.') and (expression1.data[i1+2] = 'o') and (count <= 1) and not zerofound then

begin

start1 := start;

end1 := i1;

start2 := i1 + 4;

end2 := enda;

tmp := true;

end;

if (expression1.data[i1+1] = '.') and (expression1.data[i1+2] = 'a') and (count = 0) then

begin

start1 := 0;

end1 := 0;

start2 := 0;

end2 := 0;

tmp := false;

zerofound := true;

end;

end;

if (enda - start < 3) then tmp := false;

hasor := tmp;

end;


{---------------------------------------------------------------------}

{ PushNOT - to push a NOT onto a tree }

{---------------------------------------------------------------------}

procedure pushnot(ptr,ptr2,ptr3,entrance : integer);

begin

insertrec2(ptr,ptr2,ptr3,'.not.',entrance);

end;


{---------------------------------------------------------------------}

{ PushAND - to push an AND onto a tree }

{---------------------------------------------------------------------}

procedure pushand(ptr,ptr2,ptr3,entrance : integer);

begin

insertrec2(ptr,ptr2,ptr3,'.and.',entrance);

end;


{---------------------------------------------------------------------}

{ PushOR - to push an OR onto a tree }

{---------------------------------------------------------------------}

procedure pushor(ptr,ptr2,ptr3,entrance : integer);

begin

insertrec2(ptr,ptr2,ptr3,'.or.',entrance);

end;


{---------------------------------------------------------------------}

{ ComputeStartEnd - to find the start and end under AND or OR }

{---------------------------------------------------------------------}

procedure computestartend(expression1 : texttype; var start,enda,start1,end1,start2,end2 : integer);

var

i1 : integer; { loop counter variable }

count : integer; { counter variable }

begin

count := 0;

start1 := 0;

end1 := 0;

start2 := 0;

end2 := 0;

for i1 := start to enda do

begin

if (expression1.data[i1] = '(') then count := count + 1;

if (expression1.data[i1] = ')') then count := count - 1;

if (expression1.data[i1] = ')') and (expression1.data[i1+1] = '.') and (expression1.data[i1+2] = 'a') and (count = 0) then

begin

start1 := start;

end1 := i1;

start2 := i1 + 6;

end2 := enda;

end;

end;

if (start1 = 0) then

begin

count := 0;

for i1 := start to enda do

begin

if (expression1.data[i1] = '(') then count := count + 1;

if (expression1.data[i1] = ')') then count := count - 1;

if (expression1.data[i1] = '.') and (expression1.data[i1+1] = 'a') and (count = 0) then

begin

start1 := start;

end1 := i1 - 1;

start2 := i1 + 5;

end2 := enda;

end;

end;

end;

end;


{---------------------------------------------------------------------}

{ ComputeStartEnd - to compute the start/end under AND or OR }

{---------------------------------------------------------------------}

procedure computestartend2(expression1 : texttype; var start,enda,start1,end1,start2,end2 : integer);

var

i1 : integer; { loop counter variable }

count : integer; { counter variable }

begin

count := 0;

start1 := 0;

end1 := 0;

start2 := 0;

end2 := 0;

for i1 := start to enda do

begin

if (expression1.data[i1] = '(') then count := count + 1;

if (expression1.data[i1] = ')') then count := count - 1;

if (expression1.data[i1] = ')') and (expression1.data[i1+1] = '.') and (expression1.data[i1+2] = 'o') and (count = 0) then

begin

start1 := start;

end1 := i1;

start2 := i1 + 5;

end2 := enda;

end;

end;

if (start1 = 0) then

begin

count := 0;

for i1 := start to enda do

begin

if (expression1.data[i1] = '(') then count := count + 1;

if (expression1.data[i1] = ')') then count := count - 1;

if (expression1.data[i1] = '.') and (expression1.data[i1+1] = 'o') and (count = 0) then

begin

start1 := start;

end1 := i1 - 1;

start2 := i1 + 4;

end2 := enda;

end;

end;

end;

end;


{---------------------------------------------------------------------}

{ HasLiteral - returns true if literal expression }

{---------------------------------------------------------------------}

function hasliteral(var expression1 : texttype; start1,enda : integer) : boolean;

var

tmp : boolean; { temporary boolean flag variable }

posstr1 : integer; { position of string #1 }

posstr2 : integer; { position of string #2 }

posstr3 : integer; { position of string #3 }

begin

tmp := false;

findstring('(',expression1,start1,enda,posstr1);

findstring(')',expression1,start1,enda,posstr2);

findstring('.',expression1,start1,enda,posstr3);

if (posstr1 = 0) and (posstr2 = 0) and (posstr3 = 0) then tmp := true;

hasliteral := tmp;

end;


{---------------------------------------------------------------------}

{ GetLiteral - returns the literal }

{---------------------------------------------------------------------}

procedure getliteral(var expression1 : texttype; start,enda : integer; var lit1 : string);

var

i1 : integer; { loop counter variable }

begin

lit1 := '';

for i1 := start to enda do

lit1 := lit1 + expression1.data[i1];

end;


{---------------------------------------------------------------------}

{ PushLiteral - to push a literal onto a tree }

{---------------------------------------------------------------------}

procedure pushliteral(dbptr,dbptr1,dbptr2 : integer; var lit1 : string; entrance : integer);

begin

dbptr1 := 0;

dbptr2 := 0;

insertrec3(dbptr,dbptr1,dbptr2,lit1,entrance);

end;


{---------------------------------------------------------------------}

{ Illegal - returns True if Expression is Illegal }

{---------------------------------------------------------------------}

function illegal(var expression1 : texttype; start,enda : integer) : boolean;

var

tmp : boolean; { temporary boolean flag variable }

tmp2 : boolean; { temporary boolean flag variable #2 }

tmp3 : boolean; { temporary boolean flag variable #3 }

tmp4 : boolean; { temporary boolean flag variable #4 }

i1 : integer; { loop counter variable }

posstr1 : integer; { position of string #1 }

posstr2 : integer; { position of string #2 }

count : integer; { counter variable }

begin

tmp := false;

findstring('.and.',expression1,start,enda,posstr1);

findstring('.and.',expression1,posstr1+1,enda,posstr2);

tmp2 := true;

for i1 := (posstr1 + 5) to (posstr2 - 1) do

begin

if (expression1.data[i1] = '(') or (expression1.data[i1] = ')') then tmp2 := false;

end;

if (posstr1 = 0) then tmp2 := false;

if (posstr2 = 0) then tmp2 := false;

findstring('.or.',expression1,start,enda,posstr1);

findstring('.or.',expression1,posstr1+1,enda,posstr2);

tmp3 := true;

for i1 := (posstr1 + 4) to (posstr2 - 1) do

begin

if (expression1.data[i1] = '(') or (expression1.data[i1] = ')') then tmp3 := false;

end;

if (posstr1 = 0) then tmp3 := false;

if (posstr2 = 0) then tmp3 := false;

tmp4 := false;

count := 0;

for i1 := start to enda do

begin

if (expression1.data[i1] = '(') then count := count + 1;

if (expression1.data[i1] = ')') then count := count - 1;

end;

if (count <> 0) then tmp4 := true;

tmp := tmp2 or tmp3 or tmp4;

illegal := tmp;

end;


{---------------------------------------------------------------------}

{ DumpExpression1 - to display the value of expression1 for debugging }

{---------------------------------------------------------------------}

procedure dumpexpression1(var expression1 : texttype; start,enda : integer);

var

i1 : integer; { loop counter variable }

begin

for i1 := start to enda do

write(expression1.data[i1]);

writeln;

end;


{---------------------------------------------------------------------}

{ ParseExpression1 - to parse an expression into a tree (recursive) }

{---------------------------------------------------------------------}

procedure parseexpression1(var expression1 : texttype; start,enda,dbptr,entrance : integer);

var

dbptr1 : integer; { data file pointer #1 }

dbptr2 : integer; { data file pointer #2 }

start1 : integer; { start of side 1 }

end1 : integer; { end of side 1 }

start2 : integer; { start of side 2 }

end2 : integer; { end of side 2 }

lit1 : string; { literal expression value }

entranceq : integer; { flip of '.not.' expression }

begin



if (enda >= start) and not illegal(expression1,start,enda) then

begin

{---------------------------------------------------------------------}

if debugp1 then writeln('Debug: start = ',start,' enda = ',enda);

if debugp1 then dumpexpression1(expression1,start,enda);

{---------------------------------------------------------------------}





if hasparenthesis(expression1,start,enda) then

begin


{---------------------------------------------------------------------}

if debugp1 then writeln('has parenthesis');

{---------------------------------------------------------------------}


start := start + 1;

enda := enda - 1;

parseexpression1(expression1,start,enda,dbptr,entrance)

end

else

begin

if hasnot(expression1,start,enda) then

begin


{---------------------------------------------------------------------}

if debugp1 then writeln('has not');

{---------------------------------------------------------------------}


start := start + 5;

makeempty(dbptr1);

dbptr2 := 0;

entranceq := flip(entrance);

pushnot(dbptr,dbptr1,dbptr2,entranceq);

parseexpression1(expression1,start,enda,dbptr1,entranceq)

end

else

begin

if hasand(expression1,start,enda) then

begin


{---------------------------------------------------------------------}

if debugp1 then writeln('has and');

{---------------------------------------------------------------------}


computestartend(expression1,start,enda,start1,end1,start2,end2);

makeempty(dbptr1);

makeempty(dbptr2);

pushand(dbptr,dbptr1,dbptr2,entrance);

parseexpression1(expression1,start1,end1,dbptr1,entrance);

parseexpression1(expression1,start2,end2,dbptr2,entrance);

end

else

begin

if hasor(expression1,start,enda) then

begin


{---------------------------------------------------------------------}

if debugp1 then writeln('has or');

{---------------------------------------------------------------------}


computestartend2(expression1,start,enda,start1,end1,start2,end2);

makeempty(dbptr1);

makeempty(dbptr2);

pushor(dbptr,dbptr1,dbptr2,entrance);

parseexpression1(expression1,start1,end1,dbptr1,entrance);

parseexpression1(expression1,start2,end2,dbptr2,entrance);

end

else

begin

if hasliteral(expression1,start,enda) then

begin


{---------------------------------------------------------------------}

if debugp1 then writeln('has literal');

{---------------------------------------------------------------------}


getliteral(expression1,start,enda,lit1);

dbptr1 := 0;

dbptr2 := 0;


{---------------------------------------------------------------------}

if debugp1 then writeln('lit1: ',lit1);

{---------------------------------------------------------------------}


pushliteral(dbptr,dbptr1,dbptr2,lit1,entrance);

end;

end;

end;

end;

end;

end;

end;


{---------------------------------------------------------------------}

{ ParseFile - to parse an expression into a tree }

{---------------------------------------------------------------------}

procedure parsefile(str1 : string; ptr : integer; var illegalcode : integer);

var

start : integer; { start of expression to parse }

enda : integer; { end of expression to parse }

i1 : integer; { loop counter variable }

begin

for i1 := 1 to vmax do vartable1.data[i1] := '';

vartable1.size := 0;


getexpression1(str1,expression1);

start := 1;

enda := expression1.size;


{---------------------------------------------------------------------}

if debugp1 then writeln('Debug: start = ',start,' enda = ',enda);

{---------------------------------------------------------------------}


parseexpression1(expression1,start,enda,ptr,1);

illegalcode := 0;

if (illegal(expression1,start,enda)) then illegalcode := 1;


{---------------------------------------------------------------------}

if debugp1 and (illegalcode = 1) then writeln('Illegal Expression.');

{---------------------------------------------------------------------}


end;


{---------------------------------------------------------------------}

{ Flip - to return the flip of a bit }

{---------------------------------------------------------------------}

function flip(i1 : integer) : integer;

var

tmp : integer; { temporary integer }

begin

if (i1 = 0) then tmp := 1;

if (i1 = 1) then tmp := 0;

flip := tmp;

end;


{---------------------------------------------------------------------}

{ HasChildren - returns true if node has children }

{---------------------------------------------------------------------}

function haschildren(ptr : integer) : boolean;

var

tmp : boolean; { temporary integer }

key1 : integer; { temporary key value integer }

data1 : string; { temporary data value }

left1 : integer; { temporary left pointer }

right1 : integer; { temporary right pointer }

literal1 : integer; { temporary literal flag value }

entrance1 : integer; { temporary entrance value }

exit1 : integer; { temporary exit value }

begin

tmp := false;

getrec1(ptr,key1,data1,left1,right1,literal1,entrance1,exit1);

if (left1 <> 0) or (right1 <> 0) then tmp := true;

haschildren := tmp;

end;


{---------------------------------------------------------------------}

{ CheckVarTable - to return true if variable result checks }

{---------------------------------------------------------------------}

function checkvartable(data1 : string; exit1 : integer) : boolean;

var

tmp : boolean; { boolean flag }

e1 : integer; { result of search }


{---------------------------------------------------------------------}

{ DataInTable - returns true if data1 is in var table }

{---------------------------------------------------------------------}

function dataintable(data1 : string) : boolean;

var

tmp : boolean; { result of search }

i1 : integer; { loop counter variable }

begin

tmp := false;

for i1 := 1 to vartable1.size do

begin

if (vartable1.data[i1] = data1) then tmp := true;

end;

dataintable := tmp;

end;


{---------------------------------------------------------------------}

{ Exit1Data - returns the value of exit1 for var in table }

{---------------------------------------------------------------------}

function exit1data(data1 : string) : integer;

var

tmp : integer; { result of search }

i1 : integer; { loop counter variable }

flag : boolean; { result of search }

begin

tmp := 0;

flag := false;

for i1 := 1 to vartable1.size do

begin

if (vartable1.data[i1] = data1) and not flag then

begin

tmp := vartable1.exit[i1];

flag := true;

end;

end;

exit1data := tmp;

end;


{---------------------------------------------------------------------}

{ InsertData1 - inserts a var and its exit1 value into the table }

{---------------------------------------------------------------------}

procedure insertdata1(data1 : string; exit1 : integer);

var

tmp : boolean; { result of search }

i1 : integer; { loop counter variable }

begin

tmp := false;

for i1 := 1 to vmax do

begin

if not tmp then

begin

if (vartable1.data[i1] = '') then

begin

vartable1.data[i1] := data1;

vartable1.exit[i1] := exit1;

tmp := true;

vartable1.size := vartable1.size + 1;

end;

end;

end;

end;

{---------------------------------------------------------------------}

{---------------------------------------------------------------------}

begin { checkvartable }

if dataintable(data1) then

begin

e1 := exit1data(data1);

tmp := false;

if (e1 <> exit1) then tmp := true;

end;

if not dataintable(data1) then

begin

insertdata1(data1,exit1);

tmp := false;

end;

checkvartable := tmp;

end;


{---------------------------------------------------------------------}

{ LiteralContradiction - returns 1 if there is a contradiction in the }

{ use of the literals }

{---------------------------------------------------------------------}

function literalcontradiction(ptr : integer) : boolean;

var

tmp : boolean;

key1 : integer;

data1 : string;

left1 : integer;

right1 : integer;

literal1 : integer;

entrance1 : integer;

exit1 : integer;

s1 : boolean;

s2 : boolean;

begin

tmp := false;

getrec1(ptr,key1,data1,left1,right1,literal1,entrance1,exit1);

if (literal1 = 1) and (entrance1 <> exit1) then tmp := true;

s1 := false;

s2 := false;

if (left1 <> 0) then

s1 := literalcontradiction(left1);

if (left1 = 0) then

if (literal1 = 1) and (entrance1 <> exit1) then tmp := true;

if (right1 <> 0) then

s2 := literalcontradiction(right1);

if (right1 = 0) then

if (literal1 = 1) and (entrance1 <> exit1) then tmp := true;

if s1 or s2 then tmp := true;

if (literal1 = 1) then

tmp := checkvartable(data1,exit1);

literalcontradiction := tmp;

end;


{---------------------------------------------------------------------}

{ Satisfiable - returns 1 if expression at ptr is satisfiable }

{---------------------------------------------------------------------}

function satisfiable(entrance : integer; ptr : integer) : integer;

var

key1 : integer; { temporary key value }

data1 : string; { temporary data variable value }

left1 : integer; { temporary left pointer value }

right1 : integer; { temporary right pointer value }

literal1 : integer; { temporary literal flag value }

entrance1 : integer; { temporary entrance variable value }

exit1 : integer; { temporary exit variable value }

key2 : integer; { temporary key value #2 }

data2 : string; { temporary data value #2 }

left2 : integer; { temporary left value #2 }

right2 : integer; { temporary right value #2 }

literal2 : integer; { temporary literal value #2 }

entrance2 : integer; { temporary entrance value #2 }

exit2 : integer; { temporary exit value #2 }

key3 : integer; { temporary key value #3 }

data3 : string; { temporary data variable value #3 }

left3 : integer; { temporary left ptr value #3 }

right3 : integer; { temporary right ptr value #3 }

literal3 : integer; { temporary literal value #3 }

entrance3 : integer; { temporary entrance value #3 }

exit3 : integer; { temporary exit value #3 }

key4 : integer; { temporary key value #4 }

data4 : string; { temporary data variable value #4 }

left4 : integer; { temporary left ptr value #4 }

right4 : integer; { temporary right ptr value #4 }

literal4 : integer; { temporary literal flag value #4 }

entrance4 : integer; { temporary entrance variable value #4 }

exit4 : integer; { temporary exit variable value #4 }

s1 : integer; { intermediate result of sat }

s2 :integer; { intermediate result of sat }

result : integer; { result of sat }


begin

getrec1(ptr,key1,data1,left1,right1,literal1,entrance1,exit1);


{---------------------------------------------------------------------}

if debugs1 then writeln('data1: ',data1,' left1: ',left1,' right1: ',right1,' entrance1: ',entrance1,' exit1: ',exit1,' entrance: ',entrance,' literal1: ',literal1);

{---------------------------------------------------------------------}


result := 0;

if (entrance = 0) and haschildren(ptr) then

begin

if (data1 = '.and.') then

begin


{---------------------------------------------------------------------}

if debugs1 then writeln(entrance,': ','.and.');

{---------------------------------------------------------------------}


s1 := satisfiable(1,left1);

s2 := satisfiable(1,right1);

result := 0;

if (s1 = 0) or (s2 = 0) then result := 1;

getrec1(left1,key2,data2,left2,right2,literal2,entrance2,exit2);

getrec1(right1,key3,data3,left3,right3,literal3,entrance3,exit3);

if debugs1 then writeln('data2: ',data2,' data3: ',data3);

if (data2 = '.not.') and (data3 <> '.not.') then

begin

getrec1(left1,key4,data4,left4,right4,literal4,entrance4,exit4);


{---------------------------------------------------------------------}

if debugs1 then writeln('data4: ',data4,' left4: ',left4,' left3: ',left3);

if debugs1 then writeln('left1: ',left1,' right1: ',right1);

{---------------------------------------------------------------------}


s1 := cequivalence(left4,right1);


{---------------------------------------------------------------------}

if debugs1 then writeln('l4 r1');

if debugs1 then listtree(left4);

if debugs1 then listtree(right1);

{---------------------------------------------------------------------}


if (left4 = 0) and (left1 = 0) then

begin

s1 := 1;

if (data1 = data4) then s1 := 0;

end;

result := flip(s1);

end;

if (data2 <> '.not.') and (data3 = '.not.') then

begin

getrec1(right1,key4,data4,left4,right4,literal4,entrance4,exit4);


{---------------------------------------------------------------------}

if debugs1 then writeln('data4: ',data4,' left4: ',left4,' left2: ',left2);

if debugs1 then writeln('left1: ',left1,' right1: ',right1);

{---------------------------------------------------------------------}


s1 := cequivalence(left4,left1);


{---------------------------------------------------------------------}

if debugs1 then writeln('l4 l1');

if debugs1 then listtree(left4);

if debugs1 then listtree(left1);

{---------------------------------------------------------------------}


if (left4 = 0) and (left1 = 0) then

begin

s1 := 1;

if (data1 = data4) then s1 := 0;

end;

result := flip(s1);

end;

end;

if (data1 = '.or.') then

begin


{---------------------------------------------------------------------}

if debugs1 then writeln(entrance,': ','.or.');

{---------------------------------------------------------------------}


s1 := satisfiable(1,left1);

s2 := satisfiable(1,right1);

result := 1;

if (s1 = 1) or (s2 = 1) then result := 0;

end;

if (data1 = '.not.') then

begin


{---------------------------------------------------------------------}

if debugs1 then writeln(entrance,': ','.not.');

{---------------------------------------------------------------------}


s1 := satisfiable(1,left1);

if (s1 = 0) then result := 1;

if (s1 = 1) then result := 1;

end;

end;

if (literal1 = 1) then

begin


{---------------------------------------------------------------------}

if debugs1 then writeln(entrance,': ','.literal.');

{---------------------------------------------------------------------}


result := 0;

end;

if (entrance = 1) and haschildren(ptr) then

begin

if (data1 = '.and.') then

begin


{---------------------------------------------------------------------}

if debugs1 then writeln(entrance,': ','.and.');

{---------------------------------------------------------------------}


s1 := satisfiable(1,left1);

s2 := satisfiable(1,right1);


{---------------------------------------------------------------------}

if debugs1 then writeln('s1 = ',s1,' s2 = ',s2);

{---------------------------------------------------------------------}


result := 1;

if (s1 = 0) or (s2 = 0) then result := 0;

getrec1(left1,key2,data2,left2,right2,literal2,entrance2,exit2);

getrec1(right1,key3,data3,left3,right3,literal3,entrance3,exit3);


{---------------------------------------------------------------------}

if debugs1 then writeln('data2: ',data2,' data3: ',data3);

{---------------------------------------------------------------------}


data4 := '';

if (data2 = '.not.') and (data3 <> '.not.') then

begin

getrec1(left1,key4,data4,left4,right4,literal4,entrance4,exit4);


{---------------------------------------------------------------------}

if debugs1 then writeln('data4: ',data4,' left4: ',left4,' left3: ',left3);

if debugs1 then writeln('left1: ',left1,' right1: ',right1);

if debugs1 then writeln('l4 r1');

{---------------------------------------------------------------------}


s1 := cequivalence(left4,right1);


{---------------------------------------------------------------------}

if debugs1 then listtree(left4);

if debugs1 then listtree(right1);

{---------------------------------------------------------------------}


if (left4 = 0) and (right1 = 0) then

begin

s1 := 0;

if (data1 = data4) then s1 := 1;

end;

result := flip(s1);

end;

if (data2 <> '.not.') and (data3 = '.not.') then

begin

getrec1(right1,key4,data4,left4,right4,literal4,entrance4,exit4);


{---------------------------------------------------------------------}

if debugs1 then writeln('data4: ',data4,' left4: ',left4,' left2: ',left2);

if debugs1 then writeln('left1: ',left1,' right1: ',right1);

if debugs1 then writeln('l4 l1');

{---------------------------------------------------------------------}


s1 := cequivalence(left4,left1);


{---------------------------------------------------------------------}

if debugs1 then listtree(left4);

if debugs1 then listtree(left1);

{---------------------------------------------------------------------}


if (left4 = 0) and (left1 = 0) then

begin

s1 := 0;

if (data1 = data4) then s1 := 1;

end;

result := flip(s1);

end;

end;

if (data1 = '.or.') then

begin


{---------------------------------------------------------------------}

if debugs1 then writeln(entrance,': ','.or.');

{---------------------------------------------------------------------}


s1 := satisfiable(1,left1);

s2 := satisfiable(1,right1);

result := 0;

if (s1 = 1) and (s2 = 1) then result := 1;

end;

if (data1 = '.not.') then

begin


{---------------------------------------------------------------------}

if debugs1 then writeln(entrance,': ','.not.');

{---------------------------------------------------------------------}


s1 := satisfiable(1,left1);

if (s1 = 0) then result := 1;

if (s1 = 1) then result := 1;

end;

end;

if (literal1 = 1) then

begin


{---------------------------------------------------------------------}

if debugs1 then writeln(entrance,': ','.literal.');

{---------------------------------------------------------------------}


result := 1;

end;


{---------------------------------------------------------------------}

if debugs1 then writeln('sat?: ',result);

{---------------------------------------------------------------------}


satisfiable := result;

end;


{---------------------------------------------------------------------}

{ Satisfiability - to test the satisfiability of an expression }

{---------------------------------------------------------------------}

procedure satisfiability(ptr : integer);

var

result1 : integer; { temporary result value of sat }

begin

result1 := satisfiable(1,ptr);

if literalcontradiction(ptr) then result1 := 0;

if (result1 = 0) then writeln('Expression is NOT Satisfiable.');

if (result1 = 1) then writeln('Expression IS Satisfiable.');

end;


{---------------------------------------------------------------------}

{ P1batch - to perform a batch run on a list of expressions }

{---------------------------------------------------------------------}

procedure p1batch(str2 : string);

begin

assign(ffid,str2);

reset(ffid);

while not eof(ffid) do

begin

readln(ffid,str3);

initfile;

getfree1(ptr);

getfree2(ptr,tptr);

add2treelist(tptr,ptr);

parsefile(str3,ptr,illegalcode);

if (illegalcode = 0) then satisfiability(ptr) else writeln('Illegal Expression.');

end;

close(ffid);

end;


{--------------------------------------------------------------------}

{ Cnf2text - to convert a cnf form expression to text expression }

{--------------------------------------------------------------------}

procedure cnf2text(str2 : string; var str2a : string);

const

max1 = 1000; { maximum size of cnf expression }

nv = 100; { maximum number of variables in cnf ex }

type

strarraytype = array[1..(nv+1)] of string; { type for cnf exp }

var

cfid : text; { file id of cnf exp }

cofid : text; { output file id of cnf exp }

line1 : string; { line of text }

strarray1 : strarraytype; { string table }

ch : char; { char variable }

prop1 : array[1..max1,1..(nv+1)] of integer; { boolean propos. }

j1 : integer; { intermediate integer }

j2 : integer; { intermediate integer }

j3 : integer; { intermediate integer }

j4 : integer; { intermediate integer }

nvar : integer; { number of variables }

nclauses : integer; { number of clauses }

i1 : integer; { loop counter variable }

i2 : integer; { loop counter variable }

start : boolean; { start of exp }

start2 : boolean; { start of exp #2 }

fname : string; { file name }

ofname : string; { output file name }


{--------------------------------------------------------------------}

{ Str2Int - to convert a string to an integer }

{--------------------------------------------------------------------}

function str2int(str1 : string) : integer;

var

tmp : integer; { temporary boolean flag variable }

i1 : integer; { loop counter variable }

neg : integer; { flag for negative values }

begin

tmp := 0;

neg := 1;

for i1 := 1 to length(str1) do

begin

if (str1[i1] <> '-') then

tmp := tmp*10 + ord(str1[i1]) - ord('0');

if (str1[i1] = '-') then

neg := -1;

end;

str2int := tmp*neg;

end;


{--------------------------------------------------------------------}

{ Parse1 - to run the parsing of a cnf expression }

{--------------------------------------------------------------------}

procedure parse1(line1 : string; var strarray : strarraytype);

var

i1 : integer; { loop counter variable }

i2 : integer; { loop counter variable }

begin

for i1 := 1 to (nv+1) do strarray[i1] := '';

i2 := 1;

for i1 := 1 to length(line1) do

begin

if (line1[i1] <> ' ') and (i2 <= (nv+1)) then

strarray[i2] := strarray[i2] + line1[i1];

if (line1[i1] = ' ') then

begin

i2 := i2 + 1;

end;

end;

end;


{--------------------------------------------------------------------}

begin { cnf2text }

parse1(str2,strarray1);

fname := strarray1[1];

ofname := strarray1[2];

assign(cfid,fname);

reset(cfid);

if (ofname <> '') then

begin

assign(cofid,ofname);

str2a := ofname;

rewrite(cofid);

end

else

begin

assign(cofid,fname+'.txt');

str2a := fname+'.txt';

rewrite(cofid);

end;

for i1 := 1 to max1 do

for i2 := 1 to nv do

prop1[i1,i2] := 0;

i1 := 0;

while not eof(cfid) do

begin

readln(cfid,line1);

ch := line1[1];

if (ch = 'c') then

begin

end;

if (ch = 'p') then

begin

parse1(line1,strarray1);

nvar := str2int(strarray1[3]);

nclauses := str2int(strarray1[4]);

end;

if (ch <> 'c') and (ch <> 'p') then

begin

i1 := i1 + 1;

parse1(line1,strarray1);

for i2 := 1 to nv do

begin

j1 := str2int(strarray1[i2]);

prop1[i1,i2] := j1;

end;

prop1[i1,nv+1] := 0;

end;

end;

close(cfid);

start := true;

start2 := true;

write(cofid,'(');

for i1 := 1 to nclauses do

begin

if not start2 then write(cofid,').and.(');

start2 := false;

start := true;

for i2 := 1 to nv do

begin

if (prop1[i1,i2] <> 0) then

begin

if not start then write(cofid,'.or.');

if (prop1[i1,i2] < 0) then write(cofid,'(.not.');

write(cofid,'x',abs(prop1[i1,i2]));

if (prop1[i1,i2] < 0) then write(cofid,')');

start := false;

end;

end;

end;

write(cofid,')');

close(cofid);

end;


{---------------------------------------------------------------------}

{ Batchcnf2text - to perform batch cnf to text conversions }

{---------------------------------------------------------------------}

procedure batchcnf2text(str2 : string);

begin

assign(ffid,str2);

reset(ffid);

while not eof(ffid) do

begin

readln(ffid,str3);

cnf2text(str3,str2a);

initfile;

getfree1(ptr);

getfree2(ptr,tptr);

add2treelist(tptr,ptr);

parsefile(str2a,ptr,illegalcode);

if (illegalcode = 0) then satisfiability(ptr) else writeln('Illegal Expression.');

end;

close(ffid);

end;


{---------------------------------------------------------------------}

{ Main Line (p1.pas) The Satisfiability Algorithm }

{ }

{ 5 types of runs: }

{ }

{ p1 console CMD [N] [M] }

{ - to access the inner routines (to check) }

{ p1 batch FILENAME }

{ - to execute a batch run of the satisfiability algorithm }

{ p1 cnf2text FILENAME [OUTFILENAME] }

{ - to convert a cnf expression to the form used here }

{ p1 batchcnf2text FILENAME }

{ - to batch convert cnf expressions to the form used }

{ here }

{ p1 FILENAME }

{ - to run an instance of the satisfiability algorithm }

{---------------------------------------------------------------------}

begin

str1 := paramstr(1);

str2 := paramstr(2);

str3 := paramstr(3);

str4 := paramstr(4);

if (str1 = 'console') then

begin

p1console(str1,str2,str3,str4);

end;

if (str1 = 'batch') then

begin

p1batch(str2);

end;

if (str1 = 'cnf2text') then

begin

cnf2text(str2,str2a);

end;

if (str1 = 'batchcnf2text') then

begin

batchcnf2text(str2);

end;

if (str1 <> 'console') and (str1 <> 'batch') and (str1 <> 'cnf2text') and (str1 <> 'batchcnf2text') then

begin

getfree1(ptr);

getfree2(ptr,tptr);

add2treelist(tptr,ptr);

rootptr := ptr;

parsefile(str1,ptr,illegalcode);

if (illegalcode = 0) then satisfiability(ptr) else writeln('Illegal Expression.');

end;

end.