OKlibrary  0.2.1.6
Hardness.hpp File Reference

Investigations regarding hardness of pigeonhole clause-sets. More...

Go to the source code of this file.


Detailed Description

Investigations regarding hardness of pigeonhole clause-sets.

Todo:
Influence of totally blocked clauses
  • For unsatisfiable clause-sets addition of totally blocked clauses does not influence the hardness:
    for n : 0 thru 4 do print(n,hardness_u_cs(weak_php_cs(n+1,n)));
    0 0
    1 1
    2 2
    3 3
    4 4
    
    for n : 0 thru 4 do print(n,hardness_u_cs(special_php_cs(n+1,n)));
    0 0
    1 1
    2 2
    3 3
    4 4
    
    for n : 0 thru 4 do print(n,hardness_u_cs(special_php_cs(n+2,n)));
    0 0
    1 1
    2 2
    3 3
    4 4
    
    for n : 1 thru 5 do print(n,hardness_u_cs(special_php_cs(n-1,n)));
    1 0
    2 1
    3 2
    4 3
    5 4
    
    for n : 2 thru 6 do print(n,hardness_u_cs(special_php_cs(n-2,n)));
    2 0
    3 1
    4 2
    5 3
    6 4
       
    The special PHP-clause-sets are not obtained by addition of blocked clauses from the weak PHP-clause-sets, since the AMO-clauses can be resolved with the long hole-clauses, but as the above experiments shows, even for that form the hardness is not influenced.
  • For satisfiable clause-sets:
    for n : 0 thru 4 do print(n,hardness_cs(weak_php_cs(n,n)));
    0 0
    1 0
    2 1
    3 2
    # aborted
    
    for n : 0 thru 4 do print(n,hardness_cs(strong_php_cs(n,n)));
    0 0
    1 0
    2 1
    3 2
    4 3
    
    for n : 0 thru 4 do print(n,hardness_cs(dual_strong_php_cs(n,n)));
    0 0
    1 0
    2 1
    3 1
    4 2
    
    for n : 0 thru 5 do print(n,hardness_cs(special_php_cs(n,n)));
    0 0
    1 0
    2 1
    3 1
    4 1
    # n=5: reached memory limit with heap_size_ecl_okl=10^9 (after several days)
       

Definition in file Hardness.hpp.