Merge scratch with master branch

diff --git a/src/1.log b/src/1.log
deleted file mode 100644 (file)
index 3b13110..0000000
--- a/src/1.log
+++ /dev/null
@@ -1,2018 +0,0 @@
-deserializing ...
-**********************
-Polarity time: 0.004035
-Preprocess time: 0.013218
-Decompose Order: 0.000012
-Encoding Graph Time: 0.041886
-Elapse Encode time: 1.090344
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000001
-SAT Solving time: 172.826413
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 173.916775
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003925
-Preprocess time: 0.012769
-Decompose Order: 0.000007
-Encoding Graph Time: 0.077234
-Elapse Encode time: 0.175357
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 173.880185
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 174.055553
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 174055552888.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003697
-Preprocess time: 0.000014
-Decompose Order: 0.000004
-Encoding Graph Time: 0.078022
-Elapse Encode time: 0.162977
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 169.950790
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 170.113780
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 170113779509.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003722
-Preprocess time: 0.000013
-Decompose Order: 0.000003
-Encoding Graph Time: 0.004957
-Elapse Encode time: 3.665021
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 185.708077
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 189.373110
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 189373110441.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 5         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003696
-Preprocess time: 0.000014
-Decompose Order: 0.000003
-Encoding Graph Time: 0.004988
-Elapse Encode time: 3.656909
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 223.981770
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 227.638691
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 227638691365.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003746
-Preprocess time: 0.012362
-Decompose Order: 0.000006
-Encoding Graph Time: 0.005093
-Elapse Encode time: 3.673204
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 204.648955
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 208.322172
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 208322171971.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003783
-Preprocess time: 0.000014
-Decompose Order: 0.000003
-Encoding Graph Time: 0.005070
-Elapse Encode time: 3.660124
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 168.955967
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 172.616103
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 172616103387.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 3         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003876
-Preprocess time: 0.000014
-Decompose Order: 0.000033
-Encoding Graph Time: 0.005254
-Elapse Encode time: 3.743260
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 204.470081
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 208.213356
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 208213356243.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004094
-Preprocess time: 0.000013
-Decompose Order: 0.000004
-Encoding Graph Time: 0.080160
-Elapse Encode time: 0.165375
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 160.109910
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 160.275297
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 160275296708.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 5         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004059
-Preprocess time: 0.000014
-Decompose Order: 0.000003
-Encoding Graph Time: 0.078355
-Elapse Encode time: 0.163761
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 156.193350
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 156.357122
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 156357122315.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004075
-Preprocess time: 0.000012
-Decompose Order: 0.000003
-Encoding Graph Time: 0.005185
-Elapse Encode time: 3.663215
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 203.557549
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 207.220776
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 207220776365.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 0        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003905
-Preprocess time: 0.000010
-Decompose Order: 0.000003
-Encoding Graph Time: 0.005012
-Elapse Encode time: 3.644834
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 212.951258
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 216.596105
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 216596104827.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003877
-Preprocess time: 0.012756
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005143
-Elapse Encode time: 3.682618
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 209.801021
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 213.483652
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 213483652346.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003956
-Preprocess time: 0.012794
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005206
-Elapse Encode time: 3.699788
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 212.723803
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 216.423604
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 216423604309.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 1         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003936
-Preprocess time: 0.012737
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005156
-Elapse Encode time: 3.788655
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 193.596544
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 197.385211
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 197385211257.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003742
-Preprocess time: 0.012359
-Decompose Order: 0.000007
-Encoding Graph Time: 0.076438
-Elapse Encode time: 0.173937
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 160.742431
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 160.916381
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 160916380571.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003737
-Preprocess time: 0.012349
-Decompose Order: 0.000006
-Encoding Graph Time: 0.005086
-Elapse Encode time: 3.669822
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 188.818087
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 192.487921
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 192487920763.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 2         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003727
-Preprocess time: 0.012391
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005276
-Elapse Encode time: 3.682198
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 211.634056
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 215.316267
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 215316267144.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 0        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003778
-Preprocess time: 0.012453
-Decompose Order: 0.000008
-Encoding Graph Time: 0.005142
-Elapse Encode time: 3.676799
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 198.427101
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 202.103912
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 202103912479.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003800
-Preprocess time: 0.000013
-Decompose Order: 0.000004
-Encoding Graph Time: 0.005169
-Elapse Encode time: 3.694777
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 213.284328
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 216.979118
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 216979117988.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003946
-Preprocess time: 0.000011
-Decompose Order: 0.000003
-Encoding Graph Time: 0.005132
-Elapse Encode time: 3.723860
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 175.762665
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 179.486539
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 179486538926.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003912
-Preprocess time: 0.012528
-Decompose Order: 0.000008
-Encoding Graph Time: 0.005059
-Elapse Encode time: 3.674142
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 211.915724
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 215.589878
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 215589878125.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 0        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004946
-Preprocess time: 0.014076
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005094
-Elapse Encode time: 3.698828
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 211.473552
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 215.172394
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 215172393540.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004016
-Preprocess time: 0.000011
-Decompose Order: 0.000003
-Encoding Graph Time: 0.005101
-Elapse Encode time: 3.708234
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 175.099455
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 178.807702
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 178807701670.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003954
-Preprocess time: 0.000011
-Decompose Order: 0.000003
-Encoding Graph Time: 0.005191
-Elapse Encode time: 3.710612
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 189.884156
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 193.594781
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 193594780541.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003990
-Preprocess time: 0.000011
-Decompose Order: 0.000003
-Encoding Graph Time: 0.077490
-Elapse Encode time: 0.162925
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 161.874690
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 162.037625
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 162037625387.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004718
-Preprocess time: 0.000019
-Decompose Order: 0.000004
-Encoding Graph Time: 0.006761
-Elapse Encode time: 3.685110
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 196.936218
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 200.621340
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 200621339784.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004118
-Preprocess time: 0.013453
-Decompose Order: 0.000009
-Encoding Graph Time: 0.005998
-Elapse Encode time: 3.686376
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 194.281813
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 197.968202
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 197968202182.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003897
-Preprocess time: 0.000011
-Decompose Order: 0.000003
-Encoding Graph Time: 0.005008
-Elapse Encode time: 3.673334
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 209.588656
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 213.262002
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 213262001799.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003856
-Preprocess time: 0.012520
-Decompose Order: 0.000008
-Encoding Graph Time: 0.077373
-Elapse Encode time: 0.175199
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 160.810740
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 160.985950
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 160985949607.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003781
-Preprocess time: 0.000015
-Decompose Order: 0.000005
-Encoding Graph Time: 0.077545
-Elapse Encode time: 0.162992
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 160.765425
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 160.928428
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 160928427691.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 2         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003909
-Preprocess time: 0.000016
-Decompose Order: 0.000004
-Encoding Graph Time: 0.078728
-Elapse Encode time: 0.164136
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 162.124576
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 162.288723
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 162288723346.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003781
-Preprocess time: 0.000012
-Decompose Order: 0.000005
-Encoding Graph Time: 0.004942
-Elapse Encode time: 3.680737
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 209.995768
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 213.676518
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 213676517632.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 4         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003945
-Preprocess time: 0.000011
-Decompose Order: 0.000003
-Encoding Graph Time: 0.078411
-Elapse Encode time: 0.163838
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 164.902978
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 165.066828
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 165066827531.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003898
-Preprocess time: 0.000011
-Decompose Order: 0.000004
-Encoding Graph Time: 0.005102
-Elapse Encode time: 3.732650
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 174.291819
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 178.024506
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 178024506426.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 0        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003741
-Preprocess time: 0.000014
-Decompose Order: 0.000004
-Encoding Graph Time: 0.005041
-Elapse Encode time: 3.693665
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 210.357435
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 214.051112
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 214051112258.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003847
-Preprocess time: 0.012496
-Decompose Order: 0.000008
-Encoding Graph Time: 0.005112
-Elapse Encode time: 3.687460
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 213.431153
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 217.118625
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 217118624848.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003863
-Preprocess time: 0.012529
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005267
-Elapse Encode time: 3.728645
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 176.863374
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 180.592032
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 180592031883.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 0        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003859
-Preprocess time: 0.012417
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005122
-Elapse Encode time: 3.670089
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 192.040423
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 195.710525
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 195710524957.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003848
-Preprocess time: 0.000014
-Decompose Order: 0.000004
-Encoding Graph Time: 0.005036
-Elapse Encode time: 3.685831
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 197.900643
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 201.586486
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 201586486320.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003800
-Preprocess time: 0.000011
-Decompose Order: 0.000004
-Encoding Graph Time: 0.005104
-Elapse Encode time: 3.653650
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 191.699499
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 195.353162
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 195353162260.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 0        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003814
-Preprocess time: 0.000012
-Decompose Order: 0.000003
-Encoding Graph Time: 0.005189
-Elapse Encode time: 3.650501
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 201.154915
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 204.805428
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 204805427968.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 2         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003763
-Preprocess time: 0.000014
-Decompose Order: 0.000004
-Encoding Graph Time: 0.005082
-Elapse Encode time: 3.699244
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 200.259792
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 203.959052
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 203959052436.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 1         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004775
-Preprocess time: 0.000015
-Decompose Order: 0.000006
-Encoding Graph Time: 0.005933
-Elapse Encode time: 3.663216
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 191.255302
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 194.918530
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 194918530006.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003849
-Preprocess time: 0.000013
-Decompose Order: 0.000004
-Encoding Graph Time: 0.005054
-Elapse Encode time: 3.650705
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 194.531983
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 198.182701
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 198182700896.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003755
-Preprocess time: 0.000012
-Decompose Order: 0.000004
-Encoding Graph Time: 0.077098
-Elapse Encode time: 0.163305
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 163.264840
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 163.428155
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 163428155146.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003749
-Preprocess time: 0.012392
-Decompose Order: 0.000007
-Encoding Graph Time: 0.078428
-Elapse Encode time: 0.176425
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 165.949550
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 166.125986
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 166125986333.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003869
-Preprocess time: 0.000013
-Decompose Order: 0.000004
-Encoding Graph Time: 0.076888
-Elapse Encode time: 0.162166
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 170.109839
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 170.272016
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 170272015757.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 4         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004817
-Preprocess time: 0.000020
-Decompose Order: 0.000004
-Encoding Graph Time: 0.078371
-Elapse Encode time: 0.164605
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 168.438953
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 168.603570
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 168603569572.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003824
-Preprocess time: 0.012402
-Decompose Order: 0.000008
-Encoding Graph Time: 0.076665
-Elapse Encode time: 0.182050
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 172.658556
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 172.840620
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 172840619808.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 0        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003732
-Preprocess time: 0.012341
-Decompose Order: 0.000007
-Encoding Graph Time: 0.038782
-Elapse Encode time: 1.084408
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 196.086515
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 197.170934
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 197170934389.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003798
-Preprocess time: 0.012459
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005163
-Elapse Encode time: 3.646471
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 196.787236
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 200.433720
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 200433720214.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 2         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003800
-Preprocess time: 0.012387
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005125
-Elapse Encode time: 3.736603
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 199.242297
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 202.978913
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 202978913249.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 1         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003796
-Preprocess time: 0.012289
-Decompose Order: 0.000008
-Encoding Graph Time: 0.005060
-Elapse Encode time: 3.702186
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 230.594846
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 234.297043
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 234297042838.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003742
-Preprocess time: 0.000014
-Decompose Order: 0.000004
-Encoding Graph Time: 0.005005
-Elapse Encode time: 3.657660
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 213.216063
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 216.873736
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 216873735962.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003802
-Preprocess time: 0.000014
-Decompose Order: 0.000004
-Encoding Graph Time: 0.005021
-Elapse Encode time: 3.666980
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 190.150496
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 193.817488
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 193817487748.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003708
-Preprocess time: 0.012303
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005073
-Elapse Encode time: 3.691539
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 190.448437
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 194.139991
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 194139990727.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 2         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003739
-Preprocess time: 0.012630
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005020
-Elapse Encode time: 3.672934
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 209.209322
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 212.882268
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 212882267611.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 5         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003949
-Preprocess time: 0.012802
-Decompose Order: 0.000008
-Encoding Graph Time: 0.005295
-Elapse Encode time: 3.687023
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 213.265444
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 216.952480
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 216952479581.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 1         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003912
-Preprocess time: 0.012691
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005183
-Elapse Encode time: 3.664000
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 232.840413
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 236.504427
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 236504426550.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 3         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003916
-Preprocess time: 0.012733
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005209
-Elapse Encode time: 3.735942
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 197.100228
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 200.836183
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 200836183201.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 5         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003979
-Preprocess time: 0.012754
-Decompose Order: 0.000008
-Encoding Graph Time: 0.005272
-Elapse Encode time: 3.688929
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 194.572067
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 198.261009
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 198261009074.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 0        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003906
-Preprocess time: 0.012603
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005185
-Elapse Encode time: 3.679947
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 195.583452
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 199.263412
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 199263412053.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 0        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003884
-Preprocess time: 0.012608
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005214
-Elapse Encode time: 3.673056
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 196.515939
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 200.189008
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 200189008299.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004310
-Preprocess time: 0.013806
-Decompose Order: 0.000008
-Encoding Graph Time: 0.005863
-Elapse Encode time: 3.672479
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 218.462610
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 222.135100
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 222135099600.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 4         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003947
-Preprocess time: 0.012763
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005078
-Elapse Encode time: 3.672946
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 216.175640
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 219.848599
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 219848599063.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003876
-Preprocess time: 0.012703
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005016
-Elapse Encode time: 3.681634
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 189.323384
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 193.005032
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 193005031629.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 4         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003947
-Preprocess time: 0.012753
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005069
-Elapse Encode time: 3.690430
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 213.451942
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 217.142385
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 217142384630.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003889
-Preprocess time: 0.012737
-Decompose Order: 0.000006
-Encoding Graph Time: 0.077964
-Elapse Encode time: 0.175904
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 168.975013
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 169.150954
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 169150954004.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003954
-Preprocess time: 0.000011
-Decompose Order: 0.000003
-Encoding Graph Time: 0.078389
-Elapse Encode time: 0.163362
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 162.638351
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 162.801724
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 162801723981.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003933
-Preprocess time: 0.012814
-Decompose Order: 0.000007
-Encoding Graph Time: 0.077829
-Elapse Encode time: 0.175715
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 167.368509
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 167.544236
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 167544235684.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 0        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003915
-Preprocess time: 0.012472
-Decompose Order: 0.000008
-Encoding Graph Time: 0.038816
-Elapse Encode time: 1.084491
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 157.594607
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 158.679111
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 158679110536.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 3         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003909
-Preprocess time: 0.012711
-Decompose Order: 0.000007
-Encoding Graph Time: 0.039867
-Elapse Encode time: 1.087709
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 196.644086
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 197.731808
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 197731807552.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003935
-Preprocess time: 0.012286
-Decompose Order: 0.000008
-Encoding Graph Time: 0.005066
-Elapse Encode time: 3.692239
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 212.237224
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 215.929477
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 215929476801.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003914
-Preprocess time: 0.012774
-Decompose Order: 0.000007
-Encoding Graph Time: 0.077064
-Elapse Encode time: 0.175014
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 163.079861
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 163.254888
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 163254887957.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 0        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003723
-Preprocess time: 0.012345
-Decompose Order: 0.000007
-Encoding Graph Time: 0.038708
-Elapse Encode time: 1.086417
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 173.854583
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 174.941041
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 174941041047.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003894
-Preprocess time: 0.012772
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005053
-Elapse Encode time: 3.645309
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 193.549004
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 197.194326
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 197194326176.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003943
-Preprocess time: 0.012657
-Decompose Order: 0.000008
-Encoding Graph Time: 0.039015
-Elapse Encode time: 1.086697
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 170.687788
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 171.774497
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 171774497026.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 4         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003915
-Preprocess time: 0.012660
-Decompose Order: 0.000006
-Encoding Graph Time: 0.038827
-Elapse Encode time: 1.091702
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 211.483507
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 212.575221
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 212575220713.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003908
-Preprocess time: 0.000011
-Decompose Order: 0.000003
-Encoding Graph Time: 0.040577
-Elapse Encode time: 1.075268
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 175.800611
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 176.875891
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 176875890670.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003938
-Preprocess time: 0.012794
-Decompose Order: 0.000008
-Encoding Graph Time: 0.038757
-Elapse Encode time: 1.091536
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 186.924864
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 188.016412
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 188016412411.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003900
-Preprocess time: 0.012565
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005207
-Elapse Encode time: 3.682209
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 192.647723
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 196.329945
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 196329945231.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003941
-Preprocess time: 0.012756
-Decompose Order: 0.000037
-Encoding Graph Time: 0.038824
-Elapse Encode time: 1.083426
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 179.833990
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 180.917429
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 180917428919.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003811
-Preprocess time: 0.012519
-Decompose Order: 0.000007
-Encoding Graph Time: 0.079074
-Elapse Encode time: 0.176448
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 170.526937
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 170.703396
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 170703395848.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003958
-Preprocess time: 0.012776
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005126
-Elapse Encode time: 3.666501
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 199.348463
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 203.014978
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 203014977559.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003882
-Preprocess time: 0.000010
-Decompose Order: 0.000003
-Encoding Graph Time: 0.077627
-Elapse Encode time: 0.162374
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000001
-SAT Solving time: 167.578118
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 167.740504
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 167740503520.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003840
-Preprocess time: 0.000011
-Decompose Order: 0.000004
-Encoding Graph Time: 0.004883
-Elapse Encode time: 3.645558
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 202.727908
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 206.373478
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 206373478044.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003943
-Preprocess time: 0.012472
-Decompose Order: 0.000007
-Encoding Graph Time: 0.076030
-Elapse Encode time: 0.173739
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 164.271451
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 164.445200
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 164445200208.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003937
-Preprocess time: 0.012865
-Decompose Order: 0.000009
-Encoding Graph Time: 0.005197
-Elapse Encode time: 3.736503
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 194.532342
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 198.268858
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 198268858437.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003731
-Preprocess time: 0.012372
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005044
-Elapse Encode time: 3.673733
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 195.935119
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 199.608864
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 199608864374.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003797
-Preprocess time: 0.000014
-Decompose Order: 0.000005
-Encoding Graph Time: 0.005054
-Elapse Encode time: 3.657081
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 187.706833
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 191.363926
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 191363925511.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 3         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003741
-Preprocess time: 0.000013
-Decompose Order: 0.000004
-Encoding Graph Time: 0.005019
-Elapse Encode time: 3.656541
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 188.132679
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 191.789232
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 191789231675.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 2         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003762
-Preprocess time: 0.000014
-Decompose Order: 0.000004
-Encoding Graph Time: 0.005036
-Elapse Encode time: 3.622179
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 200.267486
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 203.889678
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 203889677771.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 0        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003778
-Preprocess time: 0.000014
-Decompose Order: 0.000004
-Encoding Graph Time: 0.005054
-Elapse Encode time: 3.682708
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 176.876994
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 180.559715
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 180559715113.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003776
-Preprocess time: 0.000014
-Decompose Order: 0.000004
-Encoding Graph Time: 0.039241
-Elapse Encode time: 1.071814
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 179.120002
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 180.191829
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 180191828542.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 3         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003753
-Preprocess time: 0.000014
-Decompose Order: 0.000005
-Encoding Graph Time: 0.038972
-Elapse Encode time: 1.077591
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 173.747742
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 174.825345
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 174825345064.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003741
-Preprocess time: 0.012412
-Decompose Order: 0.000007
-Encoding Graph Time: 0.038641
-Elapse Encode time: 1.083641
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 197.424468
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 198.508122
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 198508121760.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003766
-Preprocess time: 0.000014
-Decompose Order: 0.000004
-Encoding Graph Time: 0.077172
-Elapse Encode time: 0.162511
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 165.982214
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 166.144737
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 166144736612.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 4         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003798
-Preprocess time: 0.000012
-Decompose Order: 0.000004
-Encoding Graph Time: 0.078314
-Elapse Encode time: 0.163238
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 167.105501
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 167.268750
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 167268749810.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003741
-Preprocess time: 0.012401
-Decompose Order: 0.000006
-Encoding Graph Time: 0.076291
-Elapse Encode time: 0.178145
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 168.574659
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 168.752816
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 168752815677.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003763
-Preprocess time: 0.000012
-Decompose Order: 0.000005
-Encoding Graph Time: 0.076082
-Elapse Encode time: 0.160938
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 165.394703
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 165.555651
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 165555651137.000000
-Best tuner:
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 156357122315.000000

