(defun my-sat-solve (clauses &optional all-solutions-p)
  "Solve a Boolean satisfaction problem.

Returns a list containing one solution, or all solutions if
ALL-SOLUTIONS is non-nil.

The problem is specified as CNF (Conjunctive Normal Form), that is
conjunctions of disjunctions.  Each clause is a list of integers
representing literals, possibly negated."
  (let* ((domains (my-sat-domains clauses))
         (domains (my-sat-search clauses domains all-solutions-p)))
    (mapcar #'my-sat-solution domains)))