Nesthdb

config.json

@@ -24,7 +24,63 @@
       "--child-limit","5"
     ]
   },
+  "problem_specific": {
+    "nestpmc": {
+      "max_solver_threads": 4,
+      "inner_vars_threshold": 10,
+      "max_worker_threads": 4
+    }
+  },
   "dpdb": {
-    "max_worker_threads": 24
-  }
+  },
+	"nesthdb": {
+		"threshold_hybrid" : 45,
+		"threshold_abstract" : 8,
+		"max_recursion_depth" : 1,
+		"sat_solver": {
+			"path": "/home/rafael/projects/dp_on_dbs/picosat-965/picosat",
+			"seed_arg": "-s"
+		},
+		"sharpsat_solver": {
+			"path": "/home/rafael/projects/miniC2D2/bin/linux/miniC2D",
+			"args": "-C -c",
+			"output_parser": {
+				"class": "RegExReader",
+				"args": {
+					"pattern": "Counting... (\\d+) models"
+				},
+				"result":"result"
+			}
+		},
+        "preprocessor": {
+            "path": "./pmc_linux",
+	        "args": "-vivification -eliminateLit -litImplied -iterate=10"
+        },
+        "alt_preprocessor": {
+            "path": "../Riss/coprocessor",
+            "args": "-enabled_cp3 -up -subsimp -bve -no-bve_gates -no-bve_strength -bve_red_lits=1 -cp3_bve_heap=1 -bve_heap_updates=1 -bve_totalG -bve_cgrow_t=1000 -bve_cgrow=10"
+        },
+		"pmc_solver": {
+			"path": "/home/rafael/projects/g2/build/ganak",
+			"output_parser": {
+				"class": "RegExReader",
+				"args": {
+					"pattern": "s pmc (\\d+)"
+				},
+				"result":"result"
+			}
+		},
+		"asp": {
+			"encodings": [{ 
+				"file": "./guess_min_degree.lp",
+				"size": 95,
+				"timeout": 10
+			},
+			{ 
+				"file": "./guess_increase.lp",
+				"size": 64,
+				"timeout" : 35
+			}]
+		}
+	}
 }

dpdb/problem.py

@@ -186,7 +186,6 @@ def assignment_select(self,node):
             sel_list += "{}{}".format(", " if sel_list else "", ",".join(extra_cols))
 
         candidates_sel = self.candidates_select(node)
-
         if self.candidate_store == "cte":
             q = f"WITH candidate AS ({candidates_sel}) SELECT {sel_list} FROM candidate"
         elif self.candidate_store == "subquery":

dpdb/problems/nestpmc.py

@@ -65,7 +65,7 @@ def candidates_select(self,node):
             extra_proj = []
         q = ""
 
-        if any(node.needs_introduce(v) for v in node.vertices):
+        if any(node.needs_introduce(v) for v in node.vertices + extra_proj):
             q += "WITH introduce AS ({}) ".format(self.introduce(node))
 
         q += "SELECT {}".format(

dpdb/reader.py

@@ -159,6 +159,12 @@ def store_problem_vars(self):
         else:
             self.num_vars = int(self._problem_vars[0])
             self.num_clauses = int(self._problem_vars[1])
+            if self.num_vars == 0:
+                self.models = 0
+                self.maybe_sat = False
+                if not self.silent:
+                    logger.info("Problem has 0 models (solved by pre-processing)")
+                self.done = True
 
     def read_terminated(self, lines, line, lineno):
         i = 1
@@ -182,7 +188,6 @@ def body(self, lines):
 
         maxvar = 0
         #projected_vars = set()
-
         for lineno, line in enumerate(lines):
             if not line or self.is_comment(line):
                 continue
@@ -241,7 +246,10 @@ def body(self, lines):
 
         for clause in self.clauses:
             self.vars.update([abs(lit) for lit in clause])
-        maxvar = max(maxvar,max(self.vars))
+        if len(self.vars) == 0:
+            maxvar = 0
+        else:
+            maxvar = max(maxvar,max(self.vars))
 
         self.single_vars = set((abs(l) for l in self.single_clauses))
         self.projected = self.projected.difference(self.single_vars)

nesthdb.py

@@ -108,6 +108,47 @@ def __init__(self, formula, non_nested, depth=0, **kwargs):
 
     def preprocess(self):
         global cfg
+        if "alt_preprocessor" in cfg["nesthdb"]:
+            cfg_prep = cfg["nesthdb"]["alt_preprocessor"]
+            preprocessor = [cfg_prep["path"]]
+            preprocessor.extend(cfg_prep["args"].split(' '))
+            tmp = tempfile.NamedTemporaryFile().name
+            preprocessor.append(f"-whiteList={tmp}")
+            ret = tempfile.NamedTemporaryFile().name
+            preprocessor.append(f"-dimacs={ret}")
+            clauses,proj_vars,num_vars,mapping,rev_mapping = normalize_cnf(self.formula.clauses, self.projected, True)
+            with FileWriter(tmp) as fw:
+                for p in proj_vars:
+                    fw.writeline(str(p))
+            self.active_process = ppmc = subprocess.Popen(preprocessor,stdin=subprocess.PIPE, stdout=subprocess.DEVNULL, stderr=subprocess.DEVNULL)
+            StreamWriter(ppmc.stdin).write_cnf(self.formula.num_vars,clauses,normalize=False)
+            ppmc.stdin.close()
+            ppmc.wait()
+            input = CnfReader.from_file(ret,silent=True)
+            self.active_process = None
+            if not input.error:
+                self.maybe_sat = input.maybe_sat
+                if not input.done:
+                    # fix corner case, where input.vars contains not all of range(1,input.max_vars+1)
+                    clauses, vars, proj_vars = denormalize_cnf(input.clauses,input.vars,proj_vars,rev_mapping)
+                    self.formula = Formula(vars,clauses)
+                    self.projected = proj_vars.intersection(vars)
+                    # remove single_clause_proj_vars, they are not needed/relevant and only waste resources!
+                    # consequently, these variables are treated as if they were never there, no 2 ** correction!
+                    _, singles, _ = denormalize_cnf((),input.single_vars,(),rev_mapping)
+                    self.projected_orig = self.projected_orig.difference(singles)
+                else:
+                    # set models to 1 if instance was sat
+                    if len(self.projected) == 0:
+                        self.models = 1
+                    # use result if instance was #sat
+                    elif self.projected.intersection(self.formula.vars) == self.formula.vars:
+                        self.models = input.models
+                    # dont use result if instance was pmc
+                    else:
+                        pass
+            else:
+                logger.debug("Pre-processor failed... ignoring result")
         if "preprocessor" not in cfg["nesthdb"]:
             return # True, num_vars, vars, len(clauses), clauses, None
         cfg_prep = cfg["nesthdb"]["preprocessor"]