From 560818e01afa523001f29334982193caed938aa4 Mon Sep 17 00:00:00 2001 From: Utz-Uwe Haus Date: Fri, 13 May 2011 12:20:30 +0200 Subject: [PATCH] modify default solver parameters Signed-off-by: Utz-Uwe Haus --- cuddsat.lisp | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) 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)) -- 2.11.4.GIT