SAT solver

Hello ,
I have to do satisfibility slover program which accept CNF as list and return one model at least for CNF or nil of there is not model ?

for example if function
(SAT '(and (or :X (not :Y) :Z) (or :X :Z) (not :A) :B))
return ((:Z . T) (:B . T) (:A . NIL))


Any help i am stuck i have to do it ASAP !!

thank you for help ,

So what have you written so far? CL, pseudocode, anything?

I don't know how to start please help me guys

You say you "have to do" this. Is it for a course you're studying? If so, I'd recommend going through your course notes and textbook, and possibly asking your teacher or tutor for some pointers.

The place to start would be understanding the problem: look at what it is that you have to do - what input you need to start with, and what output you need to generate as a result - and figure out the logic of it. The implementation (writing the code) comes after that.

Sorry, but this really does smell like homework. We're happy to help you understand aspects of the language, but we won't do your assignment for you.