Download
;;; -*- Mode: LISP; Syntax: Common-Lisp -*-
;;; File: qga.lsp
;;; this code can be used to generate the sets of clauses for
;;; quasigroup examples used in H. Zhang and M.E. Stickel,
;;; "Implementing the Davis-Putnam Method", submitted to the
;;; SAT 2000 special issue of Journal of Automated Reasoning
;;;
;;; to write a set of quasigroup example files in DIMACS format:
;;; (compile-file "qga.lsp")
;;; (load "qga")
;;;
;;; written by Mark E. Stickel (stickel@ai.sri.com)
(defmacro COLLECT (item place)
;; like (setf place (nconc place (list item)))
;; except last cell of list is remembered in place-last
;; so that operation is O(1)
;; collect can be used instead of (push item place) + (nreverse place) loop idiom
;; user must declare place-last variable or slot
(let* ((args (if (atom place) nil (mapcar #'(lambda (arg) (list (gensym) arg)) (rest place))))
(place (if (atom place) place (cons (first place) (mapcar #'first args))))
(place-last (if (atom place)
(intern (concatenate 'string (symbol-name place) "-LAST"))
(cons (intern (concatenate 'string (symbol-name (first place)) "-LAST"))
(rest place))))
(v (gensym))
(l (gensym)))
`(let* ((,v (cons ,item nil)) ,@args (,l ,place))
(cond
((null ,l)
(setf ,place (setf ,place-last ,v)))
(t
(rplacd ,place-last (setf ,place-last ,v))
,l)))))
(defstruct DP-CLAUSE-SET
(atoms nil)
(number-of-atoms 0) ;; in atom-hash-table, may not all appear in clauses
(number-of-clauses 0)
(number-of-literals 0)
(p-clauses nil) ;; clauses that initially contained only positive literals
(n-clauses nil) ;; clauses that initially contained only negative literals
(m1-clauses nil) ;; clauses that initially were mixed Horn clauses
(m2-clauses nil) ;; clauses that initially were mixed non-Horn clauses
(atom-hash-table (make-hash-table :test #'equal))
(atoms-last nil)
(p-clauses-last nil)
(n-clauses-last nil)
(m1-clauses-last nil)
(m2-clauses-last nil)
(number-to-atom-hash-table (make-hash-table)))
(defstruct DP-CLAUSE
(number-of-unresolved-positive-literals 0 :type fixnum)
(number-of-unresolved-negative-literals 0 :type fixnum)
(positive-literals nil)
(negative-literals nil)
(next nil))
(defstruct DP-ATOM
name
number
(value nil)
(contained-positively-clauses nil)
(contained-negatively-clauses nil)
(next nil)
(number-of-occurrences 0))
(defvar *DEFAULT-DIMACS-CNF-FORMAT* :p)
(defvar *DEFAULT-PRINT-WARNINGS* nil)
(defun DP-INSERT (clause clause-set &optional (print-warnings *default-print-warnings*))
(cl:assert (not (null clause)) ()
"Cannot insert the empty clause.")
(cl:assert (not (member 0 clause)) ()
"Clause ~S contains 0, which cannot be used as a literal." clause)
(if clause-set
(assert-dp-clause-set-p clause-set)
(setq clause-set (make-dp-clause-set)))
(unless (eq print-warnings :safe)
(let ((v (clause-contains-repeated-atom clause)))
(cond
((eq v :tautology)
(when print-warnings
(warn "Complementary literals in clause ~A." clause))
(return-from dp-insert
clause-set))
(v
(when print-warnings
(warn "Duplicate literals in clause ~A." clause))
(setq clause (delete-duplicates clause :test #'equal))))))
(let ((cl (make-dp-clause))
(nlits 0)
(p 0)
(n 0)
(positive-literals nil)
(negative-literals nil)
positive-literals-last
negative-literals-last)
(dolist (lit clause)
(let* ((pos (positive-literal-p lit))
(atom0 (if pos lit (complementary-literal lit)))
(atom (if (dp-atom-p atom0)
atom0
(atom-named atom0
clause-set
:if-does-not-exist :create))))
(incf (dp-atom-number-of-occurrences atom))
(incf nlits)
(cond
(pos
(unless (eq :false (dp-atom-value atom))
(incf p))
(collect atom positive-literals)
(push cl (dp-atom-contained-positively-clauses atom)))
(t
(unless (eq :true (dp-atom-value atom))
(incf n))
(collect atom negative-literals)
(push cl (dp-atom-contained-negatively-clauses atom))))))
(incf (dp-clause-set-number-of-clauses clause-set))
(incf (dp-clause-set-number-of-literals clause-set) nlits)
(when positive-literals
(setf (dp-clause-number-of-unresolved-positive-literals cl) p)
(setf (dp-clause-positive-literals cl) positive-literals))
(when negative-literals
(setf (dp-clause-number-of-unresolved-negative-literals cl) n)
(setf (dp-clause-negative-literals cl) negative-literals))
(cond
((null negative-literals)
(if (dp-clause-set-p-clauses clause-set)
(let ((temp (dp-clause-set-p-clauses-last clause-set)))
(setf (dp-clause-next temp)
(setf (dp-clause-set-p-clauses-last clause-set) cl)))
(setf (dp-clause-set-p-clauses clause-set)
(setf (dp-clause-set-p-clauses-last clause-set) cl))))
((null positive-literals)
(if (dp-clause-set-n-clauses clause-set)
(let ((temp (dp-clause-set-n-clauses-last clause-set)))
(setf (dp-clause-next temp)
(setf (dp-clause-set-n-clauses-last clause-set) cl)))
(setf (dp-clause-set-n-clauses clause-set)
(setf (dp-clause-set-n-clauses-last clause-set) cl))))
((null (rest positive-literals))
(if (dp-clause-set-m1-clauses clause-set)
(let ((temp (dp-clause-set-m1-clauses-last clause-set)))
(setf (dp-clause-next temp)
(setf (dp-clause-set-m1-clauses-last clause-set) cl)))
(setf (dp-clause-set-m1-clauses clause-set)
(setf (dp-clause-set-m1-clauses-last clause-set) cl))))
(t
(if (dp-clause-set-m2-clauses clause-set)
(let ((temp (dp-clause-set-m2-clauses-last clause-set)))
(setf (dp-clause-next temp)
(setf (dp-clause-set-m2-clauses-last clause-set) cl)))
(setf (dp-clause-set-m2-clauses clause-set)
(setf (dp-clause-set-m2-clauses-last clause-set) cl))))))
clause-set)
(defvar *DP-READ-STRING*)
(defvar *DP-READ-INDEX*)
(defun DP-READ (s dimacs-cnf-format print-warnings)
;; reads a single clause if dimacs-cnf-format = nil
;; reads a single literal if dimacs-cnf-format = t
(loop
(cond
(dimacs-cnf-format
(multiple-value-bind (x i)
(read-from-string *dp-read-string* nil :eof :start *dp-read-index*)
(cond
((eq :eof x)
(if (eq :eof (setq *dp-read-string* (read-line s nil :eof)))
(return :eof)
(setq *dp-read-index* 0)))
((integerp x)
(setq *dp-read-index* i)
(return x))
((eql 0 *dp-read-index*) ;ignore DIMACS problem/comment line
(when print-warnings
(warn "Skipping line ~A" *dp-read-string*))
(if (eq :eof (setq *dp-read-string* (read-line s nil :eof)))
(return :eof)
(setq *dp-read-index* 0)))
(t
(when print-warnings
(warn "Skipping noninteger ~A" x))
(setq *dp-read-index* i)))))
(t
(let ((x (read s nil :eof)))
(cond
((or (eq :eof x) (consp x))
(return x)) ;no syntax checking
(print-warnings
(warn "Skipping nonclause ~A" x))))))))
(defmacro CLAUSE-CONTAINS-TRUE-POSITIVE-LITERAL (clause)
(let ((atom (gensym)))
`(dolist (,atom (dp-clause-positive-literals ,clause) nil)
(when (eq :true (dp-atom-value ,atom))
(return t)))))
(defmacro CLAUSE-CONTAINS-TRUE-NEGATIVE-LITERAL (clause)
(let ((atom (gensym)))
`(dolist (,atom (dp-clause-negative-literals ,clause))
(when (eq :false (dp-atom-value ,atom))
(return t)))))
(defun DP-COUNT (clause-set &optional print-p)
;; (dp-count clause-set) returns and optionally prints the
;; clause and literal count of clauses stored in clause-set
(let ((nclauses 0) (nliterals 0) (natoms 0) (assigned nil))
(when clause-set
(dolist (atom (dp-clause-set-atoms clause-set))
(when (or (dp-atom-contained-positively-clauses atom) ;atom appears in clause-set
(dp-atom-contained-negatively-clauses atom))
(if (dp-atom-value atom)
(setq assigned t)
(incf natoms))))
(cond
((not assigned)
(setq nclauses (dp-clause-set-number-of-clauses clause-set))
(setq nliterals (dp-clause-set-number-of-literals clause-set)))
(t
(do ((clause (dp-clause-set-p-clauses clause-set) (dp-clause-next clause)))
((null clause))
(unless (clause-contains-true-positive-literal clause)
(incf nclauses)
(incf nliterals (dp-clause-number-of-unresolved-positive-literals clause))))
(do ((clause (dp-clause-set-n-clauses clause-set) (dp-clause-next clause)))
((null clause))
(unless (clause-contains-true-negative-literal clause)
(incf nclauses)
(incf nliterals (dp-clause-number-of-unresolved-negative-literals clause))))
(do ((clause (dp-clause-set-m1-clauses clause-set) (dp-clause-next clause)))
((null clause))
(unless (or (clause-contains-true-positive-literal clause)
(clause-contains-true-negative-literal clause))
(incf nclauses)
(incf nliterals (dp-clause-number-of-unresolved-positive-literals clause))
(incf nliterals (dp-clause-number-of-unresolved-negative-literals clause))))
(do ((clause (dp-clause-set-m2-clauses clause-set) (dp-clause-next clause)))
((null clause))
(unless (or (clause-contains-true-positive-literal clause)
(clause-contains-true-negative-literal clause))
(incf nclauses)
(incf nliterals (dp-clause-number-of-unresolved-positive-literals clause))
(incf nliterals (dp-clause-number-of-unresolved-negative-literals clause)))))))
(when print-p
(format t "~&Clause set contains ~D clauses with ~D literals formed from ~D atoms~A."
nclauses nliterals natoms (if (stringp print-p) print-p "")))
(values nclauses nliterals natoms)))
(defun DP-CLAUSES (map-fun clause-set &optional decode-fun)
;; either return or apply map-fun to all clauses in clause-set
(when clause-set
(cond
(map-fun
(do ((clause (dp-clause-set-p-clauses clause-set) (dp-clause-next clause)))
((null clause))
(unless (clause-contains-true-positive-literal clause)
(funcall map-fun (decode-dp-clause clause decode-fun))))
(do ((clause (dp-clause-set-n-clauses clause-set) (dp-clause-next clause)))
((null clause))
(unless (clause-contains-true-negative-literal clause)
(funcall map-fun (decode-dp-clause clause decode-fun))))
(do ((clause (dp-clause-set-m1-clauses clause-set) (dp-clause-next clause)))
((null clause))
(unless (or (clause-contains-true-positive-literal clause)
(clause-contains-true-negative-literal clause))
(funcall map-fun (decode-dp-clause clause decode-fun))))
(do ((clause (dp-clause-set-m2-clauses clause-set) (dp-clause-next clause)))
((null clause))
(unless (or (clause-contains-true-positive-literal clause)
(clause-contains-true-negative-literal clause))
(funcall map-fun (decode-dp-clause clause decode-fun)))))
(t
(let ((result nil) result-last)
(do ((clause (dp-clause-set-p-clauses clause-set) (dp-clause-next clause)))
((null clause))
(unless (clause-contains-true-positive-literal clause)
(collect (decode-dp-clause clause decode-fun) result)))
(do ((clause (dp-clause-set-n-clauses clause-set) (dp-clause-next clause)))
((null clause))
(unless (clause-contains-true-negative-literal clause)
(collect (decode-dp-clause clause decode-fun) result)))
(do ((clause (dp-clause-set-m1-clauses clause-set) (dp-clause-next clause)))
((null clause))
(unless (or (clause-contains-true-positive-literal clause)
(clause-contains-true-negative-literal clause))
(collect (decode-dp-clause clause decode-fun) result)))
(do ((clause (dp-clause-set-m2-clauses clause-set) (dp-clause-next clause)))
((null clause))
(unless (or (clause-contains-true-positive-literal clause)
(clause-contains-true-negative-literal clause))
(collect (decode-dp-clause clause decode-fun) result)))
result)))))
(defun DP-OUTPUT-CLAUSES-TO-FILE (filename clause-set &key (dimacs-cnf-format *default-dimacs-cnf-format*))
;; write clauses in clause-set to a file
(with-open-file (s filename :direction :output :if-exists :new-version)
(cond
(dimacs-cnf-format
(when (eq :p dimacs-cnf-format)
(format s "p cnf ~D ~D~%" (dp-clause-set-number-of-atoms clause-set) (dp-count clause-set)))
(dp-clauses #'(lambda (clause)
(dolist (lit clause)
(princ lit s)
(princ " " s))
(princ 0 s)
(terpri s))
clause-set
(if (dolist (atom (dp-clause-set-atoms clause-set) t)
(unless (and (integerp (dp-atom-name atom))
(plusp (dp-atom-name atom)))
(return nil)))
nil
#'dp-atom-number)))
(t
(dp-clauses #'(lambda (clause)
(prin1 clause s)
(terpri s))
clause-set))))
nil)
(defun ASSERT-DP-CLAUSE-SET-P (clause-set)
(cl:assert (dp-clause-set-p clause-set) ()
"~S is not a dp-clause-set." clause-set))
(defun ATOM-NAMED (x clause-set &key (if-does-not-exist :error))
(cl:assert (not (null x)) ()
"~A cannot be used as an atomic formula." x)
(let ((table (dp-clause-set-atom-hash-table clause-set)))
(or (gethash x table)
(ecase if-does-not-exist
(:create
(let ((atom (make-dp-atom
:name x
:number (incf (dp-clause-set-number-of-atoms clause-set)))))
(if (dp-clause-set-atoms clause-set)
(let ((temp (dp-clause-set-atoms-last clause-set)))
(setf (cdr temp)
(setf (dp-clause-set-atoms-last clause-set)
(cons atom nil))))
(setf (dp-clause-set-atoms clause-set)
(setf (dp-clause-set-atoms-last clause-set)
(cons atom nil))))
(setf (gethash (dp-atom-number atom) (dp-clause-set-number-to-atom-hash-table clause-set)) atom)
(setf (gethash x table) atom)))
(:error
(error "Unknown atom ~A." x))
((nil)
nil)))))
(defun POSITIVE-LITERAL-P (lit)
(cond
((numberp lit)
(plusp lit))
((and (consp lit) (eq 'not (first lit)))
nil)
(t
t)))
(defun COMPLEMENTARY-LITERAL (lit)
(cond
((numberp lit)
(- lit))
((and (consp lit) (eq 'not (first lit)))
(second lit))
(t
(list 'not lit))))
(defun CLAUSE-CONTAINS-REPEATED-ATOM (clause)
(do* ((dup nil)
(lits clause (rest lits))
(lit (first lits) (first lits))
(clit (complementary-literal lit) (complementary-literal lit)))
((null (rest lits))
dup)
(dolist (lit2 (rest lits))
(cond
((equal lit lit2)
(setq dup t))
((equal clit lit2)
(return-from clause-contains-repeated-atom
:tautology))))))
(defun DECODE-DP-CLAUSE (clause &optional decode-fun)
(let ((result nil) result-last)
(dolist (atom (dp-clause-negative-literals clause))
(unless (dp-atom-value atom)
(collect (let ((atom (if decode-fun
(funcall decode-fun atom)
(dp-atom-name atom))))
(cond
((numberp atom)
(- atom))
(t
(list 'not atom))))
result)))
(dolist (atom (dp-clause-positive-literals clause))
(unless (dp-atom-value atom)
(collect (if decode-fun
(funcall decode-fun atom)
(dp-atom-name atom))
result)))
result))
(defun ENCODE-QG-ATOM (n i j k)
(declare (ignore n))
`(,i * ,j = ,k))
(defun NEGATE (atom)
`(not ,atom))
(defvar USE-ROW-AND-COLUMN-SURJECTIVITY t)
(defun QG (v &key (isomorphism-reducing-constraint 'last-column)
not-necessarily-idempotent (clause-set (make-dp-clause-set)))
(cond
((not not-necessarily-idempotent)
(loop for i from 1 upto v
do (dp-insert
(list (encode-qg-atom v i i i))
clause-set))))
(unless (eq isomorphism-reducing-constraint 'none)
(loop for i from 1 upto v
do (loop for j from 1 upto v
when (< (1+ j) i)
do (dp-insert
(list (negate (ecase isomorphism-reducing-constraint
(first-row
(encode-qg-atom v 1 i j))
(last-row
(encode-qg-atom v v i j))
(first-column
(encode-qg-atom v i 1 j))
(last-column
(encode-qg-atom v i v j))
(first-value
(encode-qg-atom v i j 1))
(last-value
(encode-qg-atom v i j v)))))
clause-set))))
(loop for i from 1 upto v
do (loop for j from 1 upto v
do (dp-insert
(loop for k from 1 upto v
collect (encode-qg-atom v i j k))
clause-set)))
(when use-row-and-column-surjectivity
(loop for i from 1 upto v
do (loop for j from 1 upto v
do (dp-insert
(loop for k from 1 upto v
collect (encode-qg-atom v i k j))
clause-set)
(dp-insert
(loop for k from 1 upto v
collect (encode-qg-atom v k i j))
clause-set))))
(loop for i from 1 upto v
do (loop for j from 1 upto v
do (loop for k1 from 1 upto v
do (loop for k2 from (1+ k1) upto v
do (dp-insert
(list (negate (encode-qg-atom v i j k1))
(negate (encode-qg-atom v i j k2)))
clause-set)
(dp-insert
(list (negate (encode-qg-atom v i k1 j))
(negate (encode-qg-atom v i k2 j)))
clause-set)
(dp-insert
(list (negate (encode-qg-atom v k1 i j))
(negate (encode-qg-atom v k2 i j)))
clause-set)))))
clause-set)
(defun ADD-QG1-CONSTRAINT (clause-set v)
(loop for a from 1 upto v
do (loop for b from 1 upto v
do (loop for c from a upto v ;symmetric in a,c, so skip c in [1,a)
do (loop for d from 1 upto v
unless (and (= a c) (= b d))
do (loop for ab from 1 upto v
do (loop for x from 1 upto v
do (dp-insert
(list (negate (encode-qg-atom v a b ab))
(negate (encode-qg-atom v c d ab))
(negate (encode-qg-atom v x b a))
(negate (encode-qg-atom v x d c)))
clause-set)))))))
clause-set)
(defun ADD-QG2-CONSTRAINT (clause-set v)
(loop for a from 1 upto v
do (loop for b from 1 upto v
do (loop for c from a upto v ;symmetric in a,c, so skip c in [1,a)
do (loop for d from 1 upto v
unless (and (= a c) (= b d))
do (loop for ab from 1 upto v
do (loop for x from 1 upto v
do (dp-insert
(list (negate (encode-qg-atom v a b ab))
(negate (encode-qg-atom v c d ab))
(negate (encode-qg-atom v b x a))
(negate (encode-qg-atom v d x c)))
clause-set)))))))
clause-set)
(defun ADD-QG3-CONSTRAINT (clause-set v no-extra-equation-clauses)
(loop for a from 1 upto v
do (loop for b from 1 upto v
do (loop for ab from 1 upto v
do (loop for ba from 1 upto v
do (dp-insert
(list (negate (encode-qg-atom v a b ab))
(negate (encode-qg-atom v b a ba))
(encode-qg-atom v ab ba a))
clause-set)
(unless no-extra-equation-clauses
(dp-insert
(list (encode-qg-atom v a b ab)
(negate (encode-qg-atom v b a ba))
(negate (encode-qg-atom v ab ba a)))
clause-set)
(dp-insert
(list (negate (encode-qg-atom v a b ab))
(encode-qg-atom v b a ba)
(negate (encode-qg-atom v ab ba a)))
clause-set))))))
;; Slaney: if a.ax=x or xa.a=x then a=x
(loop for a from 1 upto v
do (loop for x from 1 upto v
unless (= a x)
do (loop for u from 1 upto v
do (dp-insert
(list (negate (encode-qg-atom v a x u))
(negate (encode-qg-atom v a u x)))
clause-set)
(dp-insert
(list (negate (encode-qg-atom v x a u))
(negate (encode-qg-atom v u a x)))
clause-set))))
clause-set)
(defun ADD-QG4-CONSTRAINT (clause-set v no-extra-equation-clauses)
(loop for a from 1 upto v
do (loop for b from 1 upto v
do (loop for ab from 1 upto v
do (loop for ba from 1 upto v
do (dp-insert
(list (negate (encode-qg-atom v a b ab))
(negate (encode-qg-atom v b a ba))
(encode-qg-atom v ba ab a))
clause-set)
(unless no-extra-equation-clauses
(dp-insert
(list (encode-qg-atom v a b ab)
(negate (encode-qg-atom v b a ba))
(negate (encode-qg-atom v ba ab a)))
clause-set)
(dp-insert
(list (negate (encode-qg-atom v a b ab))
(encode-qg-atom v b a ba)
(negate (encode-qg-atom v ba ab a)))
clause-set))))))
clause-set)
(defun ADD-QG5-CONSTRAINT (clause-set v no-extra-equation-clauses)
(loop for a from 1 upto v
do (loop for b from 1 upto v
do (loop for ba from 1 upto v
do (loop for ba.b from 1 upto v
do (dp-insert
(list (negate (encode-qg-atom v b a ba))
(negate (encode-qg-atom v ba b ba.b))
(encode-qg-atom v ba.b b a))
clause-set)
;; suggested by Fujita
;; also Slaney's y(xy.y)=x and (y.xy)y=x (6/28/93)
(unless no-extra-equation-clauses
(dp-insert
(list (encode-qg-atom v b a ba)
(negate (encode-qg-atom v ba b ba.b))
(negate (encode-qg-atom v ba.b b a)))
clause-set)
(dp-insert
(list (negate (encode-qg-atom v b a ba))
(encode-qg-atom v ba b ba.b)
(negate (encode-qg-atom v ba.b b a)))
clause-set))))))
clause-set)
(defun ADD-QG6-CONSTRAINT (clause-set v)
(loop for x from 1 upto v
do (loop for a from 1 upto v
do (loop for b from 1 upto v
do (loop for ab from 1 upto v
do (dp-insert
(list (negate (encode-qg-atom v a b ab))
(negate (encode-qg-atom v ab b x))
(encode-qg-atom v a ab x))
clause-set)
(dp-insert
(list (negate (encode-qg-atom v a b ab))
(negate (encode-qg-atom v a ab x))
(encode-qg-atom v ab b x))
clause-set)))))
clause-set)
(defun ADD-QG7A-CONSTRAINT (clause-set v no-extra-equation-clauses)
;;finds (132) conjugate equivalents, as suggested by Slaney
;;note: constraint on rightmost column not translated to conjugate equivalent, so number of models differs from qg7
;; (xy.x)y=x
(loop for x from 1 upto v
do (loop for y from 1 upto v
do (loop for xy from 1 upto v
do (loop for xy.x from 1 upto v
do (dp-insert
(list (negate (encode-qg-atom v x y xy))
(negate (encode-qg-atom v xy x xy.x))
(encode-qg-atom v xy.x y x))
clause-set)
(unless no-extra-equation-clauses
(dp-insert
(list (encode-qg-atom v x y xy)
(negate (encode-qg-atom v xy x xy.x))
(negate (encode-qg-atom v xy.x y x)))
clause-set)
(dp-insert
(list (negate (encode-qg-atom v x y xy))
(encode-qg-atom v xy x xy.x)
(negate (encode-qg-atom v xy.x y x)))
clause-set))))))
;; (xy.y).xy=x
(loop for x from 1 upto v
do (loop for y from 1 upto v
do (loop for xy from 1 upto v
do (loop for xy.y from 1 upto v
do (dp-insert
(list (negate (encode-qg-atom v x y xy))
(negate (encode-qg-atom v xy y xy.y))
(encode-qg-atom v xy.y xy x))
clause-set)))))
clause-set)
(defun QG1 (v &key (isomorphism-reducing-constraint 'last-column) not-necessarily-idempotent)
(let ((clause-set (qg v
:isomorphism-reducing-constraint isomorphism-reducing-constraint
:not-necessarily-idempotent not-necessarily-idempotent)))
(add-qg1-constraint clause-set v)
clause-set))
(defun QG2 (v &key (isomorphism-reducing-constraint 'last-column) not-necessarily-idempotent)
(let ((clause-set (qg v
:isomorphism-reducing-constraint isomorphism-reducing-constraint
:not-necessarily-idempotent not-necessarily-idempotent)))
(add-qg2-constraint clause-set v)
clause-set))
(defun QG3 (v &key (isomorphism-reducing-constraint 'last-value) not-necessarily-idempotent (no-extra-equation-clauses t))
(let ((clause-set (qg v
:isomorphism-reducing-constraint isomorphism-reducing-constraint
:not-necessarily-idempotent not-necessarily-idempotent)))
(add-qg3-constraint clause-set v no-extra-equation-clauses)
clause-set))
(defun QG4 (v &key (isomorphism-reducing-constraint 'last-value) not-necessarily-idempotent (no-extra-equation-clauses t))
(let ((clause-set (qg v
:isomorphism-reducing-constraint isomorphism-reducing-constraint
:not-necessarily-idempotent not-necessarily-idempotent)))
(add-qg4-constraint clause-set v no-extra-equation-clauses)
clause-set))
(defun QG5 (v &key (isomorphism-reducing-constraint 'last-column) not-necessarily-idempotent (no-extra-equation-clauses nil))
(let ((clause-set (qg v
:isomorphism-reducing-constraint isomorphism-reducing-constraint
:not-necessarily-idempotent not-necessarily-idempotent)))
(add-qg5-constraint clause-set v no-extra-equation-clauses)
clause-set))
(defun QG6 (v &key (isomorphism-reducing-constraint 'last-column))
(let ((clause-set (qg v
:isomorphism-reducing-constraint isomorphism-reducing-constraint)))
(add-qg6-constraint clause-set v)
clause-set))
(defun QG7A (v &key (isomorphism-reducing-constraint 'last-column) (no-extra-equation-clauses t))
(let ((clause-set (qg v
:isomorphism-reducing-constraint isomorphism-reducing-constraint)))
(add-qg7a-constraint clause-set v no-extra-equation-clauses)
clause-set))
(dp-output-clauses-to-file "qg1-07.cnf" (qg1 7))
(dp-output-clauses-to-file "qg1-08.cnf" (qg1 8))
(dp-output-clauses-to-file "qg2-07.cnf" (qg2 7))
(dp-output-clauses-to-file "qg2-08.cnf" (qg2 8))
(dp-output-clauses-to-file "qg3-08.cnf" (qg3 8))
(dp-output-clauses-to-file "qg3-09.cnf" (qg3 9))
(dp-output-clauses-to-file "qg4-08.cnf" (qg4 8))
(dp-output-clauses-to-file "qg4-09.cnf" (qg4 9))
(dp-output-clauses-to-file "qg5-09.cnf" (qg5 9))
(dp-output-clauses-to-file "qg5-10.cnf" (qg5 10))
(dp-output-clauses-to-file "qg5-11.cnf" (qg5 11))
(dp-output-clauses-to-file "qg5-12.cnf" (qg5 12))
(dp-output-clauses-to-file "qg5-13.cnf" (qg5 13))
(dp-output-clauses-to-file "qg6-09.cnf" (qg6 9))
(dp-output-clauses-to-file "qg6-10.cnf" (qg6 10))
(dp-output-clauses-to-file "qg6-11.cnf" (qg6 11))
(dp-output-clauses-to-file "qg6-12.cnf" (qg6 12))
(dp-output-clauses-to-file "qg7-09.cnf" (qg7a 9))
(dp-output-clauses-to-file "qg7-10.cnf" (qg7a 10))
(dp-output-clauses-to-file "qg7-11.cnf" (qg7a 11))
(dp-output-clauses-to-file "qg7-12.cnf" (qg7a 12))
(dp-output-clauses-to-file "qg7-13.cnf" (qg7a 13))
;;; qga.lsp EOF
This work is licensed under a Creative Commons Attribution 4.0 International License.