;; Simple SAT problems for testing

(setf *clauses0* '(a))

(setf *clauses1* '((and a b)))

(setf *clauses2* '((or a b)
		   (or (not a) c)
		   (or (not b) (not c))))


;; Benchmark SAT problems
;;
;; *b20* is Problem # uf20-01 from the SATLIB Uniform Random 3-SAT
;;    Benchmark Problems
;; *b50* is Problem # uf50-218
;;  http://people.cs.ubc.ca/~hoos/SATLIB/benchm.html
;;  (These are the two easiest of those benchmarks)
;;
;; Translated into our Lisp representation by hand/emacs regexp
;; Marie desJardins, CMSC 471 (UMBC), Fall 2009

(defvar *b20*)
(setf *b20*
      '((or  v4 (not v18) v19)
	(or  v3 v18 (not v5))
	(or (not v5) (not v8) (not v15))
	(or (not v20) v7 (not v16))
	(or  v10 (not v13) (not v7))
	(or (not v12) (not v9) v17)
	(or  v17 v19 v5)
	(or (not v16) v9 v15)
	(or  v11 (not v5) (not v14))
	(or  v18 (not v10) v13)
	(or (not v3) v11 v12)
	(or (not v6) (not v17) (not v8))
	(or (not v18) v14 v1)
	(or (not v19) (not v15) v10)
	(or  v12 v18 (not v19))
	(or (not v8) v4 v7)
	(or (not v8) (not v9) v4)
	(or  v7 v17 (not v15))
	(or  v12 (not v7) (not v14))
	(or (not v10) (not v11) v8)
	(or  v2 (not v15) (not v11))
	(or  v9 v6 v1)
	(or (not v11) v20 (not v17))
	(or  v9 (not v15) v13)
	(or  v12 (not v7) (not v17))
	(or (not v18) (not v2) v20)
	(or  v20 v12 v4)
	(or  v19 v11 v14)
	(or (not v16) v18 (not v4))
	(or (not v1) (not v17) (not v19))
	(or (not v13) v15 v10)
	(or (not v12) (not v14) (not v13))
	(or  v12 (not v14) (not v7))
	(or (not v7) v16 v10)
	(or  v6 v10 v7)
	(or  v20 v14 (not v16))
	(or (not v19) v17 v11)
	(or (not v7) v1 (not v20))
	(or (not v5) v12 v15)
	(or (not v4) (not v9) (not v13))
	(or  v12 (not v11) (not v7))
	(or (not v5) v19 (not v8))
	(or  v1 v16 v17)
	(or  v20 (not v14) (not v15))
	(or  v13 (not v4) v10)
	(or  v14 v7 v10)
	(or (not v5) v9 v20)
	(or  v10 v1 (not v19))
	(or (not v16) (not v15) (not v1))
	(or  v16 v3 (not v11))
	(or (not v15) (not v10) v4)
	(or  v4 (not v15) (not v3))
	(or (not v10) (not v16) v11)
	(or (not v8) v12 (not v5))
	(or  v14 (not v6) v12)
	(or  v1 v6 v11)
	(or (not v13) (not v5) (not v1))
	(or (not v7) (not v2) v12)
	(or  v1 (not v20) v19)
	(or (not v2) (not v13) (not v8))
	(or  v15 v18 v4)
	(or (not v11) v14 v9)
	(or (not v6) (not v15) (not v2))
	(or  v5 (not v12) (not v15))
	(or (not v6) v17 v5)
	(or (not v13) v5 (not v19))
	(or  v20 (not v1) v14)
	(or  v9 (not v17) v15)
	(or (not v5) v19 (not v18))
	(or (not v12) v8 (not v10))
	(or (not v18) v14 (not v4))
	(or  v15 (not v9) v13)
	(or  v9 (not v5) (not v1))
	(or  v10 (not v19) (not v14))
	(or  v20 v9 v4)
	(or (not v9) (not v2) v19)
	(or (not v5) v13 (not v17))
	(or  v2 (not v10) (not v18))
	(or (not v18) v3 v11)
	(or  v7 (not v9) v17)
	(or (not v15) (not v6) (not v3))
	(or (not v2) v3 (not v13))
	(or  v12 v3 (not v2))
	(or (not v2) (not v3) v17)
	(or  v20 (not v15) (not v16))
	(or (not v5) (not v17) (not v19))
	(or (not v20) (not v18) v11)
	(or (not v9) v1 (not v5))
	(or (not v19) v9 v17)
	(or  v12 (not v2) v17)
	(or  v4 (not v16) (not v5))
	)
      )