diff --git a/src/2.log b/src/2.log
deleted file mode 100644 (file)
index d57ea60..0000000
--- a/src/2.log
+++ /dev/null
@@ -1,2018 +0,0 @@
-deserializing ...
-**********************
-Polarity time: 0.003698
-Preprocess time: 0.011524
-Decompose Order: 0.000017
-Encoding Graph Time: 0.037881
-Elapse Encode time: 0.997790
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000001
-SAT Solving time: 22.486690
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 23.484500
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004408
-Preprocess time: 0.015162
-Decompose Order: 0.000007
-Encoding Graph Time: 0.075089
-Elapse Encode time: 0.170877
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 83.681346
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 83.852230
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 83852230129.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004306
-Preprocess time: 0.000012
-Decompose Order: 0.000003
-Encoding Graph Time: 0.041191
-Elapse Encode time: 0.993668
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 87.561080
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 88.554759
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 88554759182.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004242
-Preprocess time: 0.014907
-Decompose Order: 0.000006
-Encoding Graph Time: 0.005495
-Elapse Encode time: 3.395448
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 59.817873
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 63.213332
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 63213332241.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 5         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004321
-Preprocess time: 0.015034
-Decompose Order: 0.000006
-Encoding Graph Time: 0.041278
-Elapse Encode time: 1.011671
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 89.444982
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 90.456664
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 90456664442.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003616
-Preprocess time: 0.000013
-Decompose Order: 0.000004
-Encoding Graph Time: 0.036958
-Elapse Encode time: 0.991289
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 30.786825
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 31.778125
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 31778124877.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004231
-Preprocess time: 0.014832
-Decompose Order: 0.000007
-Encoding Graph Time: 0.039483
-Elapse Encode time: 1.005092
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 31.087874
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 32.092977
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 32092977155.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 3         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004257
-Preprocess time: 0.014958
-Decompose Order: 0.000007
-Encoding Graph Time: 0.041401
-Elapse Encode time: 1.008422
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 30.392583
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 31.401015
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 31401015378.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004297
-Preprocess time: 0.014887
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005476
-Elapse Encode time: 3.399174
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 105.910181
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 109.309367
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 109309366995.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 5         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004377
-Preprocess time: 0.015036
-Decompose Order: 0.000007
-Encoding Graph Time: 0.041241
-Elapse Encode time: 1.013063
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 40.816514
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 41.829587
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 41829587127.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004338
-Preprocess time: 0.015042
-Decompose Order: 0.000006
-Encoding Graph Time: 0.005625
-Elapse Encode time: 3.407410
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 83.632609
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 87.040030
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 87040029909.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004251
-Preprocess time: 0.014971
-Decompose Order: 0.000007
-Encoding Graph Time: 0.074759
-Elapse Encode time: 0.169985
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 83.095377
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 83.265372
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 83265371895.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003756
-Preprocess time: 0.000011
-Decompose Order: 0.000004
-Encoding Graph Time: 0.038465
-Elapse Encode time: 0.991921
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 41.302063
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 42.293995
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 42293995203.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004323
-Preprocess time: 0.000015
-Decompose Order: 0.000003
-Encoding Graph Time: 0.074547
-Elapse Encode time: 0.157879
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 81.915438
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 82.073324
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 82073324225.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 1         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004248
-Preprocess time: 0.000014
-Decompose Order: 0.000004
-Encoding Graph Time: 0.041180
-Elapse Encode time: 0.995260
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 26.421098
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 27.416369
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 27416368661.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004342
-Preprocess time: 0.000014
-Decompose Order: 0.000003
-Encoding Graph Time: 0.005481
-Elapse Encode time: 3.371583
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 85.153587
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 88.525182
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 88525181902.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004275
-Preprocess time: 0.000013
-Decompose Order: 0.000003
-Encoding Graph Time: 0.005308
-Elapse Encode time: 3.380358
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 87.043549
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 90.423918
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 90423918219.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 2         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004281
-Preprocess time: 0.000014
-Decompose Order: 0.000003
-Encoding Graph Time: 0.041230
-Elapse Encode time: 0.991263
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 52.397527
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 53.388801
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 53388800680.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004273
-Preprocess time: 0.000013
-Decompose Order: 0.000004
-Encoding Graph Time: 0.074555
-Elapse Encode time: 0.154938
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 83.008266
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 83.163213
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 83163213105.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003818
-Preprocess time: 0.011169
-Decompose Order: 0.000006
-Encoding Graph Time: 0.070034
-Elapse Encode time: 0.159874
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 82.624972
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 82.784855
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 82784854843.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 0        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004343
-Preprocess time: 0.015029
-Decompose Order: 0.000007
-Encoding Graph Time: 0.041378
-Elapse Encode time: 1.007336
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 31.199024
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 32.206371
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 32206370553.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004382
-Preprocess time: 0.000015
-Decompose Order: 0.000003
-Encoding Graph Time: 0.041151
-Elapse Encode time: 0.993579
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 20.294117
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 21.287706
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 21287706291.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003636
-Preprocess time: 0.000013
-Decompose Order: 0.000003
-Encoding Graph Time: 0.070066
-Elapse Encode time: 0.148509
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 83.965949
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 84.114467
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 84114467261.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003609
-Preprocess time: 0.011215
-Decompose Order: 0.000007
-Encoding Graph Time: 0.037147
-Elapse Encode time: 0.998892
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 30.748693
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 31.747596
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 31747596132.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004389
-Preprocess time: 0.015054
-Decompose Order: 0.000007
-Encoding Graph Time: 0.074696
-Elapse Encode time: 0.170195
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 82.414739
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 82.584943
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 82584943418.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004320
-Preprocess time: 0.014481
-Decompose Order: 0.000007
-Encoding Graph Time: 0.004594
-Elapse Encode time: 3.396318
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 85.187796
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 88.584126
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 88584125805.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004375
-Preprocess time: 0.015001
-Decompose Order: 0.000006
-Encoding Graph Time: 0.005633
-Elapse Encode time: 3.389372
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 87.848146
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 91.237530
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 91237529526.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004391
-Preprocess time: 0.000014
-Decompose Order: 0.000004
-Encoding Graph Time: 0.037852
-Elapse Encode time: 0.992423
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 61.716614
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 62.709048
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 62709047878.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004286
-Preprocess time: 0.000015
-Decompose Order: 0.000003
-Encoding Graph Time: 0.043198
-Elapse Encode time: 0.995987
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 5.946959
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 6.942956
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 6942956251.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004261
-Preprocess time: 0.000013
-Decompose Order: 0.000004
-Encoding Graph Time: 0.005362
-Elapse Encode time: 3.384706
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 112.144277
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 115.528994
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 115528994215.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004353
-Preprocess time: 0.015062
-Decompose Order: 0.000006
-Encoding Graph Time: 0.041410
-Elapse Encode time: 1.007912
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 30.765756
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 31.773680
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 31773679622.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 2         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004336
-Preprocess time: 0.000013
-Decompose Order: 0.000003
-Encoding Graph Time: 0.041225
-Elapse Encode time: 0.995415
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 8.564521
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 9.559946
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 9559946211.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004269
-Preprocess time: 0.000015
-Decompose Order: 0.000003
-Encoding Graph Time: 0.005307
-Elapse Encode time: 3.382184
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 89.076015
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 92.458210
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 92458209983.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 4         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003616
-Preprocess time: 0.000015
-Decompose Order: 0.000004
-Encoding Graph Time: 0.037030
-Elapse Encode time: 0.988529
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 30.816409
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 31.804950
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 31804949698.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003637
-Preprocess time: 0.000016
-Decompose Order: 0.000003
-Encoding Graph Time: 0.004500
-Elapse Encode time: 3.381605
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 105.624640
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 109.006257
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 109006257268.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003609
-Preprocess time: 0.000015
-Decompose Order: 0.000003
-Encoding Graph Time: 0.070066
-Elapse Encode time: 0.148246
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 83.017586
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 83.165841
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 83165841166.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003793
-Preprocess time: 0.011294
-Decompose Order: 0.000007
-Encoding Graph Time: 0.037214
-Elapse Encode time: 1.004501
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 40.405115
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 41.409626
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 41409625928.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003628
-Preprocess time: 0.000016
-Decompose Order: 0.000004
-Encoding Graph Time: 0.070005
-Elapse Encode time: 0.148406
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 82.673455
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 82.821879
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 82821878812.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003589
-Preprocess time: 0.000015
-Decompose Order: 0.000004
-Encoding Graph Time: 0.069845
-Elapse Encode time: 0.148089
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 82.260363
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 82.408461
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 82408461414.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003662
-Preprocess time: 0.011214
-Decompose Order: 0.000008
-Encoding Graph Time: 0.037162
-Elapse Encode time: 1.000221
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 63.581372
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 64.581604
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 64581603603.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003630
-Preprocess time: 0.000014
-Decompose Order: 0.000004
-Encoding Graph Time: 0.072271
-Elapse Encode time: 0.150898
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 82.865470
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 83.016377
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 83016377277.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003621
-Preprocess time: 0.000015
-Decompose Order: 0.000004
-Encoding Graph Time: 0.069953
-Elapse Encode time: 0.148476
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 84.333331
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 84.481840
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 84481839508.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 3         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003643
-Preprocess time: 0.000014
-Decompose Order: 0.000003
-Encoding Graph Time: 0.036907
-Elapse Encode time: 0.985214
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 31.198388
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 32.183612
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 32183612381.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 1         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003617
-Preprocess time: 0.000014
-Decompose Order: 0.000003
-Encoding Graph Time: 0.037008
-Elapse Encode time: 0.990691
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 8.581465
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 9.572166
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 9572165776.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003619
-Preprocess time: 0.000013
-Decompose Order: 0.000003
-Encoding Graph Time: 0.069792
-Elapse Encode time: 0.148374
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 82.737560
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 82.885944
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 82885943714.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003604
-Preprocess time: 0.000013
-Decompose Order: 0.000003
-Encoding Graph Time: 0.004465
-Elapse Encode time: 3.380603
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 87.755807
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 91.136419
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 91136419414.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003638
-Preprocess time: 0.011222
-Decompose Order: 0.000006
-Encoding Graph Time: 0.037182
-Elapse Encode time: 1.000609
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 33.460618
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 34.461239
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 34461238672.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003627
-Preprocess time: 0.011277
-Decompose Order: 0.000006
-Encoding Graph Time: 0.037141
-Elapse Encode time: 1.000240
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 62.286329
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 63.286580
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 63286579834.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 4         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003603
-Preprocess time: 0.000013
-Decompose Order: 0.000004
-Encoding Graph Time: 0.036952
-Elapse Encode time: 0.989766
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 41.587196
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 42.576994
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 42576994380.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003607
-Preprocess time: 0.011245
-Decompose Order: 0.000007
-Encoding Graph Time: 0.037129
-Elapse Encode time: 0.999497
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 8.630406
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 9.629913
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 9629913404.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003554
-Preprocess time: 0.011257
-Decompose Order: 0.000006
-Encoding Graph Time: 0.070039
-Elapse Encode time: 0.159810
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 83.135095
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 83.294914
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 83294914257.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003584
-Preprocess time: 0.011227
-Decompose Order: 0.000007
-Encoding Graph Time: 0.004614
-Elapse Encode time: 3.385892
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 49.465540
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 52.851444
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 52851443742.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 3         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003613
-Preprocess time: 0.011217
-Decompose Order: 0.000006
-Encoding Graph Time: 0.037257
-Elapse Encode time: 1.000259
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 30.583907
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 31.584177
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 31584177331.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 2         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003614
-Preprocess time: 0.011239
-Decompose Order: 0.000006
-Encoding Graph Time: 0.037056
-Elapse Encode time: 0.997787
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 20.157703
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 21.155500
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 21155500433.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003621
-Preprocess time: 0.000013
-Decompose Order: 0.000004
-Encoding Graph Time: 0.036958
-Elapse Encode time: 0.988231
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 8.732493
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 9.720734
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 9720733973.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003620
-Preprocess time: 0.000015
-Decompose Order: 0.000029
-Encoding Graph Time: 0.069906
-Elapse Encode time: 0.148470
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 82.287290
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 82.435769
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 82435769331.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003585
-Preprocess time: 0.011204
-Decompose Order: 0.000007
-Encoding Graph Time: 0.037049
-Elapse Encode time: 0.997449
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 33.548497
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 34.545956
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 34545955994.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 1         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003584
-Preprocess time: 0.011194
-Decompose Order: 0.000006
-Encoding Graph Time: 0.037103
-Elapse Encode time: 0.996823
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 68.995219
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 69.992053
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 69992053363.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 5         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003595
-Preprocess time: 0.011199
-Decompose Order: 0.000006
-Encoding Graph Time: 0.037157
-Elapse Encode time: 0.998137
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 41.424740
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 42.422888
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 42422888244.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 1         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004368
-Preprocess time: 0.015122
-Decompose Order: 0.000006
-Encoding Graph Time: 0.041379
-Elapse Encode time: 1.006678
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 33.812083
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 34.818771
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 34818770810.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 3         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003610
-Preprocess time: 0.011172
-Decompose Order: 0.000007
-Encoding Graph Time: 0.037203
-Elapse Encode time: 0.997866
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 27.557825
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 28.555701
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 28555701251.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 5         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004360
-Preprocess time: 0.015019
-Decompose Order: 0.000006
-Encoding Graph Time: 0.038774
-Elapse Encode time: 1.004089
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 63.353451
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 64.357551
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 64357550500.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004250
-Preprocess time: 0.014777
-Decompose Order: 0.000006
-Encoding Graph Time: 0.074700
-Elapse Encode time: 0.169764
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 86.908366
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 87.078139
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 87078139342.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004352
-Preprocess time: 0.014943
-Decompose Order: 0.000006
-Encoding Graph Time: 0.074774
-Elapse Encode time: 0.169911
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 86.319313
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 86.489234
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 86489233627.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003597
-Preprocess time: 0.011123
-Decompose Order: 0.000007
-Encoding Graph Time: 0.070011
-Elapse Encode time: 0.159512
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 82.454700
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 82.614221
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 82614221500.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 5         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003651
-Preprocess time: 0.011092
-Decompose Order: 0.000006
-Encoding Graph Time: 0.037092
-Elapse Encode time: 1.000286
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 71.853457
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 72.853754
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 72853753763.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003643
-Preprocess time: 0.011101
-Decompose Order: 0.000006
-Encoding Graph Time: 0.070230
-Elapse Encode time: 0.159777
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 84.719625
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 84.879412
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 84879411582.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 5         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003634
-Preprocess time: 0.011164
-Decompose Order: 0.000007
-Encoding Graph Time: 0.037201
-Elapse Encode time: 0.997829
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 51.114738
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 52.112578
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 52112578141.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003674
-Preprocess time: 0.011182
-Decompose Order: 0.000007
-Encoding Graph Time: 0.004689
-Elapse Encode time: 3.383206
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 114.611367
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 117.994583
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 117994582967.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003620
-Preprocess time: 0.000014
-Decompose Order: 0.000004
-Encoding Graph Time: 0.036837
-Elapse Encode time: 0.985972
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 46.478543
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 47.464525
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 47464524931.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003605
-Preprocess time: 0.000016
-Decompose Order: 0.000003
-Encoding Graph Time: 0.036873
-Elapse Encode time: 0.986315
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 40.200536
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 41.186862
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 41186862150.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003663
-Preprocess time: 0.011276
-Decompose Order: 0.000007
-Encoding Graph Time: 0.070148
-Elapse Encode time: 0.159843
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 82.375232
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 82.535086
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 82535085668.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 4         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003602
-Preprocess time: 0.011101
-Decompose Order: 0.000006
-Encoding Graph Time: 0.037077
-Elapse Encode time: 0.999875
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 14.009753
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 15.009639
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 15009639361.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003622
-Preprocess time: 0.011201
-Decompose Order: 0.000006
-Encoding Graph Time: 0.004631
-Elapse Encode time: 3.384540
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 75.543617
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 78.928167
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 78928166995.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003579
-Preprocess time: 0.011312
-Decompose Order: 0.000008
-Encoding Graph Time: 0.070124
-Elapse Encode time: 0.159894
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 82.061831
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 82.221734
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 82221734235.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003551
-Preprocess time: 0.011259
-Decompose Order: 0.000007
-Encoding Graph Time: 0.070051
-Elapse Encode time: 0.159558
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 82.256872
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 82.416439
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 82416439048.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003593
-Preprocess time: 0.011235
-Decompose Order: 0.000007
-Encoding Graph Time: 0.004582
-Elapse Encode time: 3.389657
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 16.307972
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 19.697641
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 19697640893.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003576
-Preprocess time: 0.011259
-Decompose Order: 0.000006
-Encoding Graph Time: 0.004639
-Elapse Encode time: 3.385306
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 16.035999
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 19.421316
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 19421316493.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 5         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003565
-Preprocess time: 0.011196
-Decompose Order: 0.000007
-Encoding Graph Time: 0.004553
-Elapse Encode time: 3.386017
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 32.369498
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 35.755526
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 5         range=[1,5]
-Received score 35755525576.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003605
-Preprocess time: 0.000016
-Decompose Order: 0.000004
-Encoding Graph Time: 0.004501
-Elapse Encode time: 3.374840
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 108.432511
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 111.807363
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 111807362878.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003596
-Preprocess time: 0.000015
-Decompose Order: 0.000003
-Encoding Graph Time: 0.004528
-Elapse Encode time: 3.372506
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 61.460759
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 64.833276
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 64833276115.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003583
-Preprocess time: 0.011129
-Decompose Order: 0.000006
-Encoding Graph Time: 0.037114
-Elapse Encode time: 0.997624
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 26.648506
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 27.646141
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 27646140703.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003623
-Preprocess time: 0.011095
-Decompose Order: 0.000006
-Encoding Graph Time: 0.037181
-Elapse Encode time: 1.000318
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 71.175752
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 72.176080
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 72176079940.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 1        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003619
-Preprocess time: 0.011116
-Decompose Order: 0.000006
-Encoding Graph Time: 0.004639
-Elapse Encode time: 3.385965
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 16.013478
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 19.399454
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 19399453559.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003562
-Preprocess time: 0.011236
-Decompose Order: 0.000006
-Encoding Graph Time: 0.070376
-Elapse Encode time: 0.160124
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 83.829085
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 83.989220
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 83989219554.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003630
-Preprocess time: 0.000014
-Decompose Order: 0.000004
-Encoding Graph Time: 0.004486
-Elapse Encode time: 3.382889
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 15.896570
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 19.279470
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 19279470399.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003534
-Preprocess time: 0.000015
-Decompose Order: 0.000003
-Encoding Graph Time: 0.069747
-Elapse Encode time: 0.148181
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 82.512962
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 82.661153
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 82661152628.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003597
-Preprocess time: 0.011241
-Decompose Order: 0.000006
-Encoding Graph Time: 0.004552
-Elapse Encode time: 3.390503
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 16.391724
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 19.782237
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 19782237090.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003606
-Preprocess time: 0.011243
-Decompose Order: 0.000006
-Encoding Graph Time: 0.069991
-Elapse Encode time: 0.159843
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 82.459144
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 82.618996
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 82618995928.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003619
-Preprocess time: 0.011217
-Decompose Order: 0.000007
-Encoding Graph Time: 0.069986
-Elapse Encode time: 0.159895
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 82.789035
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 82.948966
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 82948965952.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003641
-Preprocess time: 0.000014
-Decompose Order: 0.000004
-Encoding Graph Time: 0.004493
-Elapse Encode time: 3.379458
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 16.152344
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 19.531813
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 19531813164.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 3         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003615
-Preprocess time: 0.000014
-Decompose Order: 0.000003
-Encoding Graph Time: 0.004428
-Elapse Encode time: 3.388834
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 94.074652
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 97.463497
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 97463497348.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 2         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003597
-Preprocess time: 0.000014
-Decompose Order: 0.000003
-Encoding Graph Time: 0.004440
-Elapse Encode time: 3.379140
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 71.074409
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 74.453559
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 74453559426.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 0        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004336
-Preprocess time: 0.000022
-Decompose Order: 0.000004
-Encoding Graph Time: 0.005427
-Elapse Encode time: 3.380403
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 86.655901
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 90.036315
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 90036314667.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPT = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004355
-Preprocess time: 0.000016
-Decompose Order: 0.000003
-Encoding Graph Time: 0.074442
-Elapse Encode time: 0.154603
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 82.257309
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 82.411922
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 82411922080.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 2         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004289
-Preprocess time: 0.000014
-Decompose Order: 0.000003
-Encoding Graph Time: 0.005336
-Elapse Encode time: 3.391593
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 87.475675
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 90.867278
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 2         range=[1,5]
-Received score 90867278483.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.003639
-Preprocess time: 0.011204
-Decompose Order: 0.000006
-Encoding Graph Time: 0.004632
-Elapse Encode time: 3.383923
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 16.068230
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 19.452165
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 19452165317.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param ELEMENTOPTSETS = 0        range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004319
-Preprocess time: 0.014972
-Decompose Order: 0.000007
-Encoding Graph Time: 0.005565
-Elapse Encode time: 3.398950
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 59.972419
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 63.371381
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 63371380931.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PROXYVARIABLE = 3         range=[1,5]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004375
-Preprocess time: 0.015001
-Decompose Order: 0.000006
-Encoding Graph Time: 0.005624
-Elapse Encode time: 3.401645
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 72.692053
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 76.093709
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 3         range=[1,5]
-Received score 76093708689.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 0    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004366
-Preprocess time: 0.000014
-Decompose Order: 0.000004
-Encoding Graph Time: 0.005468
-Elapse Encode time: 3.380701
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 15.878807
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 19.259520
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 19259520074.000000
-Mutating 1 settings
-&&&&&&&&Mutating&&&&&&&
-Param PREPROCESS = 1    range=[0,1]
-&&&&&&&&&&&&&&&&&&&&&&&
-**********************
-Polarity time: 0.004352
-Preprocess time: 0.015053
-Decompose Order: 0.000006
-Encoding Graph Time: 0.005608
-Elapse Encode time: 3.403785
-Is problem UNSAT after encoding: 0
-CNF Encode time: 0.000000
-SAT Solving time: 71.899633
-Result Computed in SAT solver: SAT
-CSOLVER solve time: 75.303430
-Param PREPROCESS = 1    range=[0,1]
-Param ELEMENTOPTSETS = 1        range=[0,1]
-Param ELEMENTOPT = 0    range=[0,1]
-Param PROXYVARIABLE = 4         range=[1,5]
-Received score 75303429567.000000
-Best tuner:
-Param PREPROCESS = 0    range=[0,1]
-Param ELEMENTOPTSETS = 0        range=[0,1]
-Param ELEMENTOPT = 1    range=[0,1]
-Param PROXYVARIABLE = 1         range=[1,5]
-Received score 6942956251.000000

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index 2ac69c1de22ddbedb684e04eb44cc51cc76e61f4..957fea33ba4818cd67e98a88e66f839c8293a98e 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -113,8 +113,11 @@ void EncodingGraph::validate() {
 
 
 void EncodingGraph::encode() {
+       if (solver->getTuner()->getTunable(ENCODINGGRAPHOPT, &offon) == 0)
+               return;
+       buildGraph();
        SetIteratorEncodingSubGraph *itesg = subgraphs.iterator();
-       model_print("#SubGraph = %u", subgraphs.getSize());
+       model_print("#SubGraph = %u\n", subgraphs.getSize());
        while (itesg->hasNext()) {
                EncodingSubGraph *sg = itesg->next();
                sg->encode();
@@ -155,9 +158,6 @@ void EncodingGraph::encode() {
                                                ASSERT(encoding->isinUseElement(encodingIndex));
                                                encoding->encodingArray[encodingIndex] = value;
                                        }
-                               } else {
-                                       model_print("DAMN in encode()\n");
-                                       e->print();
                                }
                        }
                        break;
@@ -333,58 +333,36 @@ void EncodingGraph::decideEdges() {
                        EncodingNode *tmp = left; left = right; right = tmp;
                        EncodingSubGraph *tmpsg = leftGraph; leftGraph = rightGraph; rightGraph = tmpsg;
                }
-               //model_print("Right=%p RGraph=%p\tLeft=%p LGraph=%p\n", right, rightGraph, left, leftGraph);
-               uint leftSize = 0, rightSize = 0, newSize = 0, max = 0;
-               uint64_t totalCost = 0;
+               
+               uint leftSize = 0, rightSize = 0, newSize = 0, max=0;
                bool merge = false;
-//             model_print("**************decideEdge*************\n");
-//             model_print("LeftNode Size = %u\n", left->getSize());
-//             model_print("rightNode Size = %u\n", right->getSize());
-//             model_print("UnionSize = %u\n", left->s->getUnionSize(right->s));
-
                if (leftGraph == NULL && rightGraph == NULL) {
                        leftSize = convertSize(left->getSize());
                        rightSize = convertSize(right->getSize());
                        newSize = convertSize(left->s->getUnionSize(right->s));
                        newSize = (leftSize > newSize) ? leftSize : newSize;
                        newSize = (rightSize > newSize) ? rightSize : newSize;
-                       totalCost = (newSize - leftSize) * left->elements.getSize() +
-                                                                       (newSize - rightSize) * right->elements.getSize();
-                       //model_print("leftSize=%u\trighSize=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
-                       max = rightSize > leftSize ? rightSize : leftSize;
-                       if (newSize == max) {
-                               merge = true;
-                       }
                } else if (leftGraph != NULL && rightGraph == NULL) {
                        leftSize = convertSize(leftGraph->encodingSize);
                        rightSize = convertSize(right->getSize());
                        newSize = convertSize(leftGraph->estimateNewSize(right));
                        newSize = (leftSize > newSize) ? leftSize : newSize;
                        newSize = (rightSize > newSize) ? rightSize : newSize;
-                       totalCost = (newSize - leftSize) * leftGraph->numElements +
-                                                                       (newSize - rightSize) * right->elements.getSize();
-                       //model_print("leftSize=%u\trighSize=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
-                       max = rightSize > leftSize ? rightSize : leftSize;
-                       if (newSize == max) {
-                               merge = true;
-                       }
+                       max = rightSize > leftSize? rightSize : leftSize;
+//                     model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", left->measureSimilarity(right));
+                       merge = left->measureSimilarity(right) > 1.5 || max == newSize;
                } else {
                        //Neither are null
                        leftSize = convertSize(leftGraph->encodingSize);
                        rightSize = convertSize(rightGraph->encodingSize);
                        newSize = convertSize(leftGraph->estimateNewSize(rightGraph));
+//                     model_print("MergingSubGraphs: left=%u\tright=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
                        newSize = (leftSize > newSize) ? leftSize : newSize;
                        newSize = (rightSize > newSize) ? rightSize : newSize;
-                       totalCost = (newSize - leftSize) * leftGraph->numElements +
-                                                                       (newSize - rightSize) * rightGraph->numElements;
-//                     model_print("LeftGraph size=%u\n", leftGraph->encodingSize);
-//                     model_print("RightGraph size=%u\n", rightGraph->encodingSize);
-//                     model_print("UnionGraph size = %u\n", leftGraph->estimateNewSize(rightGraph));
-                       if (rightSize < 64 && leftSize < 64) {
-                               merge = true;
-                       }
+                       max = rightSize > leftSize? rightSize : leftSize;
+//                     model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", leftGraph->measureSimilarity(right));
+                       merge = leftGraph->measureSimilarity(right) > 1.5 || max == newSize;
                }
-//             model_print("******************************\n");
                if (merge) {
                        //add the edge
                        mergeNodes(left, right);
@@ -441,11 +419,33 @@ uint EncodingNode::getSize() const {
        return s->getSize();
 }
 
+uint64_t EncodingNode::getIndex(uint index){
+       return s->getElement(index);
+}
+
 VarType EncodingNode::getType() const {
        return s->getType();
 }
 
-static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
+bool EncodingNode::itemExists(uint64_t item){
+       for(uint i=0; i< s->getSize(); i++){
+               if(item == s->getElement(i))
+                       return true;
+       }
+       return false;
+}
+
+double EncodingNode::measureSimilarity(EncodingNode *node){
+       uint common = 0;
+       for(uint i=0; i < s->getSize(); i++){
+               uint64_t item = s->getElement(i);
+               if(node->itemExists(item)){
+                       common++;
+               }
+       }
+//     model_print("common=%u\tsize1=%u\tsize2=%u\tsim1=%f\tsim2=%f\n", common, s->getSize(), node->getSize(), 1.0*common/s->getSize(), 1.0*common/node->getSize());
+       return common*1.0/s->getSize() + common*1.0/node->getSize();
+}
 
 EncodingNode *EncodingGraph::createNode(Element *e) {
        if (e->type == ELEMCONST)

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.h b/src/ASTAnalyses/Encoding/encodinggraph.h
index d284d2149bf3b53e914587d956a64e20c3f1806e..ae330b853dcedca2cbeafa0f804c513a56de258a 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.h
+++ b/src/ASTAnalyses/Encoding/encodinggraph.h
@@ -42,9 +42,12 @@ public:
        EncodingNode(Set *_s);
        void addElement(Element *e);
        uint getSize() const;
+       uint64_t getIndex(uint index);
        VarType getType() const;
+        double measureSimilarity(EncodingNode *node);
        void setEncoding(ElementEncodingType e) {encoding = e;}
        ElementEncodingType getEncoding() {return encoding;}
+        bool itemExists(uint64_t item);
        bool couldBeBinaryIndex() {return encoding == BINARYINDEX || encoding == ELEM_UNASSIGNED;}
        CMEMALLOC;
 private:

diff --git a/src/ASTAnalyses/Encoding/subgraph.cc b/src/ASTAnalyses/Encoding/subgraph.cc
index f99783e42410e63fda746d12cfb3e74dc4694c2a..de76e4d0e6890d149fd703795f3713dc455ad3be 100644 (file)
--- a/src/ASTAnalyses/Encoding/subgraph.cc
+++ b/src/ASTAnalyses/Encoding/subgraph.cc
@@ -121,6 +121,58 @@ uint EncodingSubGraph::estimateNewSize(EncodingSubGraph *sg) {
        return newSize;
 }
 
+double EncodingSubGraph::measureSimilarity(EncodingNode *node) {
+       uint common = 0;
+       Hashset64Int intSet;
+       SetIteratorEncodingNode *nit = nodes.iterator();
+       while (nit->hasNext()) {
+               EncodingNode *en = nit->next();
+               for(uint i=0; i < en->getSize(); i++){
+                       intSet.add(en->getIndex(i));
+               }
+       }
+       for(uint i=0; i < node->getSize(); i++){
+               if(intSet.contains( node->getIndex(i) )){
+                       common++;
+               }
+       }
+//     model_print("measureSimilarity:139: common=%u\t GraphSize=%u\tnodeSize=%u\tGraphSim=%f\tnodeSim=%f\n", common, intSet.getSize(), node->getSize(), 1.0*common/intSet.getSize(), 1.0*common/node->getSize());
+       delete nit;
+       return common*1.0/intSet.getSize() + common*1.0/node->getSize();
+}
+
+double EncodingSubGraph::measureSimilarity(EncodingSubGraph *sg) {
+       uint common = 0;
+       Hashset64Int set1;
+       Hashset64Int set2;
+       SetIteratorEncodingNode *nit = nodes.iterator();
+       while (nit->hasNext()) {
+               EncodingNode *en = nit->next();
+               for(uint i=0; i < en->getSize(); i++){
+                       set1.add(en->getIndex(i));
+               }
+       }
+       delete nit;
+       nit = sg->nodes.iterator();
+       while (nit->hasNext()) {
+               EncodingNode *en = nit->next();
+               for(uint i=0; i < en->getSize(); i++){
+                       set2.add(en->getIndex(i));
+               }
+       }
+       delete nit;
+       SetIterator64Int *setIter1 = set1.iterator();
+       while(setIter1->hasNext()){
+               uint64_t item1 = setIter1->next();
+               if( set2.contains(item1)){
+                       common++;
+               }
+       }
+       delete setIter1;
+//     model_print("measureSimilarity:139: common=%u\tGraphSize1=%u\tGraphSize2=%u\tGraphSize1=%f\tGraphSize2=%f\n", common, set1.getSize(), set2.getSize(), 1.0*common/set1.getSize(), 1.0*common/set2.getSize());
+       return common*1.0/set1.getSize() + common*1.0/set2.getSize();
+}
+
 uint EncodingSubGraph::estimateNewSize(EncodingNode *n) {
        SetIteratorEncodingEdge *eeit = n->edges.iterator();
        uint newsize = n->getSize();

diff --git a/src/ASTAnalyses/Encoding/subgraph.h b/src/ASTAnalyses/Encoding/subgraph.h
index 9327b977ea0581917f2aef8eae919c37c32debb5..1392dba72b70ee98df814d55102c73eecce9eab2 100644 (file)
--- a/src/ASTAnalyses/Encoding/subgraph.h
+++ b/src/ASTAnalyses/Encoding/subgraph.h
@@ -45,7 +45,8 @@ public:
        void encode();
        uint getEncoding(EncodingNode *n, uint64_t val);
        uint getEncodingMaxVal(EncodingNode *n) { return maxEncodingVal;}
-
+        double measureSimilarity(EncodingNode *n);
+        double measureSimilarity(EncodingSubGraph *sg);
        CMEMALLOC;
 private:
        uint estimateNewSize(EncodingNode *n);

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index 98036a7997049100fb7a4eea058a413caab66384..45f2c5f275465e7d187fa4a0289f7c14a6af9038 100644 (file)
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -640,23 +640,17 @@ void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p) {
        if (p == P_TRUE || p == P_BOTHTRUEFALSE) {
                // proxy => expression
                Edge cnfexpr = simplifyCNF(cnf, expression);
-               Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
                if (p == P_TRUE)
                        freeEdgeRec(expression);
                outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
-               outputCNFOR(cnf, cnfnegexpr, proxy);
                freeEdgeCNF(cnfexpr);
-               freeEdgeCNF(cnfnegexpr);
        }
        if (p == P_FALSE || p == P_BOTHTRUEFALSE) {
                // expression => proxy
                Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
-               Edge cnfexpr = simplifyCNF(cnf, expression);
                freeEdgeRec(expression);
                outputCNFOR(cnf, cnfnegexpr, proxy);
-               outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
                freeEdgeCNF(cnfnegexpr);
-               freeEdgeCNF(cnfexpr);
        }
 }
 

diff --git a/src/Backend/inc_solver.cc b/src/Backend/inc_solver.cc
index 80c4e4c9f6b4b4857e4add875aff110f1990932d..c1bebb806ad0e453ebd1e5a7e087ca34ac697551 100644 (file)
--- a/src/Backend/inc_solver.cc
+++ b/src/Backend/inc_solver.cc
@@ -12,7 +12,6 @@
 #include <fcntl.h>
 #include "common.h"
 #include <string.h>
-#include <stdexcept>
 
 IncrementalSolver *allocIncrementalSolver() {
        IncrementalSolver *This = (IncrementalSolver *)ourmalloc(sizeof(IncrementalSolver));
@@ -20,6 +19,7 @@ IncrementalSolver *allocIncrementalSolver() {
        This->solution = NULL;
        This->solutionsize = 0;
        This->offset = 0;
+       This->timeout = NOTIMEOUT;
        createSolver(This);
        return This;
 }
@@ -91,7 +91,7 @@ void startSolve(IncrementalSolver *This) {
 }
 
 int getSolution(IncrementalSolver *This) {
-       int result = readIntSolver(This);
+       int result = readStatus(This);
        if (result == IS_SAT) {
                int numVars = readIntSolver(This);
                if (numVars > This->solutionsize) {
@@ -112,6 +112,33 @@ int readIntSolver(IncrementalSolver *This) {
        return value;
 }
 
+int readStatus(IncrementalSolver *This) {
+       int retval;
+       fd_set rfds;
+       FD_ZERO(&rfds);
+       FD_SET(This->from_solver_fd, &rfds);
+       fd_set * temp;
+       if(This->timeout == NOTIMEOUT){
+               retval = select(This->from_solver_fd+1, &rfds, NULL, NULL, NULL);
+       }else {
+               struct timeval tv;
+               tv.tv_sec = This->timeout;
+               tv.tv_usec = 0;
+               retval = select(This->from_solver_fd+1, &rfds, NULL, NULL, &tv);
+       }
+       if(retval == -1){
+               perror("Error in select()");
+               exit(EXIT_FAILURE);
+       }
+       else if (retval){
+               printf("Data is available now.\n");
+               return readIntSolver(This);
+       }else{
+               printf("Timeout for the solver\n");
+               return IS_INDETER;
+       }
+}
+
 void readSolver(IncrementalSolver *This, void *tmp, ssize_t size) {
        char *result = (char *) tmp;
        ssize_t bytestoread = size;
@@ -120,7 +147,7 @@ void readSolver(IncrementalSolver *This, void *tmp, ssize_t size) {
                ssize_t n = read(This->from_solver_fd, &((char *)result)[bytesread], bytestoread);
                if (n == -1) {
                        model_print("Read failure\n");
-                       throw std::runtime_error("Read failure\n");
+                       exit(-1);
                }
                bytestoread -= n;
                bytesread += n;

diff --git a/src/Backend/inc_solver.h b/src/Backend/inc_solver.h
index 78506b45dbc7ddc6526b69cb3ab5b6396017cc8c..4692cfe626f0e6fd3add84adaf4a615bcfe4ddd1 100644 (file)
--- a/src/Backend/inc_solver.h
+++ b/src/Backend/inc_solver.h
@@ -18,6 +18,8 @@
 #include "solver_interface.h"
 #include "classlist.h"
 
+#define NOTIMEOUT -1
+
 struct IncrementalSolver {
        int *buffer;
        int *solution;
@@ -26,6 +28,7 @@ struct IncrementalSolver {
        pid_t solver_pid;
        int to_solver_fd;
        int from_solver_fd;
+        long timeout;
 };
 
 IncrementalSolver *allocIncrementalSolver();
@@ -43,5 +46,6 @@ void createSolver(IncrementalSolver *This);
 void killSolver(IncrementalSolver *This);
 void flushBufferSolver(IncrementalSolver *This);
 int readIntSolver(IncrementalSolver *This);
+int readStatus(IncrementalSolver *This);
 void readSolver(IncrementalSolver *This, void *buffer, ssize_t size);
 #endif

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index ad0722b2d262bf4a89a792fa220c2d1b8a554013..d2c04f62ac2a1aeeb7c9cddb4207c7fa07d61459 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -5,7 +5,8 @@
 #include "element.h"
 #include "set.h"
 #include "predicate.h"
-
+#include "csolver.h"
+#include "tunable.h"
 
 void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool &memo) {
        uint numParents = elem->parents.getSize();
@@ -222,8 +223,16 @@ void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
        ASSERT(encoding->type == BINARYINDEX);
        allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
        getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
-       if (encoding->element->anyValue)
-               generateAnyValueBinaryIndexEncoding(encoding);
+       if (encoding->element->anyValue){
+               uint setSize = encoding->element->getRange()->getSize();
+               uint encArraySize = encoding->encArraySize;
+               model_print("setSize=%u\tencArraySize=%u\n", setSize, encArraySize);
+               if(setSize < encArraySize * (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex)/10){
+                       generateAnyValueBinaryIndexEncodingPositive(encoding);
+               } else {
+                       generateAnyValueBinaryIndexEncoding(encoding);
+               }
+       }
 }
 
 void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
@@ -293,6 +302,20 @@ void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding)
        }
 }
 
+void SATEncoder::generateAnyValueBinaryIndexEncodingPositive(ElementEncoding *encoding) {
+       if (encoding->numVars == 0)
+               return;
+       Edge carray[encoding->encArraySize];
+       uint size = 0;
+       for (uint i = 0; i < encoding->encArraySize; i++) {
+               if (encoding->isinUseElement(i)) {
+                       carray[size] = generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i);
+                       size++;
+               }
+       }
+       addConstraintCNF(cnf, constraintOR(cnf, size, carray));
+}
+
 void SATEncoder::generateAnyValueBinaryValueEncoding(ElementEncoding *encoding) {
        uint64_t minvalueminusoffset = encoding->low - encoding->offset;
        uint64_t maxvalueminusoffset = encoding->high - encoding->offset;

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 659c0d980776e4689c4271873768580e1af4be48..62adb2fa9a635fbdde70862b5d2f75c3c4eac304 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -29,7 +29,8 @@ void SATEncoder::resetSATEncoder() {
        booledgeMap.reset();
 }
 
-int SATEncoder::solve() {
+int SATEncoder::solve(long timeout) {
+       cnf->solver->timeout = timeout;
        return solveCNF(cnf);
 }
 

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 78e797ff4f73d28f854cc1084166fff47a890c39..56be737580859e0e33ae5b52bd5953287a8f2847 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -10,7 +10,7 @@ typedef Hashtable<Boolean *, Node *, uintptr_t, 4> BooleanToEdgeMap;
 
 class SATEncoder {
 public:
-       int solve();
+       int solve(long timeout);
        SATEncoder(CSolver *solver);
        ~SATEncoder();
        void resetSATEncoder();
@@ -63,6 +63,7 @@ private:
        void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
        void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
        void generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding);
+       void generateAnyValueBinaryIndexEncodingPositive(ElementEncoding *encoding);
        void generateAnyValueBinaryValueEncoding(ElementEncoding *encoding);
        CNF *cnf;
        CSolver *solver;

diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc
index 0de7043b2d51472cc58089b1e5fa9bbe44015bfe..3f9e44eeaad1df92acc6654a93d5089b43e36ff2 100644 (file)
--- a/src/Encoders/naiveencoder.cc
+++ b/src/Encoders/naiveencoder.cc
@@ -11,18 +11,19 @@
 #include "table.h"
 #include "tableentry.h"
 #include "order.h"
+#include "tunable.h"
 #include <strings.h>
 
 void naiveEncodingDecision(CSolver *This) {
        SetIteratorBooleanEdge *iterator = This->getConstraints();
        while (iterator->hasNext()) {
                BooleanEdge b = iterator->next();
-               naiveEncodingConstraint(b.getBoolean());
+               naiveEncodingConstraint(This, b.getBoolean());
        }
        delete iterator;
 }
 
-void naiveEncodingConstraint(Boolean *This) {
+void naiveEncodingConstraint(CSolver *csolver, Boolean *This) {
        switch (This->type) {
        case BOOLEANVAR: {
                return;
@@ -33,11 +34,11 @@ void naiveEncodingConstraint(Boolean *This) {
                return;
        }
        case LOGICOP: {
-               naiveEncodingLogicOp((BooleanLogic *) This);
+               naiveEncodingLogicOp(csolver, (BooleanLogic *) This);
                return;
        }
        case PREDICATEOP: {
-               naiveEncodingPredicate((BooleanPredicate *) This);
+               naiveEncodingPredicate(csolver, (BooleanPredicate *) This);
                return;
        }
        default:
@@ -45,30 +46,30 @@ void naiveEncodingConstraint(Boolean *This) {
        }
 }
 
-void naiveEncodingLogicOp(BooleanLogic *This) {
+void naiveEncodingLogicOp(CSolver *csolver, BooleanLogic *This) {
        for (uint i = 0; i < This->inputs.getSize(); i++) {
-               naiveEncodingConstraint(This->inputs.get(i).getBoolean());
+               naiveEncodingConstraint(csolver, This->inputs.get(i).getBoolean());
        }
 }
 
-void naiveEncodingPredicate(BooleanPredicate *This) {
+void naiveEncodingPredicate(CSolver *csolver, BooleanPredicate *This) {
        FunctionEncoding *encoding = This->getFunctionEncoding();
        if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
                This->getFunctionEncoding()->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
 
        for (uint i = 0; i < This->inputs.getSize(); i++) {
                Element *element = This->inputs.get(i);
-               naiveEncodingElement(element);
+               naiveEncodingElement(csolver, element);
        }
 }
 
-void naiveEncodingElement(Element *This) {
+void naiveEncodingElement(CSolver *csolver, Element *This) {
        ElementEncoding *encoding = This->getElementEncoding();
        if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
                if (This->type != ELEMCONST) {
                        model_print("INFO: naive encoder is making the decision about element %p....\n", This);
                }
-               encoding->setElementEncodingType(UNARY);
+               encoding->setElementEncodingType((ElementEncodingType)csolver->getTuner()->getVarTunable(This->getRange()->getType(), NAIVEENCODER, &NaiveEncodingDesc));
                encoding->encodingArrayInitialization();
        }
 
@@ -76,7 +77,7 @@ void naiveEncodingElement(Element *This) {
                ElementFunction *function = (ElementFunction *) This;
                for (uint i = 0; i < function->inputs.getSize(); i++) {
                        Element *element = function->inputs.get(i);
-                       naiveEncodingElement(element);
+                       naiveEncodingElement(csolver, element);
                }
                FunctionEncoding *encoding = function->getElementFunctionEncoding();
                if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)

diff --git a/src/Encoders/naiveencoder.h b/src/Encoders/naiveencoder.h
index dbc9148d6199d72257498de94791381f3f5417d6..fe84a2b64eb874b13fc6ba284e1dba3080feb5b6 100644 (file)
--- a/src/Encoders/naiveencoder.h
+++ b/src/Encoders/naiveencoder.h
@@ -10,8 +10,8 @@
  */
 
 void naiveEncodingDecision(CSolver *csolver);
-void naiveEncodingConstraint(Boolean *This);
-void naiveEncodingLogicOp(BooleanLogic *This);
-void naiveEncodingPredicate(BooleanPredicate *This);
-void naiveEncodingElement(Element *This);
+void naiveEncodingConstraint(CSolver *csolver, Boolean *This);
+void naiveEncodingLogicOp(CSolver *csolver, BooleanLogic *This);
+void naiveEncodingPredicate(CSolver *csolver, BooleanPredicate *This);
+void naiveEncodingElement(CSolver *csolver, Element *This);
 #endif

diff --git a/src/Makefile b/src/Makefile
index fcbf7103db3e33f64ae9b7b4c8b0f3f068d48513..838a47802ed595177b02e8eead9613f1cf3716c8 100644 (file)
--- a/src/Makefile
+++ b/src/Makefile
@@ -13,6 +13,7 @@ HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wi
 OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o)
 
 CFLAGS := -Wall -O0 -g
+CXXFLAGS := -std=c++1y -pthread
 CFLAGS += -IAST -IASTTransform -IASTAnalyses -IASTAnalyses/Polarity -IASTAnalyses/Order -IASTAnalyses/Encoding -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner -ISerialize
 LDFLAGS := -ldl -lrt -rdynamic -g
 SHARED := -shared
@@ -58,7 +59,7 @@ ${OBJ_DIR}/$(LIB_SO): $(OBJECTS)
        $(CXX) -g $(SHARED) -o ${OBJ_DIR}/$(LIB_SO) $+ $(LDFLAGS)
 
 ${OBJ_DIR}/%.o: %.cc
-       $(CXX) -fPIC -c $< -o $@ $(CFLAGS) -Wno-unused-variable -std=c++1y -pthread
+       $(CXX) -fPIC -c $< -o $@ $(CFLAGS) -Wno-unused-variable $(CXXFLAGS)
 
 ${OBJ_DIR}/%.o: %.c
        $(CC) -fPIC -c $< -o $@ $(CFLAGS) -Wno-unused-variable

diff --git a/src/Tuner/autotuner.cc b/src/Tuner/autotuner.cc
index d31a72f1e024733dc03d801ba221a59cc0fd46c2..6b297557af8a3e1fec719a09559c3d4bdec59a6e 100644 (file)
--- a/src/Tuner/autotuner.cc
+++ b/src/Tuner/autotuner.cc
@@ -4,52 +4,9 @@
 #include <math.h>
 #include <stdlib.h>
 #include <float.h>
-#include <iostream>
-#include <chrono>
-#include <thread>
-#include <mutex>
-#include <condition_variable>
 
-#define TIMEOUT 1000s
 #define UNSETVALUE -1
-#define POSINFINITY 9999999999L
-
-using namespace std::chrono_literals;
-
-int solve(CSolver *solver)
-{
-       try{
-               return solver->solve();
-       }
-       catch (std::runtime_error &e) {
-               return UNSETVALUE;
-       }
-}
-
-int solveWrapper(CSolver *solver)
-{
-       std::mutex m;
-       std::condition_variable cv;
-       int retValue;
-
-       std::thread t([&cv, &retValue, solver]()
-               {
-                                                               retValue = solve(solver);
-                                                               cv.notify_one();
-               });
-
-       t.detach();
-
-       {
-               std::unique_lock<std::mutex> l(m);
-               if (cv.wait_for(l, TIMEOUT) == std::cv_status::timeout)
-                       throw std::runtime_error("Timeout");
-       }
-
-       return retValue;
-}
-
-
+#define TIMEOUTSEC 5000
 AutoTuner::AutoTuner(uint _budget) :
        budget(_budget), result(UNSETVALUE) {
 }
@@ -61,23 +18,16 @@ void AutoTuner::addProblem(CSolver *solver) {
 long long AutoTuner::evaluate(CSolver *problem, SearchTuner *tuner) {
        CSolver *copy = problem->clone();
        copy->setTuner(tuner);
+       copy->setSatSolverTimeout(TIMEOUTSEC);
        model_print("**********************\n");
-       long long metric = 0L;
-       try {
-               int sat = solveWrapper(copy);
-               if (result == UNSETVALUE)
-                       result = sat;
-               else if (result != sat) {
-                       model_print("&&&&&&&&&&&&&&&&&& Result has changed &&&&&&&&&&&&&\n");
-                       copy->printConstraints();
-               }
-               metric = copy->getElapsedTime();
+       int sat = copy->solve();
+       if (result == UNSETVALUE && sat != IS_INDETER)
+               result = sat;
+       else if (result != sat && sat != IS_INDETER) {
+               model_print("&&&&&&&&&&&&&&&&&& Result has changed &&&&&&&&&&&&&\n");
+               copy->printConstraints();
        }
-       catch (std::runtime_error &e) {
-               metric = POSINFINITY;
-               model_print("TimeOut has hit\n");
-       }
-
+       long long metric = copy->getElapsedTime();
        delete copy;
        return metric;
 }

diff --git a/src/Tuner/searchtuner.cc b/src/Tuner/searchtuner.cc
index e9de49f4a8c799f99cd819b7f939486e4b83a14f..bfe66bb4dd77cdcb21e15230a09cb9e5a6da5882 100644 (file)
--- a/src/Tuner/searchtuner.cc
+++ b/src/Tuner/searchtuner.cc
@@ -44,11 +44,12 @@ void TunableSetting::setDecision(int _low, int _high, int _default, int _selecti
 }
 
 void TunableSetting::print() {
+       model_print("Param %s = %u \t range=[%u,%u]", tunableParameterToString( (Tunables)param), selectedValue, lowValue, highValue);
        if (hasVar) {
-               model_print("VarType1 %" PRIu64 ", ", type1);
+               model_print("\tVarType1 %" PRIu64 ", ", type1);
                model_print("VarType2 %" PRIu64 ", ", type2);
        }
-       model_print("Param %s = %u \t range=[%u,%u]\n", tunableParameterToString( (Tunables)param), selectedValue, lowValue, highValue);
+       model_print("\n");
 }
 
 unsigned int tunableSettingHash(TunableSetting *setting) {

diff --git a/src/Tuner/tunable.cc b/src/Tuner/tunable.cc
index 966cb0014226c9e009d6abb1aac1a68fcc07c28d..dd2cb7f5065b558b3f4818378f1a8da94fbe9a23 100644 (file)
--- a/src/Tuner/tunable.cc
+++ b/src/Tuner/tunable.cc
@@ -15,35 +15,39 @@ int DefaultTuner::getVarTunable(VarType vartype1, VarType vartype2, TunableParam
        return descriptor->defaultValue;
 }
 
-const char *tunableParameterToString(Tunables tunable) {
-       switch (tunable) {
-       case DECOMPOSEORDER:
-               return "DECOMPOSEORDER";
-       case MUSTREACHGLOBAL:
-               return "MUSTREACHGLOBAL";
-       case MUSTREACHLOCAL:
-               return "MUSTREACHLOCAL";
-       case MUSTREACHPRUNE:
-               return "MUSTREACHPRUNE";
-       case OPTIMIZEORDERSTRUCTURE:
-               return "OPTIMIZEORDERSTRUCTURE";
-       case ORDERINTEGERENCODING:
-               return "ORDERINTEGERENCODING";
-       case PREPROCESS:
-               return "PREPROCESS";
-       case NODEENCODING:
-               return "NODEENCODING";
-       case EDGEENCODING:
-               return "EDGEENCODING";
-       case MUSTEDGEPRUNE:
-               return "MUSTEDGEPRUNE";
-       case ELEMENTOPT:
-               return "ELEMENTOPT";
-       case ELEMENTOPTSETS:
-               return "ELEMENTOPTSETS";
-       case PROXYVARIABLE:
-               return "PROXYVARIABLE";
-       default:
-               ASSERT(0);
-       }
+const char* tunableParameterToString(Tunables tunable){
+        switch(tunable){
+                case DECOMPOSEORDER:
+                        return "DECOMPOSEORDER";
+                case MUSTREACHGLOBAL:
+                        return "MUSTREACHGLOBAL";
+                case MUSTREACHLOCAL:
+                        return "MUSTREACHLOCAL";
+                case MUSTREACHPRUNE:
+                        return "MUSTREACHPRUNE";
+                case OPTIMIZEORDERSTRUCTURE:
+                        return "OPTIMIZEORDERSTRUCTURE";
+                case ORDERINTEGERENCODING:
+                        return "ORDERINTEGERENCODING";
+                case PREPROCESS:
+                        return "PREPROCESS";
+                case NODEENCODING:
+                        return "NODEENCODING";
+                case EDGEENCODING:
+                        return "EDGEENCODING";
+                case MUSTEDGEPRUNE:
+                        return "MUSTEDGEPRUNE";
+               case ELEMENTOPT: 
+                       return "ELEMENTOPT";
+               case ELEMENTOPTSETS:
+                       return "ELEMENTOPTSETS";
+               case PROXYVARIABLE:
+                       return "PROXYVARIABLE";
+               case ENCODINGGRAPHOPT:
+                       return "ENCODINGGRAPHOPT";
+               case NAIVEENCODER:
+                       return "NAIVEENCODER";
+                default:
+                        ASSERT(0);
+        }
 }

diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index 9fd614a5eefc447412c6f962497fdf2b47f160a3..0213f0330193c26d872d2b9938e0718ec8f6c82d 100644 (file)
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -39,8 +39,12 @@ public:
 static TunableDesc onoff(0, 1, 1);
 static TunableDesc offon(0, 1, 0);
 static TunableDesc proxyparameter(1, 5, 2);
+static TunableDesc mustValueBinaryIndex(1, 9, 5);
+static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
+static TunableDesc NaiveEncodingDesc(ONEHOT, BINARYINDEX, ONEHOT);
 
-enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT, ELEMENTOPTSETS, PROXYVARIABLE};
+enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT, 
+        ENCODINGGRAPHOPT, ELEMENTOPTSETS, PROXYVARIABLE, MUSTVALUE, NAIVEENCODER};
 typedef enum Tunables Tunables;
 
 const char *tunableParameterToString(Tunables tunable);

diff --git a/src/csolver.cc b/src/csolver.cc
index e72b3631de5385a23442b6f663d4f1731725198e..f1bd9b64870f4dd45ed570a2d2608d2772825f8c 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -34,7 +34,8 @@ CSolver::CSolver() :
        boolFalse(boolTrue.negate()),
        unsat(false),
        tuner(NULL),
-       elapsedTime(0)
+       elapsedTime(0),
+       satsolverTimeout(NOTIMEOUT)
 {
        satEncoder = new SATEncoder(this);
 }
@@ -616,7 +617,6 @@ int CSolver::solve() {
        eop.doTransform();
 
        EncodingGraph eg(this);
-       eg.buildGraph();
        eg.encode();
 
        naiveEncodingDecision(this);
@@ -631,8 +631,8 @@ int CSolver::solve() {
        model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
 
        model_print("Is problem UNSAT after encoding: %d\n", unsat);
-       int result = unsat ? IS_UNSAT : satEncoder->solve();
-       model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : " UNSAT");
+       int result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
+       model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT? "SAT" : result == IS_INDETER? "INDETERMINATE" : " UNSAT");
        time2 = getTimeNano();
        elapsedTime = time2 - startTime;
        model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);

diff --git a/src/csolver.h b/src/csolver.h
index 19ba3e12db5eac9f06affa74540cf66bf774f997..60e7c6861033e70216aa782238d80c7b8f6c0c43 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -139,6 +139,7 @@ public:
        bool isFalse(BooleanEdge b);
 
        void setUnSAT() { model_print("Setting UNSAT %%%%%%\n"); unsat = true; }
+        void setSatSolverTimeout(long seconds){ satsolverTimeout = seconds;}
        bool isUnSAT() { return unsat; }
 
        void printConstraint(BooleanEdge boolean);
@@ -219,6 +220,7 @@ private:
        bool unsat;
        Tuner *tuner;
        long long elapsedTime;
+        long satsolverTimeout;
        friend class ElementOpt;
 };