OKlibrary  0.2.1.6
SingularDP.hpp File Reference

Plans regarding singular DP-reduction for minimal unsatisfiable clause-sets. More...

Go to the source code of this file.


Detailed Description

Plans regarding singular DP-reduction for minimal unsatisfiable clause-sets.

Todo:
Are non-1-singular tuples totally singular?
  • Let's abbreviate this conjecture with "n1stts".
  • Assuming that T is a singular tuple for F:
    counterexample_n1stts(T,F) := singulartuple_csp(T,F) and
     notonesingulartuple_csp(T,F) and not totally_singulartuple_csp_bydef(T,F)$
       
  • For n <= 6 (num_all_smusat1(6) = 95040):
    all_n_n1stts(n) := block([m:0, S],
     for F in all_smusat1_cs(n) do (
      S : maxnotonesdpst_cs_bydef(F),
      if length(S) > m then m : length(S),
      for t in S do (
       if not subsetp(permutations(t),S) then print("COUNTEREXAMPLE:",F,t)
      )),
     m)$
       
    No counterexample for n <= 5 (return for n=5: 24). And that is true, since the conjecture is true for saturated F, since there a non-1-singular tuple contains only non-1-singular variables from F.
Todo:
Special properties of the greedoid of singular sets
  • F : {{1,2},{-1,3},{-1,-3},{-2,4},{-2,-4}};
    min_unsat_bydef_cs(F);
      true
    deficiency_cs(F);
      1
    G : sdphg_cs_bydef(F);
      [{1,2,3,4},
       {{},{1},{1,2,3},{1,2,3,4},{1,2,4},{1,3},{1,3,4},{1,4},{2},{2,3},{2,3,4},{2,4},{3},{3,4},{4}}]
    grdfs_p(G);
      true
    antimtrfs_p(G);
      false
    rank_grdfs(G);
      6
    bases_grdfs(G);
      {{1,2,3,4}}
    intervalgrdfs_p(G);
      false
    gaussian_ss_p(G[2]);
      true
       
  • F : {{1,2},{-1,3},{-2,4},{-3,5},{-3,-5},{-4,6},{-4,-6}};
    min_unsat_bydef_cs(F);
      true
    deficiency_cs(F);
      1
    G : sdphg_cs_bydef(F);
    [{1,2,3,4,5,6},
     {{},{1},{1,2},{1,2,3},{1,2,3,4,5},{1,2,3,4,5,6},{1,2,3,4,6},{1,2,3,5},{1,2,3,5,6},
      {1,2,3,6},{1,2,4},{1,2,4,5},{1,2,4,5,6},{1,2,4,6},{1,2,5},{1,2,5,6},{1,2,6},{1,3},{1,3,4},
      {1,3,4,5},{1,3,4,5,6},{1,3,4,6},{1,3,5},{1,3,5,6},{1,3,6},{1,4},{1,4,5},{1,4,5,6},{1,4,6},
      {1,5},{1,5,6},{1,6},{2},{2,3},{2,3,4},{2,3,4,5},{2,3,4,5,6},{2,3,4,6},{2,3,5},{2,3,5,6},
      {2,3,6},{2,4},{2,4,5},{2,4,5,6},{2,4,6},{2,5},{2,5,6},{2,6},{3},{3,4},{3,4,5},{3,4,5,6},
      {3,4,6},{3,5},{3,5,6},{3,6},{4},{4,5},{4,5,6},{4,6},{5},{5,6},{6}}]
    grdfs_p(G);
      true
    antimtrfs_p(G);
      false
    rank_grdfs(G);
      6
    bases_grdfs(G);
      {{1,2,3,4,5,6}}
    intervalgrdfs_p(G);
      false
    gaussian_ss_p(G[2]);
      true
       
  • So is every such greedoid Gaussian ?!

Definition in file SingularDP.hpp.