CNF SAT

CNF Simplification

    A. First-Second Edition

This little problem is part of project of comp472 and it is a group assignment. However, I find it difficult to read my own
¡¡
code of Scheme and more difficult to read others. So, I decide to write it all by myself. Actually we started to assign
¡¡
different parts as different functions to be written by each member of group. However, the deadline is approaching and we
¡¡
still have some different idea of design. Therefore I write my own complete version to bid with Alex. Finally we decide to
¡¡
use my version. And before that there is another version which doesn't apply heuristic function which simply counts the
¡¡
occurrence of each variable and sort that counting list by absolute value so that searching will be proceeded by that
¡¡
order. This project takes me for nearly one week during which I seldom eat or sleep and it even reminds those exciting days
¡¡
for comp442 compiler design!

    B.The problem

You are given a input of CNF and you are supposed to prove if it is satisfiable. If yes, give one truth assignment for each

variable. If not, just output false.

C.The idea of program
¡¡

    The program need to be both sound and completeness, of course deterministic. Sound means for each output truth assignment for

    variable in case of satisfiable, it must be correct. i.e. The truth assignment really make the CNF to be true. Completeness

    means that if the CNF is possible to be satisfied and the program must be able to find the truth assignment. Deterministic

    means the program can terminate and output a result.

1. Approach Algorithm:

1.1 The simplification procedure:

The approach of our program is straightforward. We heavily rely on a list simplification procedure which linearly scans the list and spots single-variable-terms (SVT). The SVT is then used as parameter to simplify the list with the following simple rules:

a) If any clause contains the chosen, then the whole clause can be removed.

b) If the clause contains the negation of the chosen term, then that element can be removed.

The simplification procedure calls itself recursively as a new SVT might be created during execution. The procedure stops in the following situations:

a) No more SVT can be found.

b) A SVT simplification creates a contradiction with its negated form, i.e. using A to simplify and find !A as a SVT.

1.2 The backtrack procedure

The backtrack procedure is rather standard, except we need only pass the variable assignment list. When backtracking, the function first resets a global truth table which is passed by its parent. We use a global truth table for the purpose of simplification. This helps us discover truth assignments for other variables. Thus, helping the backtracking procedure to quickly reach either solution or contradiction. We have also implemented a heuristic function which helps us in evaluating which value to choose next, and with what assignment.

2. Implementation

2.1 The heuristic function

At the beginning of execution, the program linearly scans the input string and creates a variable list which is then used as a guide for choosing next variable. However, we also count the occurrence of each variable in input and record every occurrence of a variable as ¡°+1¡± and its negate form as ¡°-1¡±. Finally we sort this variable occurrence list by its absolute value because we believe that the bigger the difference of occurrence of a variable and its negate form, the better chance we can successfully guess its truth value. If variable A occurs 1000 times and !A occurs 100 times, then the occurrence difference is 1000-100=900. Then there is a good chance A is true.

¡¡

2.2 The simplification before backtracking

The program runs the simplification procedure before any backtracking. This is significant because many simple CNF problems can be solved without using any backtracking. This can also greatly reduces the size of input. The backtracking procedure is originally called with this simplified input.

2.3 Program termination

The program returns the truth table when all variables have been assigned with a truth value except in the case of a contradiction. This occurs when there is a contradiction with the first variable assigned.

2.4 Soundness of the program

All possible satisfiable output is based on truth assignments for each variable. The simplification procedure preceding backtracking will not change the solution since it only extracts information from the input. The succeeding simplification procedures will not change the satisfiability SAT because the program backtracks on an unsound choice.

2.5 Completeness of the program

We can describe the execution as a tree. The program prunes only the clauses that are definitely unsatisfiable with our current truth assignments. Since we run a complete depth-first-search on the pruned tree, we know that we are not missing anything that is solvable.

2.6 The determinism of program

Similar as what mentioned in above, the program will try all possible truth assignments for each variable until no choice can be made. Since the total number of choice is limited with the number of variables, our program will terminate.

2.7 The efficiency of the program

a) The program reduces the input expression to the simplest possible form before initiating any search procedures. This speeds up execution.

b) By applying a simplification procedure after each backtrack call, there is a good chance that some more SVT will be discovered or a contradiction is reached and this in fact saves us a lot of backtrack calls since the truth value of these SVT variables are already discovered.

c) We used a simple and effective heuristic function that counts the number of occurrences of each variable. This information is retrieved at very beginning when variable list is established and this occurrence count table is just a side product of it. Later our search sequence is based on this table, and the first truth value trial is also based on the information in this table. This heuristic is quite cheap and effective because our observation of many of satisfiable result proves this heuristic.

3. Testing

3.1 Testing issues

In order to check our results, we designed a small procedure that checks whether the given output is a correct output. This helped us to save time and work during the testing phase. Another difficulty was to find adequate test cases in order to fully test our program. We found these test cases at the following website http://www.is.titech.ac.jp/~watanebe/gensat/a1/index.html#sample

Therefore, we needed to write a little CNF translating tool in C++ to translate these testing cases.

¡¡

The test cases used have been attached to the project submission. The execution times of the test cases with respect to their ¡°variable number¡± and ¡°number of clauses¡± is as follows:

Test Name | Number of Variables | Number of Clauses | Execution Time (ms)
sat_big_01_input.txt | 50 | 1000 | 844
sat_big_02_input.txt | 50 | 5000 | 27702
sat_big_03_input.txt | 60 | 5000 | 24603
sat_big_04_input.txt | 70 | 5000 | 32447
sat_big_05_input.txt | 80 | 1000 | 21764
sat_big_06_input.txt | 80 | 2000 | 5488
sat_big_07_input.txt | 90 | 1000 | 7814
sat_big_08_input.txt | 50 | 3000 | 5817
sat_big_09_input.txt | 75 | 2500 | 19230
sat_big_10_input.txt | 50 | 250 | 120246
unsat_big_01_input.txt | 50 | 1000 | 11999
unsat_big_02_input.txt | 50 | 5000 | 52698
unsat_big_03_input.txt | 60 | 5000 | 54356
unsat_big_04_input.txt | 70 | 5000 | 67075
unsat_big_05_input.txt | 80 | 1000 | 69426
unsat_big_06_input.txt | 80 | 2000 | 40924
unsat_big_07_input.txt | 90 | 1000 | 126482
unsat_big_08_input.txt | 50 | 3000 | 21349
unsat_big_09_input.txt | 75 | 2500 | 69951
unsat_big_10_input.txt | 50 | 250 | 111611

