main.lisp

(defvar *environment* nil "The environment of an evaluation.")
(defvar *clause* nil "The input clause of an evaluation.")
(defvar *clauses* nil "A list of clauses for evaluation.")

;; a single clause is a list of 3 elements: (setf *clause* '(a (not b) c)) ;; 3-SAT clause (disjunction)
;; each element is either a single variable name (i.e. an atom) or a list containing the symbol `not' followed by a variable name

;; evaluation is with respect to an environment: (setf *environment* '((a . nil) (b . t) (c . t) (d . nil))

;; a set of clauses are evaluated with respect to each other: (setf *clauses* '((a (not b) c) (a (not b) (not c)) (a (not b) d)))

;; the list of variables in a clause can be generated with `get-variables'
;; - using this list, we can create an environment - assign each variable a default value in an environment

(defun evaluate-variable (variable environment)
  "Evaluate `variable' with respect to `environment'."
  (cdr (assoc variable environment)))

(defun evaluate-clause (clause environment)
  "Evaluate `clause' with respect to `environment'"
  (if (member t (mapcar #'(lambda (variable) (evaluate-variable variable environment)) clause))
      t
      nil))

(defun get-variables (clause)
  "Return a list of the variables in `clause'."
  (let ((vars nil))
    (cond
      ((atom clause) (push clause vars))
      ((equal (first clause) 'not) (push (second clause) vars))
      ((listp clause) (push (mapcar #'get-variables clause) vars)))
    (apply #'append vars)))

(defun get-all-variables (clauses)
  "Return a list of the variables in the list `clauses'."
  (let ((all-vars nil))
    (dolist (clause clauses)
      (let ((vars (get-variables clause)))
	(push vars all-vars)))
    (remove-duplicates (apply #'append all-vars))))

(defun unsatisfied-clauses (clauses environment)
  "Return a list of the unsatisfied `clauses' in an expression with respect to `environment'."
  (let ((unsat nil))
    (dolist (clause clauses)
      (unless (evaluate-clause clause environment)
	(push clause unsat)))
    unsat))

(defun flip-variable (variable environment)
  "Flips the truth-value of `variable' with respect to `environment'."
  (let ((temporary-env (copy-list environment)))
    (setf (cdr (assoc variable temporary-env)) (not (cdr (assoc variable temporary-env))))
    temporary-env))

(defun create-environment (clause)
  "Return an environment for `clause'."
  (let ((environment nil)
	(variables (get-variables clause)))
    (dolist (variable variables)
      (push `(,variable . nil) environment))
    environment))

(defun get-better-neighbour (clauses environment variables number-of-unsatisfied-clauses)
  "Consider S' to be a neighbour to state S, if S' can be created by flipping the state of exactly one variable in S.
   Consider S' to be a better neighbour if it generates less unsatisfied clauses than S in a given expression."
  (let ((temp-env (copy-list environment)))
    (dolist (variable variables) ;; loop over `variables'
      (let ((num-unsat (length (unsatisfied-clauses clauses (flip-variable variable temp-env)))))
	(format t "~D vs ~D~%" number-of-unsatisfied-clauses num-unsat)
	(cond
	  ((> number-of-unsatisfied-clauses num-unsat)
	   ;; (format t "~A~%" variable)
	   (return environment)))))))

;; (setf *environment* '((A . nil) (B . t) (C . t) (d . nil)))
;; (setf *clauses* '((a (not b) c) (a (not b) (not c)) (a (not b) d)))
;; (get-better-neighbour *clauses* *environment* '(a b c) (length (unsatisfied-clauses *clauses* *environment*)))

(defun solution-find (clauses state distance number-of-unsatisfied-clauses)
  (if (eq nil number-of-unsatisfied-clauses)
      state))