- Disable the UNSAT cache by default

- Update configuration
FCC · Oct 30, 2015 · 4e3d56b · 4e3d56b
1 parent 8b1123d
commit 4e3d56b
Show file tree

Hide file tree

Showing 6 changed files with 21 additions and 16 deletions.
diff --git a/satfc/src/main/java/ca/ubc/cs/beta/stationpacking/cache/RedisCacher.java b/satfc/src/main/java/ca/ubc/cs/beta/stationpacking/cache/RedisCacher.java
@@ -174,21 +174,19 @@ public Object doInRedis(RedisConnection connection) throws DataAccessException {
         return results;
     }
 
-    public ContainmentCacheInitData getContainmentCacheInitData(long limit, Map<CacheCoordinate, ImmutableBiMap<Station, Integer>> coordinateToPermutation, String acceptRegex) {
+    public ContainmentCacheInitData getContainmentCacheInitData(long limit, Map<CacheCoordinate, ImmutableBiMap<Station, Integer>> coordinateToPermutation, String acceptRegex, boolean skipSAT, boolean skipUNSAT) {
         log.info("Pulling precache data from redis");
         final Watch watch = Watch.constructAutoStartWatch();
 
         final Set<String> SATKeys = new HashSet<>();
         final Set<String> UNSATKeys = new HashSet<>();
 
         final Cursor<byte[]> scan = redisTemplate.getConnectionFactory().getConnection().scan(ScanOptions.scanOptions().build());
-        long count = 0;
-        while (count < limit && scan.hasNext()) {
+        while (SATKeys.size() + UNSATKeys.size() < limit && scan.hasNext()) {
             final String key = new String(scan.next());
-            count++;
-            if (key.startsWith("SATFC:SAT:")) {
+            if (key.startsWith("SATFC:SAT:") && !skipSAT) {
                 SATKeys.add(key);
-            } else if (key.startsWith("SATFC:UNSAT:")) {
+            } else if (key.startsWith("SATFC:UNSAT:") && !skipUNSAT) {
                 UNSATKeys.add(key);
             }
         }

diff --git a/...main/java/ca/ubc/cs/beta/stationpacking/facade/datamanager/solver/bundles/YAMLBundle.java b/...main/java/ca/ubc/cs/beta/stationpacking/facade/datamanager/solver/bundles/YAMLBundle.java
@@ -313,7 +313,7 @@ public boolean shouldCache(SolverResult result) {
         }
 
         private double minTimeToCache = 0;
-        private boolean doNotCacheUNSAT = false;
+        private boolean doNotCacheUNSAT = true;
 
     }
 

diff --git a/satfc/src/main/resources/bundles/satfc_parallel.yaml b/satfc/src/main/resources/bundles/satfc_parallel.yaml
@@ -1,15 +1,14 @@
 ---
 CONFIGS:
-  claspH1: &claspH1 --backprop --eq=0 --trans-ext=all --sat-prepro=0 --sign-def=0 --del-max=100000 --strengthen=local,1 --loops=common --init-watches=0 --heuristic=Vsids,96 --del-cfl=F,500 --restarts=D,100,0.8,100 --update-act --del-glue=4,0 --update-lbd=0 --reverse-arcs=3 --otfs=2 --del-on-restart=0 --contraction=500 --local-restarts --lookahead=no --save-progress=50
+  claspS1: &claspS1 --backprop --eq-dfs --eq=6 --trans-ext=card --sat-prepro=0 --sign-def=2 --reset-restarts=1 --del-max=1537606602 --opt-heuristic=3 --strengthen=local,2 --dom-mod=3,1 --score-res=2 --loops=common --init-watches=2 --heuristic=Domain,97 --score-other=2 --del-cfl=+,37379,3,214 --restarts=F,628 --partial-check=40 --deletion=basic,85,2 --counter-restarts=1 --del-grow=4.7859,15.8141,L,1253 --del-glue=2,0 --update-lbd=2 --reverse-arcs=2 --del-estimate=3 --opt-strategy=usc,2 --otfs=1 --init-moms --del-on-restart=50 --contraction=518 --rand-freq=0.01 --del-init=13.6918,192,16415 --local-restarts --lookahead=body,1863992766 --save-progress=152 --counter-bump=2606
   claspH2: &claspH2 --sat-prepro=0 --init-watches=2 --rand-freq=0.0 --sign-def=2 --del-init=5.0,10,2500 --strengthen=local,2 --lookahead=hybrid,1 --otfs=2 --reverse-arcs=3 --save-progress=180 --del-glue=2,0 --del-cfl=L,2000 --restarts=F,1600 --local-restarts --update-lbd=1 --heuristic=Vsids,92 --deletion=ipSort,75,2 --contraction=166 --del-grow=0 --del-on-restart=50 --del-max=32767
   claspVHF: &claspVHF --backprop --eq=0 --trans-ext=all --sat-prepro=0 --sign-def=0 --del-max=100000 --strengthen=local,1 --loops=common --init-watches=0 --heuristic=Vsids,96 --del-cfl=F,500 --restarts=D,100,0.8,100 --update-act --del-glue=4,0 --update-lbd=0 --reverse-arcs=3 --otfs=2 --del-on-restart=0 --contraction=500 --local-restarts --lookahead=no --save-progress=50
-  dcca: &dcca -alg satenstein -cutoff max -promisinglist 1 -decreasingvariable 13 -heuristic 20 -avgweightthreshold 300 -DCCAp 0.3 -DCCAq 0
+  satensteinS1: &satenstein -alg satenstein -cutoff max -heuristic 20 -decreasingvariable 12 -adaptiveprom 1 -avgweightthreshold 330 -singleclause 1 -updateschemepromlist 1 -clausepen 0 -promisinglist 1 -tabusearch 1 -alpha 1.3 -ignoreStartingAssignmentPercentage 0.4047971829522954 -selectclause 1 -adaptive 0 -randomwalk 1 -randomVarInitPercentage 0.3007051676878647 -tabu 5 -DCCAp 0.3 -DCCAq 0 -scoringmeasure 1 -maxinc 10 -sapsthresh -0.1 -performrandomwalk 1 -rho 0.8 -pflat 0.15 -rwp 0.15 -varinfalse 1 -adaptpromwalkprob 0
 UHF:
     - name: PARALLEL
       args: 
         configs:
           - 
-            - name: UNSAT_CACHE
             - name: SAT_CACHE
             - name: DELAY
               args: 
@@ -18,13 +17,13 @@ UHF:
           -   
             - name: CLASP
               args:
-                config: *claspH1
+                config: *claspS1
             - name: SAT_PRESOLVER
               args: 
                 solverConfig:
                   name: CLASP
                   args:
-                    config: *claspH1
+                    config: *claspS1
                 strategy: 
                   name: ITERATIVE_DEEPEN
                   args:
@@ -34,7 +33,7 @@ UHF:
           -
             - name: CLASP
               args: 
-                config: *claspH1
+                config: *claspS1
                 encodingType: DIRECT
           -
             - name: PARALLEL
@@ -59,7 +58,7 @@ UHF:
           -
             - name: SATENSTEIN
               args:
-                config: *dcca
+                config: *satenstein
                 encodingType: DIRECT
     - name: RESULT_SAVER
     - name: PYTHON_VERIFIER

diff --git a/satfc/src/main/resources/bundles/satfc_sequential.yaml b/satfc/src/main/resources/bundles/satfc_sequential.yaml
@@ -27,7 +27,6 @@ UHF:
               name: NEIGHBOURHOOD
               args: 
                 numLayers: 1
-    - name: UNSAT_CACHE
     - name: SAT_CACHE
     - name: RESULT_SAVER
     - name: VERIFIER

diff --git a/satfcserver/src/main/java/ca/ubc/cs/beta/stationpacking/webapp/CacheLocator.java b/satfcserver/src/main/java/ca/ubc/cs/beta/stationpacking/webapp/CacheLocator.java
@@ -113,7 +113,7 @@ public void onApplicationEvent(ContextRefreshedEvent event) {
         });
 
         log.info("Beginning to init caches");
-        final ContainmentCacheInitData containmentCacheInitData = cacher.getContainmentCacheInitData(parameters.getCacheSizeLimit(), coordinateToPermutation, parameters.getAcceptRegex());
+        final ContainmentCacheInitData containmentCacheInitData = cacher.getContainmentCacheInitData(parameters.getCacheSizeLimit(), coordinateToPermutation, parameters.getAcceptRegex(), parameters.isSkipSAT(), parameters.isSkipUNSAT());
         coordinateToBundle.keySet().forEach(cacheCoordinate -> {
             final ISatisfiabilityCache cache = cacheFactory.create(coordinateToPermutation.get(cacheCoordinate));
             log.info("Cache created for coordinate " + cacheCoordinate);

diff --git a/.../src/main/java/ca/ubc/cs/beta/stationpacking/webapp/parameters/SATFCServerParameters.java b/.../src/main/java/ca/ubc/cs/beta/stationpacking/webapp/parameters/SATFCServerParameters.java
@@ -47,6 +47,15 @@ public class SATFCServerParameters extends AbstractOptions {
     @Getter
     private long cacheSizeLimit = Long.MAX_VALUE;
 
+    @Parameter(names = "--skipSAT", description = "Do not load SAT entries from redis")
+    @Getter
+    private boolean skipSAT = false;
+
+    @Parameter(names = "--skipUNSAT", description = "Do not load UNSAT entries from redis")
+    @Getter
+    private boolean skipUNSAT = true;
+
+
     public void validate() {
         Preconditions.checkArgument(new File(constraintFolder).isDirectory(), "Provided constraint folder is not a directory", constraintFolder);
     }