OKlibrary  0.2.1.6
Degrees.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 16.2.2008 (Swansea) */
00002 /* Copyright 2008 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 
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Hypergraphs.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00025 
00026 
00027 /* Checks whether clause-set F is satisfiable according to the symmetric
00028    Lovasz Local Lemma test for clause-degrees.
00029    If true is returned then F is satisfiable, if false is returned then
00030    the test did not succeed and F may be satisfiable or unsatisfiable. */
00031 locallemma_sattest_clausedeg(F) := is(max_degree_cvg_cs(F) <= 2^(min_rank_cs(F)) / exp(1) - 1)$
00032 
00033 /* Checks whether clause-set F is satisfiable according to the symmetric
00034    Lovasz Local Lemma test for variable-degrees. */
00035 /* Slightly improved w.r.t. case k = 1. */
00036 locallemma_sattest_vardeg(F) := block([k : min_rank_cs(F)],
00037  if k = inf then return(true)
00038  elseif k = 0 then return(false)
00039  else return(is(max_variable_degree_cs(F) <= 2^k / exp(1) / k)))$
00040 
00041 /* Checks whether clause-set F is satisfiable according to the asymmetric
00042    Lovasz Local Lemma as used by [Hooker, Vinai, 1995].
00043    Improved with respect to handling of clauses of length <= 1. */
00044 /* Compare with locallemma_satapprox in
00045    ComputerAlgebra/Satisfiability/Lisp/Backtracking/DLL_solvers.mac. */
00046 locallemma_sattest_asymmetric(F) := if emptyp(F) then true
00047  elseif empty_element_p(F) then false else
00048  block([G : cvg_cs(F), break : false],
00049   for C in G[1] unless break do
00050     if gsum_s(lambda([D], 2^(-length(D))), neighbours(C, G)) > 1/4 then 
00051       break : true,
00052   return(not break))$
00053