OKlibrary  0.2.1.6
PlantedSolutions.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 1.11.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 
00024 /* *******************************************
00025    * Minimally uniquely satisfiable problems *
00026    *******************************************
00027 */
00028 
00029 /* For given formal clause-set FF and partial assignment phi, compute, by
00030    repeated randomised removal of literals from phi, a minimal
00031    phi' <= phi such that in phi' * FF all assignments from phi - phi'
00032    are enforced.
00033 */
00034 /* Prerequisite: var(phi) <= var(FF). */
00035 minUNISAT(FF,phi,solver) := block(
00036  [minimal : false, FFA : [FF[1],union(FF[2],{comp_sl(phi)})]],
00037   while not minimal do (
00038     minimal : true,
00039     for x in random_permutation(phi) unless not minimal do
00040      block([nphi : disjoin(x,phi)],
00041       if solver(apply_pa_fcs(nphi,FFA)) = false then (
00042         phi : nphi, minimal : false))
00043   ),
00044   return(phi))$
00045 /* A main application is the situation where phi is a total satisfying
00046    assignment for FF, and one wants to find a minimal phi' such that
00047    phi' * FF has phi as its unique solution.
00048    If on the other hand phi * FF is unsatisfiable, then phi' is a minimal
00049    sub-assignment of phi such that phi' * FF is still unsatisfiable.
00050 */
00051