Git Product home page Git Product logo

Comments (2)

shnarazk avatar shnarazk commented on June 12, 2024

Multiply LBD with RCC

1: origin

T56.2.0.cnf                                3145220,10854665 |time:   422.32
 #conflict:     285954, #decision:      1139695, #propagate:      809410366 
  Assignment|#rem:   693206, #fix:    36609, #elm:  2415405, prg%:  77.9600 
 Clause Kind|Remv:    72866, LBD2:    29178, Binc:    14621, Perm:  4992586 
     Restart|#BLK:     1852, #RST:     1209, eASG:   0.5452, eLBD:   0.6881 
    Conflict|aLBD:     5.56, cnfl:    69.26, bjmp:    66.33, rpc%:   0.4228 
   Clause DB|#rdc:       13, #sce:      197 |blkR:   1.4000, frcK:   0.8032 

10-3-13.cnf                                    29772,922204 |time:  1001.97
 #conflict:    2890000, #decision:      6260488, #propagate:     1331423143 
  Assignment|#rem:    25425, #fix:     2948, #elm:     1399, prg%:  14.6010 
 Clause Kind|Remv:   224907, LBD2:     7193, Binc:     1750, Perm:   895383 
     Restart|#BLK:     3079, #RST:    22938, eASG:   1.0406, eLBD:   1.5704 
    Conflict|aLBD:    52.17, cnfl:    75.80, bjmp:    74.72, rpc%:   0.7937 
   Clause DB|#rdc:       49, #sce:      306 |blkR:   1.4000, frcK:   0.9496

2 generous guard: threshold * RCC.trend() < LBD.trend()

T56.2.0.cnf                                3145220,10854665 |time:   459.30
 #conflict:     305284, #decision:      1294943, #propagate:      823134138 
  Assignment|#rem:   748302, #fix:     7267, #elm:  2389651, prg%:  76.2083 
 Clause Kind|Remv:   103271, LBD2:    28351, Binc:    14078, Perm:  5467068 
     Restart|#BLK:     2157, #RST:     1343, eASG:   0.1312, eLBD:   1.0176 
    Conflict|aLBD:     9.41, cnfl:    65.28, bjmp:    62.96, rpc%:   0.4399 
   Clause DB|#rdc:       12, #sce:      200 |blkR:   1.4000, frcK:   0.8814 

10-3-13.cnf                                    29772,922204 |time:  1002.56
 #conflict:    4250000, #decision:      9760765, #propagate:     1666401649 
  Assignment|#rem:    25201, #fix:     3172, #elm:     1399, prg%:  15.3534 
 Clause Kind|Remv:   329709, LBD2:    11859, Binc:     2623, Perm:   890640 
     Restart|#BLK:     7804, #RST:    15113, eASG:   0.8011, eLBD:   1.7488 
    Conflict|aLBD:    50.88, cnfl:   514.50, bjmp:   512.44, rpc%:   0.3556 
   Clause DB|#rdc:       56, #sce:      452 |blkR:   1.4000, frcK:   0.9797 
    Strategy|mode: ERROR

3 evacuater: threshold < LBD.trend() * RCC.trend()

T56.2.0.cnf                                3145220,10854665 |time:   535.49
 #conflict:     301611, #decision:      1292338, #propagate:      998491152 
  Assignment|#rem:   717175, #fix:    38633, #elm:  2389412, prg%:  77.1979 
 Clause Kind|Remv:    63449, LBD2:    29231, Binc:    15331, Perm:  5212232 
     Restart|#BLK:     2045, #RST:     1502, eASG:   0.5945, eLBD:   0.6225 
    Conflict|aLBD:     4.56, cnfl:    80.86, bjmp:    78.28, rpc%:   0.4980 
   Clause DB|#rdc:       12, #sce:      160 |blkR:   1.4000, frcK:   0.7837 ```

from splr.

shnarazk avatar shnarazk commented on June 12, 2024

RCC as var reward

from splr.

Related Issues (20)

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.