OKlibrary
0.2.1.6

Plans for Maximacomponents regarding SATreductions (in general) More...
Go to the source code of this file.
Plans for Maximacomponents regarding SATreductions (in general)
Packaging of reductions into some "preprocessing" is handled in Satisfiability/Lisp/Preprocessing.
/* Computing the hardness of a clauseset 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])$
Definition in file general.hpp.