Most of the time is spent in `print-cnf` on large instances: use a hash-table instead of a list

[lpaviets]

When working somewhat large problems, most of the time spent is not due to the actual SAT solver, but to the conversion of the Lisp sat-instance to a proper instance understood by the solvers. This is because print-cnf uses a list of variables and linear lookup time to encode each variable.

Using a hash-table instead speeds up the conversion, and in practice, makes the conversion take less than a second for problems which required several minutes of encoding before.

(defun print-cnf (instance &optional (stream *standard-output*) (*verbosity* *verbosity*))
  (ematch instance
    ((sat-instance cnf variables)
     (when (<= 1 *verbosity*)
       (pprint-logical-block (stream nil :per-line-prefix "c ")
         (when (<= 2 *verbosity*)
           (format stream "~&~a" cnf))
         (iter (for i from 1)
           (for v in-vector variables)
           (format stream "~&Variable ~a : ~a" i v))))
     (let ((atom-to-num (make-hash-table))) ; definition of the table
       (loop :for atom :across variables    ; all the uncommented lines
             :for i :from 1                 ; after this one
             :do (setf (gethash atom atom-to-num) i)) ; are unchanged
       (match cnf
         ((or (list* 'and clauses)
              (<> clauses (list cnf)))
          (format stream "~&p cnf ~A ~A" (length variables) (length clauses))

          (iter (for c in clauses)
            (ematch c
              ((or (list* 'or terms)
                   (<> terms (list c)))
               (when (<= 3 *verbosity*)
                 (format stream "~&c ~a" c))
               (format stream "~&~{~a ~}0"
                       (iter (for term in terms)
                         (collect
                             (ematch term
                               ((list 'not atom)
                                (- (gethash atom atom-to-num))) ; lookup in the table instead of the list
                               (atom
                                (gethash atom atom-to-num))))))))) ; same here
          (fresh-line stream)))))))

[guicho271828]

Pull request welcome!