From: Utz-Uwe Haus Date: Fri, 13 May 2011 10:20:30 +0000 (+0200) Subject: modify default solver parameters X-Git-Url: https://repo.or.cz/w/cl-cudd.git/commitdiff_plain/560818e01afa523001f29334982193caed938aa4 modify default solver parameters Signed-off-by: Utz-Uwe Haus --- diff --git a/cuddsat.lisp b/cuddsat.lisp index 72d9eea..b31df5c 100644 --- a/cuddsat.lisp +++ b/cuddsat.lisp @@ -142,11 +142,21 @@ :vars vars))) (cuddapi:cudd-ref truevar) ;; it is used as inital cnf (cuddapi:cudd-enable-reordering-reporting manager) - (cuddapi:cudd-autodyn-enable manager :cudd-reorder-symm-sift) - ; (cuddapi:cudd-autodyn-enable manager :cudd-reorder-symm-sift-conv) ; (cuddapi:cudd-autodyn-enable manager :cudd-reorder-symm-sift) + ; (cuddapi:cudd-autodyn-enable manager :cudd-reorder-symm-sift-conv) + ; (cuddapi:cudd-autodyn-enable manager :cudd-reorder-sift) + (cuddapi:cudd-autodyn-enable manager :cudd-reorder-symm-sift) + (cuddapi:cudd-autodyn-enable manager :cudd-reorder-window-4) + (cuddapi:cudd-set-max-growth manager 12d0) + (format T ";; cudd: max sift growth ~D, max number of variables sifted: ~D~%" + (cuddapi:cudd-read-max-growth manager) + (cuddapi:cudd-read-sift-max-var manager)) (loop :for c :in clauses - :do (sat-env-add-clause env c)) + :with numclauses := (length clauses) + :for counter :downfrom numclauses + :do (sat-env-add-clause env c) + :when (= 0 (mod counter 10)) + :do (format T "~&;; ~D clauses to go~%" counter)) env))