(defvar *b50*)
(setf *b50*
      '((or (not v3) v36 v7)
	(or (not v3) (not v42) (not v48))
	(or (not v49) (not v47) (not v41))
	(or v8 (not v40) v17)
	(or (not v21) (not v31) (not v39))
	(or v36 (not v22) v49)
	(or v27 v38 v14)
	(or v15 (not v18) v6)
	(or v6 v7 (not v43))
	(or v34 (not v7) v23)
	(or v2 v14 (not v13))
	(or v2 v47 (not v42))
	(or (not v33) (not v35) v3)
	(or v44 v40 v49)
	(or v50 v36 v31)
	(or (not v36) (not v3) (not v37))
	(or v26 (not v29) v43)
	(or v15 v29 (not v45))
	(or v24 (not v11) v18)
	(or (not v47) (not v26) v6)
	(or (not v50) (not v33) (not v10))
	(or v32 v6 v16)
	(or (not v34) v37 v41)
	(or v7 (not v28) (not v17))
	(or (not v44) v46 v19)
	(or v7 v22 (not v48))
	(or v3 v39 v34)
	(or v31 v46 (not v43))
	(or (not v27) v32 v23)
	(or v37 (not v50) (not v18))
	(or v20 v5 v11)
	(or (not v45) (not v24) v6)
	(or (not v34) (not v23) (not v14))
	(or (not v22) v21 v20)
	(or (not v17) v50 v24)
	(or (not v25) (not v24) (not v27))
	(or v3 v35 v21)
	(or (not v26) v47 (not v36))
	(or (not v28) (not v45) v49)
	(or (not v21) (not v6) v12)
	(or (not v17) (not v15) (not v39))
	(or v41 v2 (not v14))
	(or v25 v36 (not v23))
	(or (not v39) (not v3) (not v40))
	(or v50 v20 v35)
	(or v27 v31 (not v39))
	(or v45 (not v15) (not v40))
	(or v34 v50 v35)
	(or (not v1) (not v48) v12)
	(or v18 (not v35) (not v30))
	(or v27 (not v24) (not v25))
	(or (not v4) (not v33) (not v12))
	(or (not v43) (not v24) (not v37))
	(or (not v37) v31 (not v44))
	(or (not v9) (not v38) v14)
	(or v33 (not v16) v34)
	(or v4 (not v35) (not v5))
	(or (not v3) (not v21) (not v19))
	(or (not v35) (not v36) (not v29))
	(or v7 (not v43) v36)
	(or v30 v14 v41)
	(or (not v35) (not v24) (not v7))
	(or v35 (not v42) v6)
	(or (not v1) (not v15) v39)
	(or v27 v49 (not v16))
	(or (not v37) v49 (not v10))
	(or v50 (not v46) (not v3))
	(or (not v41) v20 v34)
	(or (not v1) v23 v28)
	(or (not v12) (not v30) (not v20))
	(or (not v24) v29 (not v37))
	(or v12 v5 (not v44))
	(or (not v6) (not v2) v48)
	(or (not v2) (not v49) (not v43))
	(or v1 (not v50) v24)
	(or (not v7) (not v50) (not v44))
	(or (not v41) v43 v4)
	(or v13 v15 (not v11))
	(or (not v3) (not v11) v23)
	(or v33 v48 v41)
	(or v9 v23 (not v49))
	(or (not v43) v47 v1)
	(or (not v40) v16 (not v29))
	(or v30 v19 v3)
	(or v19 (not v34) v48)
	(or (not v16) (not v44) v14)
	(or v38 (not v45) (not v12))
	(or (not v4) (not v14) (not v31))
	(or (not v48) v35 (not v1))
	(or v45 (not v13) v19)
	(or v9 v42 (not v7))
	(or (not v1) (not v15) v8)
	(or (not v13) (not v44) (not v14))
	(or (not v43) (not v37) (not v31))
	(or (not v27) (not v29) v47)
	(or v7 v4 v17)
	(or v7 v10 v35)
	(or (not v25) v20 v17)
	(or v35 (not v5) (not v42))
	(or (not v50) v24 (not v5))
	(or (not v21) (not v26) v2)
	(or (not v8) v45 (not v21))
	(or (not v16) v33 v49)
	(or (not v38) v6 v16)
	(or v5 v21 v37)
	(or v8 v38 v31)
	(or (not v21) v33 v14)
	(or v20 v40 (not v5))
	(or (not v29) (not v9) v31)
	(or (not v7) v42 (not v22))
	(or (not v48) v8 v26)
	(or v48 (not v38) v33)
	(or (not v34) v49 v46)
	(or (not v14) (not v46) v25)
	(or (not v46) v4 v18)
	(or v36 (not v12) (not v31))
	(or v12 (not v18) v14)
	(or (not v7) v46 (not v16))
	(or v9 (not v8) v7)
	(or v49 (not v42) (not v22))
	(or v22 (not v15) v38)
	(or v34 (not v41) v47)
	(or v22 (not v26) v32)
	(or (not v25) (not v45) (not v21))
	(or (not v26) v32 (not v11))
	(or v15 v26 (not v25))
	(or (not v1) v46 v25)
	(or (not v14) (not v31) v30)
	(or (not v9) (not v22) v12)
	(or (not v18) v26 (not v35))
	(or (not v16) (not v32) (not v21))
	(or v31 (not v49) (not v21))
	(or v11 v9 v41)
	(or (not v13) (not v30) v19)
	(or (not v10) v4 v6)
	(or (not v4) v3 (not v22))
	(or (not v25) (not v50) (not v18))
	(or (not v40) v4 v9)
	(or v37 v20 v46)
	(or (not v27) v22 (not v29))
	(or v34 v14 v3)
	(or v3 (not v31) v20)
	(or (not v50) v2 (not v26))
	(or v17 (not v29) v38)
	(or (not v49) v12 (not v41))
	(or v15 (not v35) (not v43))
	(or (not v22) (not v23) (not v49))
	(or (not v9) v33 v48)
	(or v26 v29 v35)
	(or v27 (not v50) v37)
	(or (not v7) v46 (not v43))
	(or (not v46) (not v37) (not v8))
	(or (not v40) v36 (not v24))
	(or (not v44) v46 v15)
	(or (not v3) v36 (not v16))
	(or (not v48) v9 v43)
	(or (not v25) (not v4) v44)
	(or (not v22) v37 (not v7))
	(or (not v31) (not v17) (not v22))
	(or (not v11) (not v48) v17)
	(or v23 v34 (not v28))
	(or v23 (not v48) (not v39))
	(or (not v37) (not v1) (not v23))
	(or (not v19) v27 v14)
	(or (not v22) v33 (not v6))
	(or (not v6) (not v32) (not v26))
	(or v18 (not v20) (not v46))
	(or v43 v22 v27)
	(or (not v13) v34 v49)
	(or (not v35) (not v46) v3)
	(or v32 v39 (not v43))
	(or v6 (not v39) (not v9))
	(or v27 v39 (not v16))
	(or v25 (not v17) (not v15))
	(or (not v43) v27 v34)
	(or (not v6) v49 v5)
	(or (not v38) v11 v14)
	(or v40 (not v38) v47)
	(or v37 (not v14) v17)
	(or v39 v29 v36)
	(or (not v39) (not v28) v1)
	(or (not v18) v14 (not v16))
	(or (not v40) v50 v15)
	(or v37 (not v42) v18)
	(or (not v13) v31 v33)
	(or v2 (not v42) v33)
	(or v8 (not v3) (not v22))
	(or v1 v23 (not v31))
	(or (not v20) (not v45) v26)
	(or v42 v11 v49)
	(or v29 v11 (not v43))
	(or (not v20) (not v21) v30)
	(or v23 v45 (not v35))
	(or v38 (not v30) (not v14))
	(or (not v9) v48 (not v29))
	(or v11 (not v18) (not v23))
	(or (not v41) (not v1) (not v29))
	(or v5 v41 v26)
	(or v44 (not v30) (not v7))
	(or v38 (not v6) (not v41))
	(or v46 v48 (not v15))
	(or (not v18) (not v10) (not v47))
	(or v38 v46 (not v32))
	(or (not v32) v46 v12)
	(or v31 v40 v14)
	(or (not v18) v2 v49)
	(or v28 (not v38) v27)
	(or (not v16) (not v21) v14)
	(or (not v29) v15 v12)
	(or v49 v34 v5)
	(or v14 v22 (not v12))
	(or v30 v33 v20)
	(or (not v24) v22 v25)
	(or v4 (not v48) (not v23))
	(or (not v30) (not v36) v9)
	(or v44 v12 (not v35))
	(or v38 v3 (not v21))
	(or (not v11) v33 v49)
	)
      )