[DO NOT MERGED] try a different weight computation

picus/algorithms/dpvl.rkt

@@ -81,7 +81,6 @@
 (define :range-vec null)
 
 (define :linear-clauses #f)
-(define :weight-map #f)
 
 ; main solving procedure
 ; returns:
@@ -164,7 +163,7 @@
      (values 'normal ks us null)]
     ; else, set not empty, move forward
     [else
-     (define sid (apply-selector uspool :weight-map))
+     (define sid (apply-selector uspool (l0:compute-weight-map :linear-clauses)))
      (define-values (solved? info) (dpvl-solve ks us sid))
      ; send feedback to selector
      (selector-feedback sid solved?)
@@ -418,7 +417,6 @@
   ; generate linear-clauses requires no optimization to exclude ror and rand
   ; linear-clauses requires normalized constraints to get best results
   (set! :linear-clauses (l0:compute-linear-clauses :sdmcnsts #t))
-  (set! :weight-map (l0:compute-weight-map :linear-clauses))
 
   ; ==== first apply optimization phase 0 ====
   (set! :p0cnsts (:optimize-r1cs-p0 :cnsts))

picus/algorithms/lemmas/linear-lemma.rkt

@@ -41,12 +41,12 @@
   (define res (make-hash))
   (for ([clause (in-list linear-clauses)])
     (match-define (cons deducible-vars nonlinear-vars) clause)
-    ;; NOTE(sorawee): I think this is not optimal. We should revisit this.
     (define len-deducible (set-count deducible-vars))
+    (define len-nonlinear (set-count nonlinear-vars))
     (for ([var (in-set deducible-vars)])
-      (hash-update! res var (λ (old) (+ old len-deducible -1)) 0))
+      (hash-update! res var (λ (old) (max old (exact->inexact (/ 1 (+ len-deducible len-nonlinear))))) 0))
     (for ([var (in-set nonlinear-vars)])
-      (hash-update! res var (λ (old) (+ old len-deducible)) 0)))
+      (hash-update! res var (λ (old) (max old (exact->inexact (/ 1 (+ len-deducible len-nonlinear))))) 0)))
   res)
 
 ; recursively apply linear lemma