pibase_open

find open problems in topology from pibase
git clone https://a3nm.net/git/pibase_open/
Log | Files | Refs | README

explore.py (3576B)

      1 #!/usr/bin/python3
      2 
      3 import pycosat
      4 from collections import deque
      5 
      6 properties = {}
      7 n = 1
      8 pn = {}
      9 pnr = {}
     10 
     11 with open("properties", 'r') as pf:
     12     for l in pf.readlines():
     13         f = l.strip().split(' ')
     14         properties[f[0]] = ' '.join(f[1:])
     15         pn[n] = f[0]
     16         pnr[f[0]] = n
     17         n += 1
     18 
     19 def props_to_nums(xx):
     20     return [-pnr[x[1:]] if x[0] == '-' else +pnr[x] for x in xx]
     21 
     22 def props_to_names(xx):
     23     return ["NOT " + properties[x[1:]] + " (" + x[1:] + ")" if x[0] == '-'
     24             else properties[x] + " (" + x + ")" for x in xx]
     25 
     26 clauses = []
     27 with open("theorems", 'r') as pf:
     28     for l in pf.readlines():
     29         f = l.strip().split(' ')
     30         cl = props_to_nums(f[1:])
     31         clauses.append(cl)
     32 
     33 try:
     34     spaces = {}
     35     with open("full_spaces", 'r') as pf:
     36         for l in pf.readlines():
     37             f = l.strip().split(' ')
     38             spaces[f[0]] = set(f[1:])
     39 except FileNotFoundError: 
     40     # do the completion
     41     spaces = {}
     42     with open("spaces", 'r') as pf:
     43         for l in pf.readlines():
     44             f = l.strip().split(' ')
     45             spaces[f[0]] = set(f[1:])
     46     with open("full_spaces", 'w') as pw:
     47         for s in spaces.keys():
     48             completion = set()
     49             ss = spaces[s]
     50             cl = [[x] for x in props_to_nums(ss)]
     51             for p in properties.keys():
     52                 if p not in ss and ("-" + p) not in ss:
     53                     res_pos = pycosat.solve(clauses + cl + [props_to_nums([p])])
     54                     res_neg = pycosat.solve(clauses + cl +
     55                             [props_to_nums(["-"+p])])
     56                     res_pos2 = (res_pos == "UNSAT")
     57                     res_neg2 = (res_neg == "UNSAT")
     58                     assert(not (res_pos2 and res_neg2))
     59                     if res_pos2:
     60                         completion.add("-"+p)
     61                     if res_neg2:
     62                         completion.add(p)
     63             spaces[s] = spaces[s].union(completion)
     64             print(s + " " + " ".join(spaces[s]), file=pw)
     65 
     66 outputs = set()
     67 q = deque([()])
     68 while q:
     69     pref = q.popleft()
     70 
     71     # is it redundant? (does it cover an existing output?)
     72     # TODO: this is super naive, we can probably do better
     73     covers_one_out = False
     74     for o in outputs:
     75         covered = True
     76         for op in o:
     77             if op not in pref:
     78                 covered = False
     79                 break
     80         if covered:
     81             covers_one_out = True
     82             break
     83     if covers_one_out:
     84         continue # do not investigate this
     85 
     86     # is it consistent?
     87     res = pycosat.solve(clauses + [[x] for x in props_to_nums(pref)])
     88     if res == "UNSAT":
     89         continue # forget about this
     90 
     91     # is it covered by a known space?
     92     covered_by_one = False
     93     for s in spaces.keys():
     94         ss = spaces[s]
     95         covered = True
     96         for p in pref:
     97             if p not in ss:
     98                 covered = False
     99                 break
    100         if covered:
    101             covered_by_one = True
    102             break
    103     if not covered_by_one:
    104         # it is not covered, we have a minimal open problem:
    105         print (" AND ".join(props_to_names(pref)))
    106         outputs.add(tuple(pref))
    107         continue
    108 
    109     # not redundant, consistent, but covered: continue exploring
    110     for p in properties.keys():
    111         if (len(pref) > 0):
    112             nlast = pref[-1] if pref[-1][0] != "-" else pref[-1][1:]
    113             if p <= nlast:
    114                 continue # add properties in increasing order
    115         if p not in pref and ("-" + p) not in pref:
    116             q.append(pref + (p,))
    117             q.append(pref + ("-" + p,))
    118 
    119