OKlibrary  0.2.1.6
GeneralisedUCP.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 15.12.2007 (Swansea) */
00002 /* Copyright 2007, 2008, 2009, 2011, 2012 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/Hypergraphs/Lisp/SetSystems.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Reductions/UnitClausePropagation.mac")$
00025 
00026 
00027 /* **********************
00028    * The r_k reductions *
00029    **********************
00030 */
00031 
00032 /* "Generalised unit-clause-propagation":
00033     input a clause-set F and level k >= 0, output r_k(F).
00034     Every forced assignment is found for k large enough.
00035 */
00036 /* The general idea: */
00037 generalised_ucp_g_cs(F,k) :=
00038  if k=0 then
00039    if elementp({},F) then {{}} else F
00040  else block([V : var_cs(F), break : false],
00041   for v in V unless break do for eps in {-1,1} unless break do
00042     if generalised_ucp(apply_pa({eps * v}, F), k-1) = {{}} then
00043       (F : apply_pa({-eps * v}, F), break : true),
00044   if break then return(generalised_ucp(F,k)) else return(F))$
00045 
00046 /* For the cases k=0,1 one has special algorithms (making the
00047    implementation more efficient), and also the case k=1 should
00048    be applied in any case. This is implemented in this basic algorithm:
00049 */
00050 /* RENAME: generalised_ucp_cs */
00051 generalised_ucp(F,k) := block(
00052  if elementp({},F) then return({{}})
00053  elseif k=0 then return(F),
00054  F : ucp_0_cs(F),
00055  if k=1 or F={{}} then return(F)
00056  else block([mr : min_rank_cs(F)],
00057   if mr > k then return(F) else
00058    block([V : var_cs(F), break : false],
00059    for v in V unless break do for eps in {-1,1} unless break do
00060      if generalised_ucp(apply_pa({eps * v}, F), k-1) = {{}} then
00061        (F : apply_pa({-eps * v}, F), break : true),
00062    if break then return(generalised_ucp(F,k)) else return(F))))$
00063 generalised_ucp_cs(F,k) := generalised_ucp(F,k)$
00064 
00065 /* generalised_ucp(F,1) is unit-clause-elimination.
00066    If F in 2-CNF, then generalised_ucp(F,2) = {{}} iff F is unsatisfiable.
00067    If {} in F, then the result is always {{}}.
00068 */
00069 
00070 /* Input a clause-set F and level k, output r_k(F) together with a forced
00071    partial assignment phi s.t. phi * F = r_k(F) */
00072 /* RENAME: generalised_ucp_pa_cs */
00073 generalised_ucp_pa(F,k) := block([R : generalised_ucp_opa(F,k)],
00074  [R[1], setify(R[2])])$
00075 generalised_ucp_pa_cs(F,k) := generalised_ucp_pa(F,k)$
00076 /* The variation which returns an ordered partial assignment (in the
00077    order the forced assignments were found; variables are tested
00078    in the natural order, trying "true" first):
00079 */
00080 /* RENAME: generalised_ucp_opa_cs */
00081 generalised_ucp_opa(F,k) := block([V : var_cs(F), mr : min_rank_cs(F)],
00082  if mr > k then [F,[]]
00083  elseif mr = 0 then [{{}},listify(V)] else
00084   block([break : false, x],
00085   for v in V unless break do for eps in {-1,1} unless break do
00086     if generalised_ucp(apply_pa({eps * v}, F), k-1) = {{}} then (
00087       x : -eps * v,
00088       F : apply_pa({x}, F),
00089       break : true),
00090   if break then block([R : generalised_ucp_opa(F,k)],
00091     return([R[1], cons(x, R[2])]))
00092   else return([F,[]])))$
00093 
00094 
00095 /* Instances */
00096 
00097 generalised_ucp0_cs(F) := generalised_ucp_cs(F,0);
00098 generalised_ucp1(F) := generalised_ucp(F,1);
00099 generalised_ucp2(F) := generalised_ucp(F,2);
00100 generalised_ucp_pa1(F) := generalised_ucp_pa(F,1);
00101 generalised_ucp_pa2(F) := generalised_ucp_pa(F,2);
00102 
00103 
00104 /* *******************************
00105    * Reduction by weak autarkies *
00106    *******************************
00107 */
00108 
00109 /* Generalised pure-literal-elimination, more precisely, reduction by
00110    weak autarkies found by making k assumptions; input a clause-set.
00111    weakaut_red(F,1) is pure-literal-elimination, strengthened by
00112    subsumption.
00113    Every weak autarky is found for k large enough. */
00114 weakaut_red(F,k) := if k = 0 then F else
00115   block([L : literals_v(var_cs(F)), break : false, G],
00116     for x in L unless break do (
00117       G : weakaut_red(apply_pa({x},F),k-1),
00118       if subsetp(G, F) then break : true),
00119     if break then return(weakaut_red(G,k)) else return(F))$
00120 
00121 /* Additionally return the weak autarky found. */
00122 weakaut_red_pa(F,k) := if k = 0 then [F,{}] 
00123  else block(
00124   [V : var_cs(F), L, break : false, y, G, H],
00125   L : literals_v(V),
00126   for x in L unless break do (
00127     G : weakaut_red_pa(apply_pa({x},F),k-1),
00128     if subsetp(G[1], F) then (y : x, break : true)
00129   ),
00130   if break then (
00131     H : weakaut_red_pa(G[1],k), 
00132     return([H[1], union(H[2], G[2], {y})]))
00133   else return([F,{}]))$
00134 
00135 
00136 /* ****************************************************************
00137    * Combining generalised unit-clause and weak-autarky-reduction *
00138    ****************************************************************
00139 */
00140 
00141 /* Combined generalised ucp and weak-autarky-reductions: Guarantees that
00142    either F = {{}} or F = {} or for all literals x we have
00143      generalised_ucp(apply_pa({x}, F),k-1) <> {{}} and
00144      generalised_weakaut(apply_pa({x}, F),k-1) is not subset of F.
00145   For k >= n(F) solves the SAT-problem for F.
00146 */
00147 generalised_ucp_war(F,k) := if has_empty_element(F) then {{}}
00148   elseif k = 0 then F else
00149   block([L : literals_v(var_cs(F)), break : false, G],
00150     for x in L unless break do (
00151       G : generalised_ucp_war(apply_pa({x},F),k-1),
00152       if G = {{}} then (
00153         F : apply_pa({-x},F), break : true)
00154       elseif subsetp(G, F) then (
00155         F : G, break : true
00156       )),
00157     if break then return(generalised_ucp_war(F,k)) else return(F))$
00158 
00159 /* Additionally return the partial assignment yielding the result. */
00160 generalised_ucp_war_pa(F,k) := block([V : var_cs(F)],
00161  if has_empty_element(F) then return([{{}}, V])
00162  elseif k = 0 then return([F,{}]) 
00163  else block(
00164   [L : literals_v(V), break : false, y, G, H],
00165   for x in L unless break do (
00166     G : generalised_ucp_war_pa(apply_pa({x},F),k-1),
00167     if G[1] = {{}} then (
00168       F : apply_pa({-x},F), y : -x, break : true)
00169     elseif subsetp(G[1], F) then (
00170       F : G[1], y : x, break : true)),
00171   if break then (
00172     H : generalised_ucp_war_pa(F,k), 
00173     return([H[1], union(H[2], G[2], {y})]))
00174   else return([F,{}])))$
00175 
00176 
00177 /* ******************************************************************
00178    * Generalised elimination of pure literals by forced assignments *
00179    ******************************************************************
00180 */
00181 
00182 /* This reduction is really meaningful only as a part of generalised_ucp_ple 
00183    below. */
00184 
00185 /* Generalised pure-literal-elimination ("ple") by sub-ordinated ucp.
00186    Finds thus all weak autarkies which are "mostly enforced". */
00187 generalised_ple(F,k) := block([L : literals_v(var_cs(F)), break : false, G],
00188   for x in L unless break do (
00189     G : generalised_ucp(apply_pa({x},F),k),
00190     if subsetp(G, F) then break : true),
00191   if break then return(generalised_ple(G,k)) else return(F))$
00192 
00193 /* generalised_ple(F,0) is pure-literal-elimination.
00194    generalised_ple(F,1) is the lean kernel for F in 2-CNF if F all clauses of
00195    F have length (exactly) 2.
00196    If {} in F then the result is {{}}.
00197 */
00198 
00199 /* Additionally return the weak autarky found */
00200 generalised_ple_pa(F,k) := block([L : literals_v(var_cs(F)), break : false, y],
00201   for x in L unless break do
00202     if subsetp(generalised_ucp(apply_pa({x},F),k), F) then (y : x, break : true),
00203   if break then
00204    block([G : generalised_ucp_pa(apply_pa({y},F),k)],
00205     block([H : generalised_ple_pa(G[1],k)], 
00206      return([H[1], union(H[2], G[2], {y})])))
00207   else return([F,{}]))$
00208 
00209 
00210 /* *******************************************************
00211    * Look-ahead reduction for r_k and enforced autarkies *
00212    *******************************************************
00213 */
00214 
00215 /* Combined generalised ucp-ple: Guarantees that
00216    either F = {{}} or F = {} or for all literals x we have
00217      generalised_ucp(apply_pa({x}, F),k) <> {{}} and
00218      generalised_ucp(apply_pa({x}, F),k) is not subset of F.
00219 */
00220 generalised_ucp_ple(F,k) := generalised_ple(generalised_ucp(F,k+1),k)$
00221 
00222 /* generalised_ucp_ple(F,0) is unit-clause-elimination and elimination
00223    of pure literals.
00224    generalised_ucp_ple(F,1) solves SAT for clause-sizes at most 2.
00225 */
00226 
00227 /* Additionally return the partial assignment leading to the reduced
00228    clause-set */
00229 generalised_ucp_ple_pa(F,k) := block([G : generalised_ucp_pa(F,k+1), H],
00230   H : generalised_ple_pa(G[1],k),
00231   return([H[1], union(G[2], H[2])]))$
00232 
00233 /* Instances */
00234 
00235 generalised_ucp_ple0(F) := generalised_ucp_ple(F,0)$
00236 generalised_ucp_ple1(F) := generalised_ucp_ple(F,1)$
00237 generalised_ucp_ple_pa0(F) := generalised_ucp_ple_pa(F,0)$
00238 generalised_ucp_ple_pa1(F) := generalised_ucp_ple_pa(F,1)$
00239 
00240 /* Note that splitting trees obtained via generalised_ucp_ple(F,k)
00241    for unsatisfiable F are r_{k+1}-splitting trees!
00242 */
00243 
00244