diff --git a/config.json b/config.json index d91a86f..dbb5af5 100644 --- a/config.json +++ b/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 + }] + } + } } diff --git a/dpdb/problem.py b/dpdb/problem.py index 7adb1d6..7567298 100644 --- a/dpdb/problem.py +++ b/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": diff --git a/dpdb/problems/nestpmc.py b/dpdb/problems/nestpmc.py index ffb4868..5be00a5 100644 --- a/dpdb/problems/nestpmc.py +++ b/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( diff --git a/dpdb/reader.py b/dpdb/reader.py index a679b4b..b126128 100644 --- a/dpdb/reader.py +++ b/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) diff --git a/nesthdb.py b/nesthdb.py index c4b8ea0..f7740c4 100644 --- a/nesthdb.py +++ b/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"]