CNF SAT

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

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.

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.

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

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.The major functions

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