OKlibrary  0.2.1.6
PlantedSolutions.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 2.11.2008 (Swansea) */
00002 /* Copyright 2008, 2009 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/TestSystem/Lisp/Asserts.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/DLL_solvers.mac")$
00024 
00025 kill(f)$
00026 
00027 /* *******************************************
00028    * Minimally uniquely satisfiable problems *
00029    *******************************************
00030 */
00031 
00032 okltest_minUNISAT(f) := block([solver],
00033   set_random(0),
00034   assert(f([{},{}],{},solver) = {}),
00035   solver : dll_simplest_trivial2,
00036   assert(f([{1},{{1}}],{},solver) = {}),
00037   assert(f([{1},{}],{-1},solver) = {-1}),
00038   assert(f([{1},{{1}}],{1},solver) = {}),
00039   assert(f([{1,2},{{1,2},{1,-2}}],{1},solver) = {}),
00040   assert(f([{1,2},{{1,2}}],{1,2},solver) = {1,2}),
00041   assert(f([{1,2},{{1,2}}],{1,-2},solver) = {-2}),
00042   assert(f([{1,2,3},{{1,2},{2,3}}],{-1,-3,2},solver) = {-1,-3}),
00043   assert(f([{1},{{1},{-1}}],{1},solver) = {}),
00044   assert(f([{1},{{-1}}],{1},solver) = {1}),
00045   assert(f([{1,2},{{1},{-1}}],{1},solver) = {}),
00046   assert(f([{1,2},{{1},{2}}],{-1,-2},solver) = {-2}),
00047   assert(f([{1,2},{{1}}],{2},solver) = {2}),
00048   assert(f([{1,2},{{1}}],{1,2},solver) = {2}),
00049   true)$
00050