¡¡

4. Avenues left untried

4.1 Two Algorithms

Two different algorithms were designed for this problem. We noticed that the first approach gave better results when the given input had a small number of variables, but a large number of clauses. On the other hand, the second approach gave better results when the input had a small number of clauses and a large number of variables. Therefore, in order to increase the efficiency, we could have merged these two procedures so that the choice (based on the number of clauses and variables input) of the algorithm to apply is made at the beginning.

Because of time constraints, the program that would run faster on large variable sets was never completed. It had a few interesting ideas and hooks for easily implementable heuristics. Unfortunately, we did not have the time to implement these heuristics, and without them, the program was slower for almost all cases.

The idea behind the unfinished program is to go clause-by-clause and force that clause to be satisfiable. By doing so, we can update a variable-truth list and backtrack as soon as we find an unsatisfiable clause.

This will allow multiple backtrackings in a row. Unfortunately, when uneducated, this algorithm is exponential on the number of clauses which is usually higher than then number of variables.

There were two heuristics that we wanted to implement.

a) When given a single clause which had multiple variables to choose from, we wanted to use the variable that was most present. This would decrease the level of branching.

b) When choosing the next clause to make true, we were to implement a sliding window which would choose the clause with the fewest number of unset variables. By doing so, we both decrease the branching factor as well as assure that we find a clause that is already unsatisfiable very quickly.

The code for the unfinished program is included in this document as it shows a different way of dealing with the SAT problem. It does run, and although less tested, seems to fulfill the requirements on Satisfiability, Completeness and Termination.

4.2 Other Ideas

a) We gave up on sorting the input because the cost was too high for nominal gains.

b) Originally we planned to use some small functions to quickly solve some particular patterns of SAT problem. For example, a CNF with an exponential number of non-repeated clauses is definitely unsatisfiable. Another example is for the clauses (A B)(!A B) ¨¨ B. And also (A B)(!A !B) ¨¨ A can be replaced by B. Although we implemented some of these functions, we did not have time to assemble and test these quick detection functions.

c) Similarly code was completed that made searching the variable list constant. The indexing code is included as ¡°QUICKLIST.scm¡± the code is finished, but the time required to integrate the code was too high.

d) We also considered some fancy algorithms even though most of them were not correct or feasible to implement. Here are some of them:

i) We want to discover the canonical cover of each clause by discovering the common subset of each two clause. Here what canonical cover means that each clause is purely independent and has no correlative relation with other clauses. For example, we have (A B)(B C). Then, B is a subset (the set of common variables to both clauses) of these two clauses (B can be itself a set of variables). B can be either True or False. If B is True, we don¡¯t need to care about the truth values of A and C. If B is False, then both A and C have to be True. Therefore, finding the common variables of two clauses, allows us to make the best choice in choosing the next variable to try. This approach removes some significant number of backtracking steps. However, the implementation cost is very high.

¡¡

ii) We also planned to sort before each backtracking step. The list is sorted by clause length and by the alphabetical order of variables. The variable to try is chosen from the shortest clause, speeding up the simplification procedure. Therefore, sorting the list by length would have made the choice of the variable easier. On the other hand, sorting by alphabetical order eases the process of finding a common subset of two consecutive clauses. However, sorting before each backtracking step highly increases the time complexity.

