OKlibrary  0.2.1.6
Hardness.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 21.6.2011 (Swansea) */
00002 /* Copyright 2011, 2012, 2013 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00033 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00034 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Statistics.mac")$
00035 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Reductions/GeneralisedUCP.mac")$
00036 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Primality/PrimeImplicatesImplicants.mac")$
00037 
00038 
00039 /* **********************
00040    * Computing hardness *
00041    **********************
00042 */
00043 
00044 /* Computing the hardness of a clause-set F with its prime-implicates PI
00045    as input:
00046 */
00047 hardness_wpi_cs(F,PI) := block([k : 0, F_phi],
00048   for C in PI do (
00049     F_phi : apply_pa(comp_sl(C),F),
00050     while generalised_ucp_cs(F_phi,k) # {{}} do k:k+1
00051   ),
00052   k)$
00053 /* Remark: if one wants to see the prime implicates causing an increase in
00054    assumed hardness, replace "k:k+1" by "(print(k,C), k:k+1)".
00055 */
00056 /* Taking just the clause-set F: */
00057 hardness_cs(F) := hardness_wpi_cs(F,min_resolution_closure_cs(F)[1])$
00058 /* Only considering unsatisfiable F: */
00059 hardness_u_cs(F) := hardness_wpi_cs(F,{{}})$
00060 
00061 
00062 /* **********************************
00063    * Computing propagation-hardness *
00064    **********************************
00065 */
00066 
00067 /* Computing the p-hardness of a clause-set F with its prime-implicates PI
00068    as input:
00069 */
00070 phardness_wpi_cs(F,PI) := if emptyp(F) or elementp({},F) then 0
00071  elseif PI = {{}} then max(hardness_wpi_cs(F,PI),1) else
00072  block([k : 1, F_phi],
00073   for C in PI do for x in C do (
00074     F_phi : apply_pa(comp_sl(disjoin(x,C)),F),
00075     while not elementp(x,generalised_ucp_pa_cs(F_phi,k)[2]) do k : k+1
00076   ),
00077   k)$
00078 /* Taking just the clause-set F: */
00079 phardness_cs(F) := phardness_wpi_cs(F,min_resolution_closure_cs(F)[1])$
00080 
00081 
00082 /* ************************
00083    * Computing w-hardness *
00084    ************************
00085 */
00086 
00087 /* Computing the w-hardness of a clause-set F with its prime-implicates PI
00088    as input:
00089 */
00090 whardness_wpi_cs(F,PI) := block([k : 0, F_phi],
00091   for C in PI do (
00092     F_phi : apply_pa(comp_sl(C),F),
00093     while min_kresolution_closure_cs(F_phi,k)[1] # {{}} do k : k+1
00094   ),
00095   k)$
00096 /* Taking just the clause-set F: */
00097 whardness_cs(F) := whardness_wpi_cs(F,min_resolution_closure_cs(F)[1])$
00098 /* Only considering unsatisfiable F: */
00099 whardness_u_cs(F) := whardness_wpi_cs(F,{{}})$
00100 
00101