OKlibrary  0.2.1.6
general.hpp File Reference

Plans for Maxima-components regarding SAT-reductions (in general) More...

Go to the source code of this file.


Detailed Description

Plans for Maxima-components regarding SAT-reductions (in general)

Packaging of reductions into some "preprocessing" is handled in Satisfiability/Lisp/Preprocessing.

Todo:
Compute propagation-hardness
  • We should provide functions phardness_wpi_cs and phardness_cs.
Todo:
DONE (function hardness_wpi_cs has been provided) Computing the hardness of a clause-set representation
  • NEEDS UPDATE.
  • See "Hardness of boolean function representations" in Experimentation/Investigations/BooleanFunctions/plans/general.hpp.
  • To compute the hardness of a clause-set F we can do the following:
    /* Computing the hardness of a clause-set F with its prime implicates F_PI
       as input. */
    hardness_wpi_cs(F,F_PI) := block([max_k : 0, count : 0, maxcount : length(F_PI)],
      maxcount : length(F_PI),
      for C in F_PI do (
        count : count + 1,
        if mod(count, 50) = 0 then
          print(sconcat("[",count,"/",maxcount,"] Hardness(F) >= ", max_k," ...")),
        for k : 0 while generalised_ucp(apply_pa(comp_sl(C),F),k) # {{}} do
          max_k : max(max_k, k + 1)),
      return(max_k))$
    
    hardness_cs(F) := hardness_wpi_cs(F,min_resolution_closure_cs(F)[1])$
       
  • DONE (see Hardness.mac) A new file Hardness.mac should be created in this module and these functions transferred there with tests.
Todo:
Create milestones
Todo:
Write docus

Definition in file general.hpp.