d)

    D.The major functions

    To run them, you need only (load "satisfy.scm") at command line of Gambit or other Scheme prgram. then (time (satisfy test)). Of course you

    need to load the test cases first.

    In "source code" there will be files needed to run in "gambit":
    To run:
     (load "satisfy.scm")
    (load "testfile.txt")
    (time (satisfy test))

    Another little answer-checking tools is located in "checker.txt"

    To run:
    (load "satisfy.scm")
    (load "testfile.txt")
    (load "checker.txt")
    (checksatisfy test)

    "test" is the input cnf name.

    In "tools", there is small program to translate test sample into cnf format:
    The web of sample test is here:
    http://www.is.titech.ac.jp/~watanabe/gensat/a1/index.html#sample

    To use the tool, at command line, type: cnftrans.exe filename
    (for those "100 variable, 500 clause test cases, my program just run and run, Can someone run the test to see if my program is good?)

     You can use the little transform tool I posted in "project/testing/testing tool/" to translate the sample txt file in above web to

     cnf format.

    E.Further improvement

    The next step?

    F.File listing

    1. utility.txt

    2. satisfy.scm

    3. mergeterm.txt

    4. probelist.txt

    5. checker.txt

    6. testcases.txt

    7. cnftrans.cpp

    ¡¡

    file name: utility.txt

    ;there is subtle difference between these contradictive predicate
    ;cannot simply negate them
    (define not_symbol
    	(lambda (x)
    		(if (symbol? x)
    			#f
    			(if (is_not x)
    				#f
    				#t
    			)
    		)
    	)
    )

    (define is_negate
    	(lambda (x y)
    		;(begin (pp (list "is_negate x=" x "y=" y))
    		(cond
    			((and(symbol? x)(symbol? y)) #f)
    			((and(list? x)(list? y)) #f)
    			((and(is_not x)(symbol? y))(eq? (cadr x) y))
    			((and(symbol? x)(is_not y))(eq? x (cadr y)))
    			(else #f)
    		)
    		;)
    	)
    )

    (define clauselength
    	(lambda (ls)
    		(if (is_symbol ls)
    			0
    			(- (length ls) 1)
    		)
    	)
    )

    (define is_symbol
    	(lambda (x)
    		(or (symbol? x)(is_not x))
    	)
    )

    (define is_not
    	(lambda (ls)
    		(if (or(symbol? ls)(boolean? ls))
    			#f
    			(eq? (car ls) 'NOT)
    		)
    	)
    )

    (define is_or
    	(lambda (ls)
    		(if (symbol? ls)
    			#f
    			 (eq? (car ls) 'OR)
    		)
    	)
    )

    (define is_and
    	(lambda (ls)
    		(if (symbol? ls)
    			#f
    			(eq? (car ls) 'AND)
    		)
    	)
    )

    ;this is my own limited version of "map"
    (define foreach
    	(lambda (f)
    		(lambda (ls)
    			(if   (null? ls)
    				'()
    				(cons (f (car ls)) ((foreach f) (cdr ls)))
    			)
    		)
    	)
    )

    ;"this is my own limited version of "append"
    (define concat
    	(lambda (ls1 ls2)
    		(if (null? ls1)
    			ls2
    			(cons (car ls1) (concat (cdr ls1) ls2))
    		)
    	)
    )

    (define concatlist
    	(lambda (ls)
    		(if (null? ls)
    			'()
    			(concat (car ls) (concatlist (cdr ls)))
    		)
    	)
    )

    (define term2string
    	(lambda (ls)
    		(if (is_not ls)
    			(symbol->string (cadr ls))
    			(symbol->string ls)
    		)
    	)
    )

    (define termcomp
    	(lambda (ls1 ls2)
    		(if (string=? (term2string ls1)(term2string ls2))
    			(if (and (is_not ls1)(symbol? ls2));  define "not A" < "A"
    				#t
    				#f ;all other cases assume they are not ls1<ls2
    			)
    			(string<? (term2string ls1)(term2string ls2))
    		)
    	)
    )

    (define generic_insert
    	(lambda (f)
    		(lambda (x ls)
    			(if (null? ls)
    				(list x)
    				(if (f x (car ls))
    					(cons x ls)
    					(cons (car ls) ((generic_insert f) x (cdr ls)))
    				)
    			)
    		)
    	)
    )

    ; a general purpose sorting algorithm which is a bubble sort with user defined compare method
    ; as parameter f.
    (define generic_sort
    	(lambda (f)
    		(lambda (ls)
    			(if (null? (cdr ls))
    				ls
    				((generic_insert f) (car ls) ((generic_sort f) (cdr ls)))
    			)
    		)
    	)
    )

    (define generic_insert_unique
    	(lambda (fsmall fequal)
    		(lambda (x ls)
    			;(begin (pp (list "insert x=" x "ls=" ls))
    			(if (null? ls)
    				(list x)
    				(if (fsmall x (car ls))
    					(cons x ls)
    					(if (fequal x (car ls))
    						ls ;find repeat
    						(cons (car ls) ((generic_insert_unique fsmall fequal) x (cdr ls)))
    					)
    				)
    			)
    			;)
    		)
    	)
    )

    (define is_keyword
    	(lambda (x)
    		(or (eq? x 'AND)(eq? x 'OR))
    	)
    )

    ; a general purpose sorting algorithm which is a bubble sort with user defined compare method
    ; as parameter f.
    (define generic_sort_unique
    	(lambda (fsmall fequal)
    		(lambda (ls)
    			;(begin (pp (list "sort ls=" ls))
    			(if (null? ls)
    				'()
    				(if (not_symbol (car ls))
    					((generic_insert_unique fsmall fequal) ((generic_sort_unique fsmall fequal)(car ls))
    						((generic_sort_unique fsmall fequal)(cdr ls)))
    					(if (is_keyword (car ls))
    						(cons (car ls)((generic_sort_unique fsmall fequal)(cdr ls)))
    						((generic_insert_unique fsmall fequal) (car ls)
    							((generic_sort_unique fsmall fequal) (cdr ls)))
    					)
    				)
    			)
    			;)
    		)
    	)
    )

    ¡¡

    file name: satisfy.scm

    ;///////////////////////////////////////////////////////////////////////////////////
    ;This is the main module of satisfy project.
    ;The major function is "satisfy"
    ;To use it, just (load "satisfy.scm") and run (satisfy test)
    ;The satisfy function will assume a well-formated CNF input with maximum two
    ;repetition of same redundant variable in same clause.
    ;Satisfy call a "backtrack" which will implement the backtrack algorithm
    ;
    ;
    ;

    (load "mergeterm.txt")
    (load "probelist.txt")

    (define getnextvar
    	(lambda (varlist)
    		(if (null? varlist)
    			'()
    			(if (eq? 'N (cdr (car varlist)))
    				(car (car varlist))
    				(getnextvar (cdr varlist))
    			)
    		)
    	)
    )

    (define dosimplifylist
    	(lambda (ls current)
    		(if (getsymbol current)
    			(simplifylist ((shrinklistwithsymbol current) ls))
    			(simplifylist ((shrinklistwithsymbol (getnegatefromsymbol current)) ls))
    		)
    	)
    )

    (define dobacktrack
    	(lambda (ls current)
    		(let ((result (dosimplifylist ls current)))
    			(if (boolean? result)
    				result
    				(backtrack result gVarlist)
    			)
    		)
    	)
    )

    ;keep the local context

    (define wrapdobacktrack
    	(lambda (ls varlist current which)
    		(begin
    			(setsymbol current which)
    			(let ((result1 (dobacktrack ls current)))
    				(if (boolean? result1);must be false
    					(begin
    						;(pp (list "backtracking...gVarlist" gVarlist "current=" current))
    						(set! gVarlist varlist)
    						(setsymbol current (not which))
    						(let ((result2 (dobacktrack ls current)))
    							(if (boolean? result2)
    								(begin
    									;(pp(list "backtracking after false current=" current "gVarlist=" gVarlist "gNewlist="gNewlist))

    									#f; unsatisfiable
    								)
    								result2
    							)
    						)
    					)
    					result1
    				)
    			)
    		)
    	)
    )

    (define checkvarboolean
    	(lambda (current)
    		(> (cdr(assq current gVarCountList)) 0)
    	)
    )

    ;
    ;The major function to implement backtrack
    ;the parameter "varlist" give the guide of which variable has been set with
    ;truth value. And it is kept as private for each function framework
    ;
    (define backtrack
    	(lambda (ls varlist)
    		(begin ;(pp (list "backtrack gVarlist="	gVarlist ))
    		(set! gVarlist varlist)
    		(let ((current (getnextvar varlist)))
    			(if (null? current)
    				varlist; find satisfiable
    				(wrapdobacktrack ls varlist current (checkvarboolean current))
    			)
    		))
    	)
    )

    ;The main function which test satisfiable of input string.
    ;
    ;
    (define satisfy
    	(lambda (ls)
    		(set! gVarlist (constructvarlistplus ls))
    		(let ((result (simplifylist ls)))
    			(if (boolean? result)
    				#f
    				(begin
    					;(pp (list "before backtrack, the gVarlist=" gVarlist))
    					(backtrack (cdr ls) gVarlist)
    				)
    			)
    		)
    	)
    )

    file name: mergeterm.txt

    ;/////////////////////////////////////////////////////////////////////
    ;This is the initializing part of project which construct the basic variable
    ;list for program running.
    ;The major function here is: constructvarlistplus, retrieveplus
    ;"retrieveplus" is traversing input list and pickup all variables and remove
    ;both repetition and its negated format of variable name.
    ;The side effect is that it also count the occurrance of each variable. Add
    ;+1 for each variable and -1 for each negated format. And finally store the
    ;sum of the occurrance count and stores it in a global variable gVarCountList
    ;
    ;"constructvarlistplus" initialize variable list(different from occurrance
    ;count list) and sort variable list according to the absolute value of occurrance
    ;of each variable, so that backtracking function will choose variable by this
    ;sequence. And choose truth assignment by referencing the occurrance count value.
    ;If it is positive, it choose true first, otherwise verse versa.
    ;
    ;

    (load "utility.txt")
    (load "testcases.txt")

    ;(define test10001 '(AND M N (NOT A) (OR P Q R) (OR A B)(OR P Q) C F))

    (define gVarCountList '())

    (define varcountcomp
    	(lambda (var1 var2)
    		(> (abs (cdr var1)) (abs (cdr var2)))
    	)
    )

    (define sortvarcountlist
    	(lambda (ls)
    		((generic_sort varcountcomp) ls)
    	)
    )

    (define wrapdoaddtolist
    	(lambda (x ls)
    		(if (is_not x)
    			(doaddtolist (cons (cadr x) -1) ls)
    			(doaddtolist (cons x 1) ls)
    		)
    	)
    )

    (define doaddtolist
    	(lambda (sym ls)
    		(begin ;(pp(list "doaddtolist sym=" sym  "ls=" ls))
    		(if (null? ls)
    			(list sym)
    			(if (equal? (car sym) (car (car ls)))
    				(begin ;(pp(list "doaddtolist (cdr sym)=" (cdr sym) "(cdr(car ls))=" (cdr(car ls))))
    					(cons (cons (car sym)(+ (cdr (car ls))(cdr sym))) (cdr ls))
    				)
    				(begin ;(pp(list "doaddtolist (car ls)=" (car ls) "(cdr ls)=" (cdr ls)))
    					(cons (car ls)(doaddtolist sym (cdr ls)))
    				)
    			)
    		))
    	)
    )

    (define mergetwolistplus
    	(lambda (ls1 ls2)
    		(begin ;(pp(list "mergetwolistplus ls1=" ls1 "ls2=" ls2))
    		(if (null? ls1)
    			ls2
    			(mergetwolistplus (cdr ls1)(doaddtolist (car ls1) ls2))
    		))
    	)
    )

    ;traverse input list collecting variable name and occurrance count.
    ;
    (define retrieveplus
    	(lambda (ls)
    		(begin ;(pp(list "retrieveplus ls=" ls))
    		(if (null? ls)
    			'()
    			(if (not_symbol (car ls))
    				(mergetwolistplus (retrieveplus (car ls)) (retrieveplus (cdr ls)))
    				(if (or (is_and  ls) (is_or  ls))
    					(retrieveplus (cdr ls))
    					(wrapdoaddtolist (car ls) (retrieveplus (cdr ls)))
    				)
    			)
    		))
    	)
    )

    (define symbolcomp
    	(lambda (ls1 ls2)
    		(if (string=? (symbol2string ls1)(symbol2string ls2))
    			(if (and (is_not ls1)(symbol? ls2));  define "not A" < "A"
    				#t
    				#f ;all other cases assume they are not ls1<ls2
    			)
    			(string<? (symbol2string ls1)(symbol2string ls2))
    		)
    	)
    )

    (define getcountvalue
    	(lambda (x)
    		(cdr (assq x gVarCountList))
    	)
    )

    (define choosevarbycount
    	(lambda (satlst)
    		(if (null? (cdr satlst))
    			(car(car satlst))
    			(let ((result (choosevarbycount (cdr satlst))))
    				(if (< (abs (getcountvalue (car (car satlst))))(abs(getcountvalue result)))
    					result
    					(car (car satlst))
    				)
    			)
    		)
    	)
    )

    (define satlst '((A . #t) (B . #t)))

    (define initialpair
    	(lambda (sym)
    		(cons sym 'N)
    	)
    )

    (define initialpairplus
    	(lambda (sym)
    		(cons (car sym) 'N)
    	)
    )

    (define initvarlistplus
    	(lambda (ls)
    		(map initialpairplus ls)
    	)
    )

    ;The function to construct variable list and sorted according to absolute value of occurance
    ;count value. And it also initialize the variable list to "unset" or 'N
    ;
    (define constructvarlistplus
    	(lambda (ls)
    		(let ((result (retrieveplus ls)))
    			(begin
    				(set! result (sortvarcountlist result))
    				(set! gVarCountList result)
    				(initvarlistplus result)
    			)
    		)
    	)
    )

    (define addtolist
    	(lambda (x ls)
    		(if (is_not x)
    			(addtolist (cadr x) ls)
    			;(begin (pp (list "addtolist x=" x "ls=" ls))
    			(if (null? ls)
    				(list  x)
    				(if (or(is_negate x (car ls))(equal? x (car ls)))
    					ls
    					(cons (car ls)(addtolist x (cdr ls)))
    				)
    			)
    		)
    		;)
    	)
    )

    (define symbolsort
    	(lambda (ls)
    		((generic_sort symbolcomp) ls)
    	)
    )

    (define mergetwolist
    	(lambda (ls1 ls2)
    		(if (null? ls1)
    			ls2
    			(mergetwolist (cdr ls1)(addtolist (car ls1) ls2))
    		)
    	)
    )

    ; this function will remove all not or and, only retrieve symbols and put in a list
    (define retrieve
    	(lambda (ls)
    		(if (null? ls)
    			'()
    			(if (not_symbol (car ls))
    				(mergetwolist (retrieve (car ls)) (retrieve (cdr ls)))
    				(if (or (is_and  ls) (is_or  ls))
    					(retrieve (cdr ls))
    					(addtolist (car ls) (retrieve (cdr ls)))
    				)
    			)
    		)
    	)
    )

    (define initvarlist
    	(lambda (ls)
    		(map initialpair ls)
    	)
    )

    (define constructvarlist
    	(lambda (ls)
    		(initvarlist (retrieve ls))
    	)
    )

    file name: probelist.txt

    ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
    ;
    ;
    ;
    ;
    ;
    ;
    ;
    ;
    ;

    (define test101 '((B C D) (A F) (G H) (M) (O A) (WHY IS IT T)(B C) (A)))

    (define test1020 '(AND B   (OR (NOT N) (NOT B) K (NOT B)) (OR O P) (OR (NOT N)  (NOT B)) (OR N G)  (OR G H M) (OR G K)
    	(OR M N A G H) (OR (NOT A) N (NOT B) C D P Q R)))

    (define test1021 '(AND B  (OR (NOT B) c ) ))

    (load "utility.txt")
    (load "testcases.txt")

    (define gVarlist '());global variable

    (define setsymbol
    	(lambda (x value)
    		(set! gVarlist (dosetsymbol x value gVarlist))
    	)
    )

    (define dosetsymbol
    	(lambda (x value varlist)
    		(if (null? varlist)
    			(list (cons x value))
    			(if (equal? x (car(car varlist)))
    				(cons (cons x value) (cdr varlist))
    				(cons (car varlist) (dosetsymbol x value (cdr varlist)))
    			)
    		)
    	)
    )

    (define getsymbol
    	(lambda (x)
    		(cdr (assoc x gVarlist))
    	)
    )

    ;helper function to do linear probing
    (define doprobelist
    	(lambda (f)
    		(lambda (ls1 ls2)
    			;(begin (pp (list "doprobelist ls1=" ls1 "ls2=" ls2))
    			(if (null? ls2)
    				'()
    				(if (null? (car ls2));ignore null
    					((doprobelist f) ls1 (cdr ls2))
    					(if (not(f (car ls2)))
    						((doprobelist f)(append ls1 (list (car ls2))) (cdr ls2))
    						(car ls2)
    					)
    				)
    			)
    			;)
    		)
    	)
    )

    ;This is the linear probing function skeleton
    ;it takes two function as parameter, the first is a test function which takes a list as parameter
    ;the second is an exec function which also takes the returning list from "doprobelist" as first
    ;parameter, retrieve necessary information and exec another list which is its second parameter
    ;the returning of probelist is the processed list

    (define probelist
    	(lambda (ftest fexec)
    		(lambda (ls)
    			;(begin (pp (list "probelist ls=" ls))
    			(if (boolean? ls)
    				ls
    				(let ((result ((doprobelist ftest)'() ls)))
    					(if  (null? result)
    						ls
    						((probelist ftest fexec)((fexec result) ls))
    					)
    				)
    			)
    			;)
    		)
    	)
    )

    (define is_negate
    	(lambda (x y)
    		;(begin (pp (list "is_negate x=" x "y=" y))
    		(cond
    			((and(symbol? x)(symbol? y)) #f)
    			((and(list? x)(list? y)) #f)
    			((and(is_not x)(symbol? y))(eq? (cadr x) y))
    			((and(symbol? x)(is_not y))(eq? x (cadr y)))
    			(else #f)
    		)
    		;)
    	)
    )

    ;(define mytest ((checktermwithsymbol '(NOT A)) '(AND B C A)))
    ;(define mytest1 ((checktermwithsymbol  'A)  '(OR N (NOT B) (NOT A) xC D P Q R)))
    ;(define mytest2 ((removesymbol  '(NOT A))  '(OR N (NOT B) (NOT A) xC D P Q R)))
    ;(define test1030 '(AND

    (define getnegatefromsymbol
    	(lambda (ls)
    		(if (is_not ls)
    			(cadr ls)
    			(list 'NOT ls)
    		)
    	)
    )

    (define clearsymbol
    	(lambda (sym)
    		(if (is_symbol sym)
    			sym
    			(if (is_or sym)
    				(cadr sym)
    				(pp "error")
    			)
    		)
    	)
    )

    ;
    ;process each term and try to detecting if the term contains either the variable itself or
    ;its negated format. In first case, it remove entire term to empty list. In second case,
    ; it only removes the negated format of variable alone.
    (define mychecktermwithsymbol
    	(lambda (sym)
    		(lambda (ls)
    			(begin ;(pp (list "mychecktermwithsymbol sym=" sym ))
    			(let ((sym (clearsymbol sym)))
    				(begin ;(pp(list "mychecktermwithsymbol sym=" sym "ls=" ls))
    				(if (null? ls)
    					'()
    					(if (boolean? ls)
    						(pp "mygod!")
    					(if (is_symbol ls)
    						(if (equal? sym ls)
    							#t
    							(if (is_negate sym ls)
    								(begin ;(pp (list "is_negate sym=" sym))
    									#f
    								)
    								ls
    							)
    						)
    						(if (equal? sym (car ls))
    							#t
    							;;you need wait the result from child
    							(let ((result ((mychecktermwithsymbol sym)(cdr ls))))
    								(if (boolean? result)
    									result ;;means you find the same
    									(if (is_negate sym (car ls))
    										result ;;you remove the negate
    										(cons (car ls) result)
    									)
    								)
    							)
    						)
    					))
    				))
    			))
    		)
    	)
    )

    (define checkandsetsymbol
    	(lambda (sym)
    		(begin ;(pp (list "checkandsetsymbol sym=" sym))
    		;(if (or(is_and sym)(is_or sym))
    			;(checkandsetsymbol (cdr sym))
    		(if (is_not sym)
    			(let ((sym (cadr sym)))
    				(let ((result (getsymbol sym)))
    					(if (eq? 'N result)
    						(begin (setsymbol sym #f)
    							;(pp (list "within checkand setsymbol sym=" sym"gVarlist" gVarlist))
    							;(setcurlist sym)
    							#t
    						)
    						(if result
    							;contradiction
    							#f
    							#t
    						)
    						;else do nothing
    					)
    				)

    			)
    			(let ((result (getsymbol sym)))
    				(if (eq? 'N result)
    					(begin  (setsymbol sym #t)
    						;(setcurlist sym)
    						#t
    					)
    					(if (not result)
    						#f
    						#t
    					);else do nothing
    				)
    			)
    		))
    	)
    )

    (define testbooleanfalse
    	(lambda (term)
    		(and (boolean? term)(not term))
    	)
    )
    (define testbooleantrue
    	(lambda (term)
    		(if (and (boolean? term) term)
    			'()
    			term
    		)
    	)
    )

    (define wrapmysmartconstruct
    	(lambda (term ls)
    		(if (or (testbooleanfalse term)(testbooleanfalse ls))
    			#f
    			(mysmartconstruct (testbooleantrue term)(testbooleantrue ls))
    		)
    	)
    )

    ;reconstruct list by removing both empty list and removing redundent variable. (Only one repetition
    ;is expected) It also helps to reveal those hidden single-variable clause, like (OR A) which is ;hidden single variable term
    ;

    (define mysmartconstruct
    	(lambda (term ls)
    		(if (null? term)
    			ls
    			(if (is_symbol term)
    				(cons term ls)
    				(if (and (= 3 (length term))(equal? (cadr term)(caddr term)))
    					(cons (cadr term) ls)
    					(if (= 2 (length term))
    						(cons (cadr term) ls)
    						(if (= 1 (length term));a single (or)
    							ls
    							(cons term ls)
    						)
    					)
    				)
    			)
    		)
    	)
    )

    (define wrapshrink_catch '())

    (define wrapshrinklistwithsymbol
    	(lambda (sym)
    		(lambda (ls)
    			(begin (set! wrapshrink_catch (list "wrapshrinkwithsymbol sym=" sym "ls=" ls))
    			(if (checkandsetsymbol sym)
    				((shrinklistwithsymbol sym)ls)
    				#f
    			))
    		)
    	)
    )

    (define catch '())

    (define docompare
    	(lambda (x ls)
    		(if (null? ls)
    			(begin
    				(pp (list "difference: " x))
    				'()
    			)
    			(if (equal? x (car ls))
    				'()
    				(docompare x (cdr ls))
    			)
    		)
    	)
    )

    (define diff
    	(lambda (ls1 ls2)
    		(begin
    			(compare ls1 ls2)
    			(compare ls2 ls1)
    		)
    	)
    )

    (define compare
    	(lambda (ls1 ls2)
    		(if (null? ls1)
    			'()
    			(begin
    				(docompare (car ls1) ls2)
    				(compare (cdr ls1) ls2)
    			)
    		)
    	)
    )

    (define shrink_catch '())
    (define shrinklistwithsymbol
    	(lambda (sym)
    		(lambda (ls)
    			(begin ;(set! shrink_catch (list "shrinklistwithsymbol sym=" sym "ls=" ls))
    				;(set! catch (list "shrinklistwithsymbol sym=" sym))
    			(if (null? ls)
    				'()
    				(if (boolean? ls)
    					ls
    					(wrapmysmartconstruct ((mychecktermwithsymbol sym) (car ls))
    						((shrinklistwithsymbol sym)(cdr ls)))
    				)
    			))
    		)
    	)
    )

    (define simplifylist
    	(lambda (ls)
    		((probelist issingleterm wrapshrinklistwithsymbol) ls)
    	)
    )

    (define simplifylistwithoutset
    	(lambda (ls)
    		((probelist issingleterm shrinklistwithsymbol) ls)
    	)
    )

    (define getargument
    	(lambda (x)
    		(if (cdr x)
    			(car x)
    			(getnegatefromsymbol (car x))
    		)
    	)
    )

    ;(define demo (setsymbolandsimplify (cdr test) input))

    (define setsymbolandsimplify
    	(lambda (ls argument)
    		(if (null? argument)
    			(begin ;(pp(list "after set ls=" ls))
    				ls
    			)
    			(let ((result  (simplifylistwithoutset
    						((shrinklistwithsymbol (getargument(car argument))) ls)) ))
    					(setsymbolandsimplify result (cdr argument))
    			)
    		)
    	)
    )

    (define mylist '())
    (define buffer1 '())
    (define buffer2 '())

    (define mycall
    	(lambda (ls)
    		(if (null? ls)
    			mylist
    			(begin
    				(let ((result (demo (car (car ls)))))
    					(if (boolean? result)
    						(pp "oh")
    						(mycall (cdr ls))
    					)
    				)
    			)
    		)
    	)
    )

    (define demo
    	(lambda (x)
    		(begin (pp (list "now simplify x=" x ))
    			;(if (eq? x 'A45)
    				;#t
    				(begin
    					(set! buffer2 buffer1)
    					;(pp " it is done!")
    					(set! buffer1 mylist)
    					(set!  mylist (simplifylistwithoutset ((shrinklistwithsymbol x) buffer2)))
    					;(if (eq? x 'A1)
    						;'()
    				)
    			;)
    			;(pp (list "after simplify mylist is" mylist ))
    		)
    	)
    )

    (define issingleterm
    	(lambda (ls)
    		(if (null? ls)
    			#f
    			(if (symbol? ls)
    				(not (or (eq? ls 'AND)(eq? ls 'OR)))
    				(if (is_not ls)
    					#t
    					(if (and (is_or ls)(= 2 (length ls)))
    						#t
    						(if (and (is_or ls)(= 3 (length ls))(equal? (cadr ls)(caddr ls)))
    							#t
    							#f
    						)
    					)
    				)
    			)
    		)
    	)
    )

    file name: testcases.txt

    (define test1 '(AND (NOT A) B (NOT (OR A B))))
    (define test2 '(AND A B))
    (define test3 '(NOT (AND A (NOT (NOT C)) D (OR E (NOT F)))))
    (define test4 '(NOT (NOT (NOT (NOT C)))))

    (define test5 '(NOT (AND A (OR B C))))
    (define test6 '(NOT (NOT (AND A B))))
    (define test7 '(NOT (AND (NOT B) (OR (NOT A) (NOT B)))))
    (define test8 '(NOT (AND (NOT A) (NOT B))))

    (define test9 '(NOT(NOT A)))
    (define test27 '(AND A B C (OR P Q R) (OR X Y Z))) ;(or (and a b c x y z p) (and a b c x y z q) (and a b c x y z r))
              ;(or (and a b c p x) (and a b c p y) (and a b c p z) (and a b c q x) (and a b c q y) (and a b c q z) (and a b c r x) (and a b c r y) (and a b c r z))
    (define test28 '(AND (OR P Q R) A B C (OR X Y Z))) ;(or (and a b c x y p z) (and a b c x y q z) (and a b c x y r z))
              ;(or (and p a b c x) (and p a b c y) (and p a b c z) (and q a b c x) (and q a b c y) (and q a b c z) (and r a b c x) (and r a b c y) (and r a b c z))
    (define test29 '(AND (OR P Q R) (OR X Y Z) A B C)) ;(or (and a b c x y p z) (and a b c x y q z) (and a b c x y r z))
              ;The previous code does not solve this properly.
    (define test30 '(AND A (OR P Q R) B (OR X Y Z) C)) ;(or (and a b c x y p z) (and a b c x y q z) (and a b c x y r z))
              ;(or (and a p b x c) (and a p b y c) (and a p b z c) (and a q b x c) (and a q b y c) (and a q b z c) (and a r b x c) (and a r b y c) (and a r b z c))

    (define test01 '(AND (OR B (AND C (OR M N) F) D) (OR W(AND P (OR Q
    (AND X Y) X A)))))
    (define test21 '(AND X A (OR B (AND C (OR M N) F) D) (OR W(AND P (OR Q
    (AND X Y))))))
    (define test02 '(AND X (OR Y Z)))
    (define test03 '(AND (OR B C D) A B))
    (define test04 '(AND X Z (OR A B C)))
    (define test08 '(AND (OR A B C) X Z))
    (define test05 '(AND (OR X Y) (OR W Z) ))
    (define test06 '(OR (AND X Y (OR A B)) U))
    (define test07 '(AND (OR X Y N Z) (OR U W M)))
    (define test09 '(AND A D (OR B C)))
    (define test10 '(AND (OR B C) A D))
    (define test11 '(AND D (OR B C) A))
    (define test12 '(AND A D (OR B A)))
    (define test13 '(AND (OR B A) A D))
    (define test14 '(AND D (OR B A) A))
    (define test15 '(OR (AND D A) (AND C B) D))
    (define test16 '(OR D (AND D A) (AND C B)))
    (define test17 '(OR A (NOT D) (AND B A)))
    (define test18 '(OR (AND B A) A D))
    (define test19 '(OR D (AND B A) A))
    (define test20 '(OR (NOT A) B C))
    (define test22 '(OR (AND A D) D (AND C B)))

    (define test102 '(AND B (NOT b)  (OR M (NOT N) K) (OR O P) (OR (NOT N) B) (OR N G) (NOT A) A (OR G H M) (OR G K)
    	(OR M N A G H) (OR (NOT A) N (NOT B) C D P Q R)))

    (define test103 '(AND B (NOT c)  (OR M (NOT N) K) (OR O P) (OR (NOT N) B) (OR z a c b(NOT a))
    	(OR N G) (NOT a) A (OR G H M) (OR G K)
    	(OR M N A G mnH) (OR N  (NOT B) (NOT A) xC D P Q R)))

    (define test104 '(AND A (NOT B)  (OR M (NOT N) K) (OR O P) (OR (NOT N) B) (OR z a c b(NOT a)) (OR N G)
    		(NOT C) A (OR G H M) (OR G K) (OR M N A G mnH) (OR N  (NOT B) (NOT A) xC D P Q R)))

    (define sorttest101

    '(AND

    (OR V5 V6)

    (OR (NOT V5) (NOT V0) (NOT V1) (NOT V2) (NOT V3) (NOT V4) )

    (OR (NOT V5) V0 (NOT V1) (NOT V2) (NOT V3) (NOT V4) )

    (OR (NOT V5) (NOT V0) V1 (NOT V2) (NOT V3) (NOT V4) )

    (OR (NOT V5) V0 V1 (NOT V2) (NOT V3) (NOT V4) )

    (OR (NOT V5) (NOT V0) (NOT V1) V2 (NOT V3) (NOT V4) )

    (OR (NOT V5) V0 (NOT V1) V2 (NOT V3) (NOT V4) )

    (OR (NOT V5) (NOT V0) V1 V2 (NOT V3) (NOT V4) )

    (OR (NOT V5) V0 V1 V2 (NOT V3) (NOT V4) )

    (OR (NOT V5) (NOT V0) (NOT V1) (NOT V2) V3 (NOT V4) )

    (OR (NOT V5) V0 (NOT V1) (NOT V2) V3 (NOT V4) )

    (OR (NOT V5) (NOT V0) V1 (NOT V2) V3 (NOT V4) )

    (OR (NOT V5) V0 V1 (NOT V2) V3 (NOT V4) )

    (OR (NOT V5) (NOT V0) (NOT V1) V2 V3 (NOT V4) )

    (OR (NOT V5) V0 (NOT V1) V2 V3 (NOT V4) )

    (OR (NOT V5) (NOT V0) V1 V2 V3 (NOT V4) )

    (OR (NOT V5) V0 V1 V2 V3 (NOT V4) )

    (OR (NOT V5) (NOT V0) (NOT V1) (NOT V2) (NOT V3) V4 )

    (OR (NOT V5) V0 (NOT V1) (NOT V2) (NOT V3) V4 )

    (OR (NOT V5) (NOT V0) V1 (NOT V2) (NOT V3) V4 )

    (OR (NOT V5) V0 V1 (NOT V2) (NOT V3) V4 )

    (OR (NOT V5) (NOT V0) (NOT V1) V2 (NOT V3) V4 )

    (OR (NOT V5) V0 (NOT V1) V2 (NOT V3) V4 )

    (OR (NOT V5) (NOT V0) V1 V2 (NOT V3) V4 )

    (OR (NOT V5) V0 V1 V2 (NOT V3) V4 )

    (OR (NOT V5) (NOT V0) (NOT V1) (NOT V2) V3 V4 )

    (OR (NOT V5) V0 (NOT V1) (NOT V2) V3 V4 )

    (OR (NOT V5) (NOT V0) V1 (NOT V2) V3 V4 )

    (OR (NOT V5) V0 V1 (NOT V2) V3 V4 )

    (OR (NOT V5) (NOT V0) (NOT V1) V2 V3 V4 )

    (OR (NOT V5) V0 (NOT V1) V2 V3 V4 )

    (OR (NOT V5) (NOT V0) V1 V2 V3 V4 )

    (OR (NOT V5) V0 V1 V2 V3 V4 )))

    file name: checker.txt

    ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
    ;This is the small testing tool which will use the return variable
    ;truth assignment to test the satisfiability of input list
    ;To use it, just (load "checker.txt")
    ;and (checksatisfy test) assuming your funtion is called "satisfy"
    ;
    ;
    ;

    (load "utility.txt")

    (define dogetsymbol
    	(lambda(var varlist)
    		(if (is_not var)
    			(not(cdr (assoc (cadr var) varlist)))
    			;(cdr (assoc (cadr var) varlist));deliberately left for debugging
    			(cdr (assoc var varlist))
    		)
    	)
    )

    (define snapvarlist
    	(lambda (var varlist)
    		(if (is_not var)
    			(assoc (cadr var) varlist)
    			(assoc var varlist)
    		)
    	)
    )

    (define checksymbol
    	(lambda (sym varlist)
    		(dogetsymbol sym varlist)
    	)
    )

    (define checkterm
    	(lambda (term varlist)
    		;(begin (pp (list "checkterm term=" term "varlist=" varlist))
    		(if (null? term)
    			#f
    			(if (or(is_or term)(is_and term))
    			   	(checkterm (cdr term) varlist)
    				(if (is_symbol term)
    					(checksymbol term varlist)
    					(or (checksymbol (car term) varlist)
    						(checkterm (cdr term) varlist))
    				)
    			)
    		);)
    	)
    )

    (define outputerror
    	(lambda (term varlist)
    		;(begin (pp(list "outputerror term=" term "varlist=" varlist))
    		(if (null? term)
    			'()
    			(if (or(is_or term)(is_and term))
    				(outputerror(cdr term) varlist)
    				(if (is_symbol term)
    					(snapvarlist term varlist)
    					(cons (snapvarlist (car term) varlist)
    						(outputerror (cdr term)varlist))
    				)
    			)
    		);)
    	)
    )

    (define stepbystep
    	(lambda (ls varlist)
    		(if (null? ls)
    			(pp "congratulations!")
    			(if (checkterm (car ls) varlist)
    				(stepbystep (cdr ls) varlist)
    				(begin
    					(pp (list "there is an error term "(car ls)))
    					(outputerror (car ls) varlist)
    				)
    			)
    		)
    	)
    )

    (define checker
    	(lambda (ls varlist)
    		(if (not(boolean? varlist))
    			(stepbystep (cdr ls) varlist)
    			(pp (list "so you mean it is unsatisfiable, do you expect me to clarify it? no way!"))

    		)
    	)
    )

    ;a wrapper for using , you should use this
    (define checksatisfy
    	(lambda (ls)
    		(checker ls (satisfy ls))
    	)
    )

    ¡¡

    file name: cnftrans.cpp

    #include <iostream>
    #include <fstream>

    using namespace std;
    const int MaxBuffer=256;

    char buffer[MaxBuffer];
    int array[100];

    ifstream in;
    ofstream out;
    void readTitle();
    void createSolution();
    void readCNF(int clauseNum, int varNumber, int clauseLength);

    int main(int argc, char**argv)
    {
    	int clauseNum, varNumber, clauseLength;
    	if (argc!=2)
    	{
    		cout<<"usage: cnfTrans filename\n";
    		exit(0);
    	}
    	in.open(argv[1]);
    	strcpy(buffer, argv[1]);
    	buffer[strlen(buffer)-4]='\0';
    	strcat(buffer, "_input.txt");
    	out.open(buffer);

    	readTitle();

    	createSolution();
    	in>>varNumber>>clauseNum>>clauseLength;
    	readCNF(varNumber, clauseNum, clauseLength);
    	/*
    	in>>varNumber;
    	in>>count;
    	in>>termcount;
    	out<<"(define test '(AND ";
    	for (int i=0; i<count; i++)
    	{
    		//termcount=0;
    		in>>index;
    		for (int k=0; k<termcount; k++)
    		{
    			in>>array[k];
    		}
    			/*
    		while (index!=0)
    		{
    			array[termcount]=index;
    			in>>index;
    			termcount++;
    		}
    		*/
    	/*
    		if (termcount>1)
    		{
    			out<<" (OR ";
    		}
    		for (int j=0; j<termcount; j++)
    		{
    			if (array[j]>0)
    			{
    				sprintf(buffer, " A%d ", array[j]);
    			}
    			else
    			{
    				sprintf(buffer, " (NOT A%d) ", -array[j]);
    			}
    			out<<buffer;
    		}
    		if (termcount>1)
    		{
    			out<<")";
    		}
    		out<<"\n";
    	}

    	out<<"))";
    	*/

    	return 0;
    }

    void readCNF(int varNumber, int clauseNum, int clauseLength)
    {
    	int index;
    	out<<"(define test '(AND ";
    	for (int i=0; i<clauseNum; i++)
    	{
    		out<<"(OR ";
    		for (int j=0; j<clauseLength; j++)
    		{
    			in>>index;
    			if (index<0)
    			{
    				itoa(-index, buffer, 10);
    				out<<"(NOT A"<<buffer<<")";
    			}
    			else
    			{
    				itoa(index, buffer, 10);
    				out<<" A"<<buffer<<" ";
    			}
    		}
    		out<<")\n";
    	}
    	out<<"))\n";
    }

    void createSolution()
    {
    	int length=strlen(buffer);
    	out<<"(define solution '(\n";
    	for (int i=0; i<length; i++)
    	{
    		out<<"(A"<<(i+1)<<" . #"<<(buffer[i]=='0'?"f":"t")<<")\n";
    	}
    	out<<"))\n";
    }

    void readTitle()
    {
    	in.getline(buffer, MaxBuffer);
    	in>>buffer;
    	in>>buffer;
    	in>>buffer;
    	in>>buffer;
    }

    ¡¡

    ¡¡