From cb27924ba5a3ef99d44a1e0cbdd43906b2a28d61 Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Thu, 20 Sep 2018 19:58:25 -0700 Subject: [PATCH] Commiting my local changes ... --- deploy-cs.sh | 2 +- src/1.log | 2018 +++++++++++++++++++++ src/2.log | 2018 +++++++++++++++++++++ src/ASTAnalyses/Encoding/encodinggraph.cc | 25 +- src/Backend/constraint.cc | 9 + src/Backend/inc_solver.cc | 3 +- src/Backend/satencoder.cc | 6 + src/Encoders/naiveencoder.cc | 2 +- src/Makefile | 2 +- src/Test/deserializerautotune.cc | 2 +- src/Tuner/autotuner.cc | 72 +- src/common.mk | 2 +- src/csolver.cc | 6 +- 13 files changed, 4140 insertions(+), 27 deletions(-) create mode 100644 src/1.log create mode 100644 src/2.log diff --git a/deploy-cs.sh b/deploy-cs.sh index 7cec4fc..bafb92a 100755 --- a/deploy-cs.sh +++ b/deploy-cs.sh @@ -4,7 +4,7 @@ set -e BASE=../ -SERVERS="dc-8.calit2.uci.edu dc-9.calit2.uci.edu dc-10.calit2.uci.edu dc-11.calit2.uci.edu" +SERVERS="dc-5.calit2.uci.edu dc-7.calit2.uci.edu dc-8.calit2.uci.edu dc-9.calit2.uci.edu dc-10.calit2.uci.edu dc-11.calit2.uci.edu" REMOTEDIR="/scratch/hamed/" INFILE="constraint_compiler/" SRC="constraint_compiler/src/" diff --git a/src/1.log b/src/1.log new file mode 100644 index 0000000..3b13110 --- /dev/null +++ b/src/1.log @@ -0,0 +1,2018 @@ +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 new file mode 100644 index 0000000..d57ea60 --- /dev/null +++ b/src/2.log @@ -0,0 +1,2018 @@ +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 43043a7..b55c7f2 100644 --- a/src/ASTAnalyses/Encoding/encodinggraph.cc +++ b/src/ASTAnalyses/Encoding/encodinggraph.cc @@ -114,6 +114,7 @@ void EncodingGraph::validate() { void EncodingGraph::encode() { SetIteratorEncodingSubGraph *itesg = subgraphs.iterator(); + model_print("#SubGraph = %u", subgraphs.getSize()); while (itesg->hasNext()) { EncodingSubGraph *sg = itesg->next(); sg->encode(); @@ -326,6 +327,12 @@ void EncodingGraph::decideEdges() { uint leftSize = 0, rightSize = 0, newSize = 0; uint64_t totalCost = 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()); @@ -334,6 +341,9 @@ void EncodingGraph::decideEdges() { newSize = (rightSize > newSize) ? rightSize : newSize; totalCost = (newSize - leftSize) * left->elements.getSize() + (newSize - rightSize) * right->elements.getSize(); + if(leftSize == newSize && rightSize == newSize){ + merge = true; + } } else if (leftGraph != NULL && rightGraph == NULL) { leftSize = convertSize(leftGraph->encodingSize); rightSize = convertSize(right->getSize()); @@ -342,13 +352,14 @@ void EncodingGraph::decideEdges() { newSize = (rightSize > newSize) ? rightSize : newSize; totalCost = (newSize - leftSize) * leftGraph->numElements + (newSize - rightSize) * right->elements.getSize(); + if(leftSize == newSize && rightSize == newSize){ + merge = true; + } } else { //Neither are null - //Are we already merged? if (leftGraph == rightGraph) continue; - leftSize = convertSize(leftGraph->encodingSize); rightSize = convertSize(rightGraph->encodingSize); newSize = convertSize(leftGraph->estimateNewSize(rightGraph)); @@ -356,9 +367,15 @@ void EncodingGraph::decideEdges() { 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; + } } - - if ((totalCost * CONVERSIONFACTOR) < eeValue) { +// model_print("******************************\n"); + if (merge) { //add the edge mergeNodes(left, right); } diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc index b35b456..6425c58 100644 --- a/src/Backend/constraint.cc +++ b/src/Backend/constraint.cc @@ -575,6 +575,9 @@ Edge simplifyCNF(CNF *cnf, Edge input) { void addClause(CNF *cnf, uint numliterals, int *literals){ cnf->clausecount++; + for(uint i=0; i< numliterals; i++) + model_print("%d ", literals[i]); + model_print("\n"); addArrayClauseLiteral(cnf->solver, numliterals, literals); } @@ -640,17 +643,23 @@ 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 d295cee..80c4e4c 100644 --- a/src/Backend/inc_solver.cc +++ b/src/Backend/inc_solver.cc @@ -12,6 +12,7 @@ #include #include "common.h" #include +#include IncrementalSolver *allocIncrementalSolver() { IncrementalSolver *This = (IncrementalSolver *)ourmalloc(sizeof(IncrementalSolver)); @@ -119,7 +120,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"); - exit(-1); + throw std::runtime_error("Read failure\n"); } bytestoread -= n; bytesread += n; diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc index 659c0d9..4c49b16 100644 --- a/src/Backend/satencoder.cc +++ b/src/Backend/satencoder.cc @@ -37,7 +37,13 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) { SetIteratorBooleanEdge *iterator = csolver->getConstraints(); while (iterator->hasNext()) { BooleanEdge constraint = iterator->next(); + model_print("**********************************************************\n"); + constraint.print(); + model_print("\n"); Edge c = encodeConstraintSATEncoder(constraint); + model_print("&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&\n"); + printCNF(c); + model_print("\n"); addConstraintCNF(cnf, c); } delete iterator; diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc index 7e33c1b..f5aa44b 100644 --- a/src/Encoders/naiveencoder.cc +++ b/src/Encoders/naiveencoder.cc @@ -68,7 +68,7 @@ void naiveEncodingElement(Element *This) { if(This->type != ELEMCONST){ model_print("INFO: naive encoder is making the decision about element %p....\n", This); } - encoding->setElementEncodingType(BINARYINDEX); + encoding->setElementEncodingType(UNARY); encoding->encodingArrayInitialization(); } diff --git a/src/Makefile b/src/Makefile index caccbdb..fcbf710 100644 --- a/src/Makefile +++ b/src/Makefile @@ -58,7 +58,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 + $(CXX) -fPIC -c $< -o $@ $(CFLAGS) -Wno-unused-variable -std=c++1y -pthread ${OBJ_DIR}/%.o: %.c $(CC) -fPIC -c $< -o $@ $(CFLAGS) -Wno-unused-variable diff --git a/src/Test/deserializerautotune.cc b/src/Test/deserializerautotune.cc index d3f2440..7c3728d 100644 --- a/src/Test/deserializerautotune.cc +++ b/src/Test/deserializerautotune.cc @@ -7,7 +7,7 @@ int main(int argc, char **argv) { exit(-1); } CSolver *solvers[argc - 1]; - AutoTuner *autotuner = new AutoTuner(100); + AutoTuner *autotuner = new AutoTuner(300); for (int i = 1; i < argc; i++) { solvers[i - 1] = CSolver::deserialize(argv[i]); autotuner->addProblem(solvers[i - 1]); diff --git a/src/Tuner/autotuner.cc b/src/Tuner/autotuner.cc index 842bab8..29c3289 100644 --- a/src/Tuner/autotuner.cc +++ b/src/Tuner/autotuner.cc @@ -4,8 +4,51 @@ #include #include #include +#include +#include +#include +#include +#include +#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 l(m); + if(cv.wait_for(l, TIMEOUT) == std::cv_status::timeout) + throw std::runtime_error("Timeout"); + } + + return retValue; +} + AutoTuner::AutoTuner(uint _budget) : budget(_budget), result(UNSETVALUE) { @@ -19,21 +62,22 @@ long long AutoTuner::evaluate(CSolver *problem, SearchTuner *tuner) { CSolver *copy = problem->clone(); copy->setTuner(tuner); model_print("**********************\n"); - int sat = copy->solve(); - if (result == UNSETVALUE) - result = sat; - else if (result != sat) { - model_print("&&&&&&&&&&&&&&&&&& Result has changed &&&&&&&&&&&&&\n"); - copy->printConstraints(); + 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(); + } + catch(std::runtime_error& e) { + metric = POSINFINITY; + model_print("TimeOut has hit\n"); } - //model_print("SAT %d\n", result); - long long elapsedTime = copy->getElapsedTime(); -// long long encodeTime = copy->getEncodeTime(); -// long long solveTime = copy->getSolveTime(); - long long metric = elapsedTime; -// model_print("Elapsed Time: %llu\n", elapsedTime); -// model_print("Encode Time: %llu\n", encodeTime); -// model_print("Solve Time: %llu\n", solveTime); + delete copy; return metric; } diff --git a/src/common.mk b/src/common.mk index 8ffb364..fbd6f88 100644 --- a/src/common.mk +++ b/src/common.mk @@ -1,7 +1,7 @@ # A few common Makefile items CC := gcc -CXX := g++ +CXX := g++-5 UNAME := $(shell uname) diff --git a/src/csolver.cc b/src/csolver.cc index b7c9aa4..5cdca73 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -615,9 +615,9 @@ int CSolver::solve() { ElementOpt eop(this); eop.doTransform(); -// EncodingGraph eg(this); -// eg.buildGraph(); -// eg.encode(); + EncodingGraph eg(this); + eg.buildGraph(); + eg.encode(); naiveEncodingDecision(this); // eg.validate(); -- 2.34.1