Making nesthdb easier to run

.gitignore

@@ -0,0 +1,3 @@
+bin/
+
+__pycache__

common.py

@@ -1,5 +1,5 @@
 #!/usr/bin/python3
-# -*- coding: future_fstrings -*-
+
 import argparse
 import logging
 import subprocess
@@ -84,7 +84,7 @@ def setup_arg_parser(usage):
     parser = argparse.ArgumentParser(usage="%(prog)s [general options] -f input-file problem-type [problem specific-options]", formatter_class=MyFormatter)
 
     parser.add_argument("-f", "--file", dest="file", help="Input file for the problem to solve", required=True)
-    
+
     # general options
     gen_opts = parser.add_argument_group("general options", "General options")
     gen_opts.add_argument("-t", dest="type", help="type of the cluster run", default="")
@@ -110,7 +110,7 @@ def parse_args(parser):
     logging.basicConfig(format='[%(levelname)s] %(name)s: %(message)s', level=log_level)
 
     return args
-    
+
 """
 _LOG_LEVEL_STRINGS = ["DEBUG_SQL", "DEBUG", "INFO", "WARNING", "ERROR", "CRITICAL"]
 
@@ -155,7 +155,7 @@ class MyFormatter(argparse.ArgumentDefaultsHelpFormatter,argparse.RawDescription
             p.add_argument(arg,**kwargs)
 
     parser.add_argument("-f", "--file", dest="file", help="Input file for the problem to solve", required=True)
-    
+
     # general options
     gen_opts = parser.add_argument_group("general options", "General options")
     gen_opts.add_argument("-t", dest="type", help="type of the cluster run", default="")

config.json

@@ -3,28 +3,83 @@
     "dsn": {
       "host": "localhost",
       "port": 5432,
-      "database": "logicsem", 
-      "user": "logicsem", 
+      "database": "logicsem",
+      "user": "logicsem",
       "password": "XXX",
       "application_name": "dpdb"
     },
     "max_connections": 100
   },
   "db_admin": {
-      "host": "localhost",
-      "port": 5432,
-      "database": "logicsem",
-      "user": "postgres",
-      "password": "XXX",
-      "application_name": "dpdb-admin"
+    "host": "localhost",
+    "port": 5432,
+    "database": "logicsem",
+    "user": "postgres",
+    "password": "XXX",
+    "application_name": "dpdb-admin"
   },
   "htd": {
-    "path": "../htd/bin/htd_main",
+    "path": "./bin/htd_main",
     "parameters": [
       "--child-limit","5"
     ]
   },
   "dpdb": {
-    "max_worker_threads": 24
+  },
+  "problem_specific": {
+    "nestpmc": {
+      "max_solver_threads": 12,
+      "inner_vars_threshold": 40,
+      "max_worker_threads": 12
+    }
+  },
+  "nesthdb": {
+    "threshold_hybrid" : 1000,
+    "threshold_abstract" : 8,
+    "max_recursion_depth" : 1,
+    "sat_solver": {
+      "path": "./bin/picosat",
+      "seed_arg": "-s"
+    },
+    "sharpsat_solver": {
+      "path": "<PATH_TO>/miniC2D-1.0.0",
+      "args": "-C -c",
+      "output_parser": {
+        "class": "RegExReader",
+        "args": {
+          "pattern": "Counting... (\\d+) models"
+        },
+        "result":"result"
+      }
+    },
+    "pmc_solver": {
+      "path": "./projMC-wrapper.py",
+      "seed_arg": "-s",
+      "output_parser": {
+        "class": "RegExReader",
+        "args": {
+          "pattern": "s (\\d+)\\n"
+        },
+        "result":"result"
+      }
+    },
+    "preprocessor": {
+      "path": "./bin/pmc",
+      "args": "-vivification -eliminateLit -litImplied -iterate=10"
+    },
+    "asp": {
+      "encodings": [
+          {
+            "file": "./guess_min_degree.lp",
+            "size": 95,
+            "timeout": 10
+          },
+          {
+            "file": "./guess_increase.lp",
+            "size": 64,
+            "timeout" : 35
+          }
+      ]
+    }
   }
 }

dpdb/abstraction.py

@@ -1,4 +1,3 @@
-# -*- coding: future_fstrings -*-
 import clingo
 import importlib
 import logging
@@ -150,13 +149,13 @@ def choose_subset(self, select_subset, encodingFile, timeout=30, usc=False, solv
         c = clingoctl
 
         aset = [sys.maxsize, False, [], None, []]
-        
+
         def __on_model(model):
             #if len(model.cost) == 0:
             #    return
-            
+
             logger.debug("better answer set found: %s %s %s", model, model.cost, model.optimality_proven)
-            
+
             aset[1] |= model.optimality_proven
             opt = model.cost[0] if len(model.cost) > 0 else 0
             if opt <= aset[0]:
@@ -173,7 +172,7 @@ def __on_model(model):
 
         # FIXME: use mutable string
         prog = encodingContent
-        
+
         if clingoctl is None:
             c = clingo.Control()
 
@@ -190,7 +189,7 @@ def __on_model(model):
             for p in self._nodes:
                 prog += "p({0}).\n".format(p)
 
-            # subset (buckets) of proj to select upon 
+            # subset (buckets) of proj to select upon
             #for b in range(1, select_subset + 1, 1):
             prog += "b({0}).\n".format(select_subset)
             #print(prog)
@@ -391,4 +390,3 @@ def normalize(self):
         self.normalized_nodes = normalized_nodes
         self.normalized_adj = normalized_adj
         self.normalized_edges = normalized_edges
-

dpdb/db.py

@@ -1,4 +1,3 @@
-# -*- coding: future_fstrings -*-
 import logging
 import select
 import re
@@ -37,7 +36,7 @@ def from_pool(cls, pool):
         instance = cls()
         instance._pool = pool
         instance._conn = pool.getconn()
-        return instance 
+        return instance
 
     # we need this wrapper because conn object is required
     def __debug_query__ (self, query, params = []):
@@ -86,7 +85,7 @@ def exec_and_fetch(self,q,p = []):
                 return cur.fetchone()
         except pg.errors.AdminShutdown:
             logger.warning("Connection closed by admin")
-        
+
     def exec_and_fetch_all(self,q,p = []):
         try:
             self.__debug_query__(q,p)

dpdb/problem.py

@@ -1,4 +1,3 @@
-# -*- coding: future_fstrings -*-
 import logging
 import os
 import signal
@@ -255,7 +254,7 @@ def init_problem():
                 [self.name,self.type,self.td.num_bags,self.td.tree_width,self.td.num_orig_vertices,self.td.root.id],"id")[0]
             self.set_id(problem_id)
             logger.info("Created problem with ID %d", self.id)
-            
+
         def drop_tables():
             logger.debug("Dropping tables")
             self.db.drop_table("td_bag")
@@ -310,7 +309,7 @@ def create_tables_for_node(n, workers = {}):
             db.create_view(f"td_node_{n.id}_v", ass_view)
             if "parallel_setup" in self.kwargs and self.kwargs["parallel_setup"]:
                 db.close()
-            
+
         def insert_data():
             logger.debug("Inserting problem data")
             self.db.ignore_next_praefix(3)
@@ -436,4 +435,3 @@ def solve_node(self, node, db):
             row_cnt = db.last_rowcount
             db.update("td_node_status",["end_time","rows"],["statement_timestamp()",str(row_cnt)],[f"node = {node.id}"])
         db.commit()
-

dpdb/problems/nestpmc.py

@@ -1,4 +1,3 @@
-# -*- coding: future_fstrings -*-
 import logging
 import subprocess
 from collections import defaultdict
@@ -45,7 +44,7 @@ def __init__(self, name, pool, max_solver_threads=12, inner_vars_threshold=0, st
 
     def td_node_column_def(self,var):
         return td_node_column_def(var)
-        
+
     def td_node_extra_columns(self):
         return [("model_count","NUMERIC")]
 

dpdb/problems/pmc.py

@@ -1,4 +1,3 @@
-# -*- coding: future_fstrings -*-
 import logging
 from collections import defaultdict
 
@@ -15,7 +14,7 @@ def __init__(self, name, pool, store_formula=False, **kwargs):
 
     def td_node_column_def(self,var):
         return td_node_column_def(var)
-        
+
     def filter(self,node):
         return filter(self.var_clause_dict, node)
 

dpdb/problems/pmcext.py

@@ -1,4 +1,3 @@
-# -*- coding: future_fstrings -*-
 import logging
 import subprocess
 from collections import defaultdict
@@ -27,7 +26,7 @@ def __init__(self, name, pool, max_solver_threads=12, store_formula=False, **kwa
 
     def td_node_column_def(self,var):
         return td_node_column_def(var)
-        
+
     def td_node_extra_columns(self):
         return [("model_count","NUMERIC")]
 

dpdb/problems/sat.py

@@ -1,4 +1,3 @@
-# -*- coding: future_fstrings -*-
 import logging
 from collections import defaultdict
 
@@ -16,7 +15,7 @@ def __init__(self, name, pool, store_formula=False, **kwargs):
 
     def td_node_column_def(self,var):
         return td_node_column_def(var)
-        
+
     def filter(self,node):
         return filter(self.var_clause_dict, node)
 

dpdb/problems/sat_util.py

@@ -1,4 +1,3 @@
-# -*- coding: future_fstrings -*-
 from dpdb.problem import *
 from collections import defaultdict
 

dpdb/problems/sharpsat.py

@@ -1,4 +1,3 @@
-# -*- coding: future_fstrings -*-
 import logging
 from collections import defaultdict
 
@@ -19,7 +18,7 @@ def td_node_column_def(self,var):
 
     def td_node_extra_columns(self):
         return [("model_count","NUMERIC")]
-        
+
     def candidate_extra_cols(self,node):
         return ["{} AS model_count".format(
                 " * ".join(set([var2cnt(node,v) for v in node.vertices] +
@@ -91,4 +90,3 @@ def node2cnt(node):
         )
     }
 )
-

dpdb/problems/sharpsatext.py

@@ -1,4 +1,3 @@
-# -*- coding: future_fstrings -*-
 import clingo
 import logging
 import subprocess
@@ -31,7 +30,7 @@ def __init__(self, name, pool, max_solver_threads=12, store_formula=False, **kwa
 
     def td_node_column_def(self,var):
         return td_node_column_def(var)
-        
+
     def td_node_extra_columns(self):
         return [("model_count","NUMERIC")]
 

dpdb/problems/vertexcover.py

@@ -1,4 +1,3 @@
-# -*- coding: future_fstrings -*-
 import logging
 
 from dpdb.reader import TdReader, TwReader, EdgeReader
@@ -17,7 +16,7 @@ def td_node_column_def(self,var):
 
     def td_node_extra_columns(self):
         return [("size","INTEGER")]
-        
+
     def candidate_extra_cols(self,node):
         introduce = [var2size(node,v) for v in node.vertices if node.needs_introduce(v)]
         join = [node2size(n) for n in node.children]
@@ -32,7 +31,7 @@ def candidate_extra_cols(self,node):
             if len(join) > 1:
                 children = [vc for c in node.children for vc in c.vertices if vc in node.vertices]
                 duplicates = ["case when {} then 1 else 0 end * {}".format(
-                                    var2tab_col(node,var,False),len(node.vertex_children(var))-1) 
+                                    var2tab_col(node,var,False),len(node.vertex_children(var))-1)
                                 for var in set(children) if len(node.vertex_children(var)) > 1]
                 # subtract vertices counted multiple times
                 if duplicates:
@@ -116,4 +115,3 @@ def node2size(node):
         )
     }
 )
-

helper.py

@@ -0,0 +1,25 @@
+#!/usr/bin/env python3
+
+import os
+
+def absolutizePath(relPath): # paths in config may be relative to root of repository
+    return os.path.abspath(os.path.join(os.path.dirname(__file__), relPath))
+
+def absolutizePaths(object): # returns new config in which all paths are absolute
+    if isinstance(object, str): # base case
+        return object
+    else:
+        assert isinstance(object, dict), object # config
+        absCfg = {} # new config with absolute paths, to be returned
+        for (key, value) in object.items():
+            assert isinstance(key, str), key
+            if key in {"path", "file"}:
+                assert isinstance(value, str), value
+                absCfg[key] = absolutizePath(value)
+            elif isinstance(value, dict):
+                absCfg[key] = absolutizePaths(value)
+            elif isinstance(value, list): # possibly `list` of `str`
+                absCfg[key] = [absolutizePaths(member) for member in value]
+            else: # base case
+                absCfg[key] = value
+        return absCfg