pibase_open

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

README (3240B)

      1 A project to generate "open problems" for the data of pibase
      2 <https://github.com/pi-base/data>. Pibase contains:
      3 
      4 - properties, that have a name
      5 - spaces, that have a partial valuation of properties (i.e., a list of positive
      6   and negative properties)
      7 - theorems, that say that a conjunction of properties (positive or negative)
      8   implies a conjunction of properties (positive or negative)
      9 
     10 An "open problem" is a partial valuation of properties which is minimal under
     11 inclusion and satisfies:
     12 
     13 - it is satisfiable, i.e., can be extended to a complete valuations that
     14   satisfies the theorems
     15 - it is not covered by a known space
     16 
     17 This code generates open problems. Here is how to use it:
     18 
     19 - store the pibase github repository in ~/apps/data
     20 
     21 - run ./get_properties.sh > properties
     22 
     23 The file "properties" will now contain a list of lines of the form:
     24 
     25   "Pxyz human-readable name"
     26 
     27 where Pxyz is the property identifier
     28 
     29 - run ./get_spaces.sh > spaces
     30 
     31 The file "spaces" will now contain a list of lines of the form:
     32   
     33   "Sxyz Qa Qb Qc"
     34 
     35 where Sxyz is the space identifier and each Qx is either of the form Pxyz (a
     36 property) or -Pxyz (the negation of a property)
     37 
     38 - run ./get_theorems.sh > theorems
     39 
     40 The file "theorems" will now contain a list of lines of the form:
     41 
     42   Txyz Qa Qb Qc
     43 
     44 Where each theorem with identifier Txyz is rewritten to as many copies as it has
     45 consequences (i.e., a b => d e f gets rewritten to a b => d, a b => e, a b => f)
     46 and each of these consequences is written as a disjunctive clause, i.e.,
     47 a b -c => d is written as -a -b c d.
     48 
     49 Hence, the whole file theorems is a Boolean CNF formula.
     50 
     51 - run ./explore.py
     52 
     53 This will first "complete" the properties of the space, generating a file
     54 "full_spaces" with lines of the same form as "spaces" that contain all
     55 properties that logically follow from the known properties given the theorems.
     56 The algorithm is that, for each property p such the space neither has p nor -p,
     57 we run a SAT solver on the theorems plus the known properties plus p, and
     58 another SAT solver on the theorems plus the known properties plus -p. If the
     59 first (resp second) call is unsatisfiable, then -p (resp p) is added.
     60 
     61 IMPORTANT: the file "full_spaces" should be removed whenever the list of
     62 properties, spaces, or theorems is changed!
     63 
     64 Next, "explore.py" performs a BFS on the partial valuations of properties (in
     65 increasing order) and outputs the open problems. Here is the algorithm:
     66 
     67 - if a partial valuation covers a previously printed open problem, stop
     68   exploring this partial valuation
     69   (i.e., if "-b c" was reported as an open problem then "a -b c" should not be
     70   explored)
     71 
     72 - else, if the partial valuation is unsatisfiable (checked with a SAT solver on
     73   the partial valuation plus the theorems), then stop exploring this partial
     74   valuation
     75 
     76 - else, if the partial valuation is not covered by any space (remembering that
     77   they have been completed), then we have found a minimal open problem: output
     78   it and stop exploring
     79 
     80 - otherwise, do not print the partial valuation, but try all possible ways to
     81   extend it (by adding a property greater than the greatest property in the
     82   valuation, with either positive or negative polarity) and add all such results
     83   to the BFS's queue
     84