Produced some code solving the SAT problem with scheme, a functional language. It's not perfect and might caused the application to crash when the number of literals of an assignment is more than 25.. One problem is the allassign function: it will save much more space with tail recursion.. But I was too lazy to change my code.
#lang racket
;counts the the number of clauses
(define (countclauses data)
(cond
((null? data) 0)
((= (car data) 0) (+ 1 (countclauses (cdr data))))
(#t (countclauses (cdr data)))))
;determines the maximum variable number
(define (maxvar data)
(cond
((null? data) 0)
(#t (let* ((max (maxvar (cdr data)))
(c (car data))
(a (if (< c 0) (- c) c)))
(if (> a max) a max)))))
;takes a single argument, a list of integers representing a SAT problem in DIMACS format,
;and returns a list of lists, where each list represents a clause.
(define (getClauses lis)
(saveClause lis '()))
(define (saveClause lis temp)
(cond
((null? lis) '())
((zero? (car lis)) (append (list temp) (saveClause (cdr lis) '())))
(else (saveClause (cdr lis) (cons (car lis) temp)))))
;takes a positive integer n and generates all possible assignments of length n.
(define (allassign num)
(allassign2 num '(())))
(define (allassign2 num temp)
(cond
((zero? num) temp)
(else (append (allassign2 (- num 1) (list (cons #t (car temp)))) (allassign2 (- num 1) (list (cons #f (car temp))))))))
;takes a variable and a list representing an assignment
;returns the value of that variable under that assignment
(define (eval-var var lis)
(cond
((eq? var 1) (car lis))
(else (eval-var (- var 1) (cdr lis)))))
;similar function to evaluate a literal
(define (eval-lit var lis assgn)
(cond
((eq? var 1) (if (< (car lis) 0) (not (eval-var (opposite (car lis)) assgn)) (eval-var (car lis) assgn)))
(else (eval-lit (- var 1) (cdr lis) assgn))))
(define (opposite var)
(if (< var 0) (- 0 var) var))
;evaluate a clause
(define (eval-clause var lis assgn)
(cond
((eq? var 1) (eval-clause2 (car lis) assgn))
(else (eval-clause (- var 1) (cdr lis) assgn))))
(define (eval-clause2 lis assgn)
(cond
((null? lis) #f)
((eq? #t (eval-lit 1 lis assgn)) #t)
(else (eval-clause2 (cdr lis) assgn))))
;evaluate a CNF
(define (eval-form lis assgn)
(cond
((null? lis) #t)
((eq? #f (eval-clause 1 lis assgn)) #f)
(else (eval-form (cdr lis) assgn))))
;main function, determines whether a list of integers is satisfiable
(define (sat lis)
(SATsolver2 (getClauses lis) (allassign (maxvar lis))))
(define (SATsolver2 lis assgn)
(cond
((null? assgn) #f)
((eq? #t (eval-form lis (car assgn))) #t)
(else (SATsolver2 lis (cdr assgn)))))
