OKlibrary  0.2.1.6
Glucose.hpp File Reference

General plans monitoring glucose and glucose-2.0. More...

Go to the source code of this file.


Detailed Description

General plans monitoring glucose and glucose-2.0.

Todo:
Extracted data attribute names
  • A typical glucose run on PHP(5,4):
    maxima> output_weak_php(6,5,"PHP_6_5.cnf");
    > glucose PHP_6_5.cnf
    
    c This is glucose 1.0 --  based on MiniSAT (Many thanks to MiniSAT team)
    
    c ============================[ Problem Statistics ]=============================
    c |                                                                             |
    c |  Number of variables:  30                                                   |
    c |  Number of clauses:    81                                                   |
    c |  Parsing time:         0.00         s                                       |
    ============================[ Search Statistics ]==============================
    | Conflicts |          ORIGINAL         |          LEARNT          | Progress |
    |           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
    ===============================================================================
    |         0 |      30       81      180 |       27        0   -nan |  0.000 % |
    ===============================================================================
    c restarts              : 1
    c nb ReduceDB           : 0
    c nb learnts DL2        : 15
    c nb learnts size 2     : 11
    c nb learnts size 1     : 4
    c conflicts             : 139            (inf /sec)
    c decisions             : 162            (1.23 % random) (inf /sec)
    c propagations          : 800            (inf /sec)
    c conflict literals     : 868            (19.63 % deleted)
    c Memory used           : 1.88 MB
    c CPU time              : 0 s
    
    s UNSATISFIABLE
       
  • A typical glucose-2.0 run:
    maxima> output_weak_php(6,5,"PHP_6_5.cnf");
    > glucose-2.0 PHP_6_5.cnf
    
    c This is glucose 2.0 --  based on MiniSAT (Many thanks to MiniSAT team)
    c WARNING: for repeatability, setting FPU to use double precision
    c ============================[ Problem Statistics ]=============================
    c |                                                                             |
    c |  Number of variables:            30                                         |
    c |  Number of clauses:              81                                         |
    c |  Parse time:                   0.00 s                                       |
    c |                                                                             |
    c ============================[ Search Statistics ]==============================
    c | Conflicts |          ORIGINAL         |          LEARNT          | Progress |
    c |           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
    c ===============================================================================
    c |       148 |       4       79      170 |        0       35      5 | 86.667 % |
    c ===============================================================================
    c restarts              : 1
    c nb ReduceDB           : 0
    c nb removed Clauses    : 0
    c nb learnts DL2        : 22
    c nb learnts size 2     : 12
    c nb learnts size 1     : 6
    c conflicts             : 148            (inf /sec)
    c decisions             : 198            (0.00 % random) (inf /sec)
    c propagations          : 956            (inf /sec)
    c conflict literals     : 879            (17.15 % deleted)
    c nb reduced Clauses    : 32
    c CPU time              : 0 s
    
    s UNSATISFIABLE
       
  • We see that the two key differences in output are
    • "Parsing time" for glucose vs "Parse time" for glucose-2.0.
    • "Memory used" isn't given by glucose-2.0 but is by glucose.
    • "nb removed Clauses" isn't given by glucose but is by glucose-2.0.
  • As there are only minor differences, as well as the fact that glucose is deprecated in favour of glucose-2.0, it seems best to have just one script that handles both glucose and glucose-2.0.
  • We now have ExtractGlucose:
    maxima> output_weak_php(6,5,"PHP_6_5.cnf");
    > glucose PHP_6_5.cnf | ExtractGlucose
    rn rc t sat cfs dec rts r1 mem ptime cfl rdb rrc ldlc l2c l1c
    30 81 0 0 139 162 1 800 1.88 0.00 868 0 0 15 11 4
    
    > glucose-2.0 PHP_6_5.cnf | ExtractGlucose
    rn rc t sat cfs dec rts r1 mem ptime cfl rdb rrc ldlc l2c l1c
    30 81 0 0 148 198 1 956 0 0.00 879 0 0 22 12 6
       
  • Attributes that are given by glucose but not glucose-2.0 or vice-versa are given default "zero" values.
  • We have the following attributes:
    • rn : the (solver-specific) number of variables.
    • rc : the (solver-specific) number of clauses.
    • t : the time taken in seconds.
    • sat: satisfiable (1), unsatisfiable (0), UNKNOWN (2).
    • cfs : number of conflicts.
    • dec: number of decisions.
    • rts: number of restarts.
    • r1: number of unit-clauses propagated.
    • mem: memory used in MB.
    • ptime: time spent preprocessing in seconds.
    • cfl: number of conflict literals.
    • rdb: number of "ReduceDB" calls.
    • rrc: number of "removed clauses".
    • ldlc: number of learnt clauses "DL2".
    • l2c: number of learnt clauses of size 2.
    • l1c: number of learnt clauses of size 1.
  • We should investigate:
    • What is "ReduceDB"?
    • When are clauses "removed" and why?
    • What is DL2?
  • We need full explanations for each of these attributes in the docus.

Definition in file Glucose.hpp.