OKlibrary  0.2.1.6
Generators.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 29.11.2007 (Swansea) */
00002 /* Copyright 2007, 2008, 2009, 2010, 2011, 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 
00022 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/PartialAssignments.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Substitutions.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/Basics.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Combinatorics/Lisp/Enumeration/Subsets.mac")$
00029 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Strings.mac")$
00030 
00031 
00032 /* ********************
00033    * Full clause-sets *
00034    ********************
00035 */
00036 
00037 /* The full clause-set over variable set or list V: */
00038 full_fcs_v(V) := [if listp(V) then setify(V) else V, all_tass(V)]$
00039 full_cs_v(V) := all_tass(V)$
00040 /* We have full_fcs_v(V) = expand_fcs([V,{{}}]) for sets V. */
00041 
00042 full_fcl_v(V) := [listify(V), all_tass_l(listify(V))]$
00043 full_cl_v(V) := all_tass_l(listify(V))$
00044 /* Remark: the order of  full_fcl_v(V) is lexicographical, based on
00045    [-1,1,-2,2,...,-n,n], for V=[1,...,n].
00046 */
00047 
00048 /* The formal full clause-set with variable set {1,...,n} and all
00049    possible (full) clauses (also known as "canonical CNF/DNF"): */
00050 full_fcs(n) := full_fcs_v(setn(n))$
00051 full_cs(n) := full_cs_v(setn(n))$
00052 full_fcl(n) := full_fcl_v(setn(n))$
00053 full_cl(n) := full_cl_v(setn(n))$
00054 
00055 /* Measures */
00056 
00057 nvar_full_fcs(n) := n$
00058 
00059 /* List of clause-counts for full_fcs as with ncl_list_f */
00060 ncl_list_full_fcs(n) := [[n,2^n]]$
00061 ncl_full_fcs(n) := 2^n$
00062 
00063 deficiency_full_fcs(n) := ncl_full_fcs(n) - nvar_full_fcs(n)$
00064 
00065 
00066 /* Output */
00067 
00068 output_fullcs(n,filename) :=
00069  outputext_fcl(
00070    sconcat("Canonical unsatisfiable clause-set with ", n, " variables.
00071 c ", created_by_OKlib()),
00072    full_fcl(n),
00073    filename)$
00074 
00075 output_fullcs_stdname(n) := output_fullcs(n,
00076  sconcat("FullCls-",n,".cnf"))$
00077 
00078 
00079 /* ********************
00080    * Order principles *
00081    ********************
00082 */
00083 
00084 /* Variables are "gt(i,j)", meaning that there is an edge from i to j: */
00085 kill(gt)$
00086 declare(gt, noun)$
00087 declare(gt, posfun)$
00088 gt_var(i,j) := nounify(gt)(i,j)$
00089 
00090 /* The list of variables: */
00091 var_ordergt(m) := lappend(map(
00092   lambda([p], map(lambda([po], apply(gt_var, po)), listify(permutations(p)))),
00093   colex_ksubsets_l(setn(m), 2)))$
00094 
00095 /* The clauses expressing transitivity: */
00096 ordergt_transitivity_ocs(m) :=
00097   lappend(map(
00098     lambda([S], map(
00099       lambda([p], {-gt_var(p[1],p[2]),-gt_var(p[2],p[3]),gt_var(p[1],p[3])}),
00100       listify(permutations(S)))),
00101     colex_ksubsets_l(setn(m), 3)))$
00102 
00103 ordergt_nocycles_ocs(m) := map(
00104   lambda([p], comp_sl(map(lambda([po], apply(gt_var, po)), permutations(p)))),
00105   colex_ksubsets_l(setn(m), 2))$
00106 
00107 ordergt_nosource_ocs(m) := block([M : setn(m)],
00108   create_list(map(lambda([x], gt_var(x,j)), disjoin(j,M)) , j,1,m))$
00109 
00110 ordergt_ofcs(m) := [var_ordergt(m), append(ordergt_transitivity_ocs(m),ordergt_nocycles_ocs(m),ordergt_nosource_ocs(m))]$
00111 
00112 output_ordergt(m,filename) := block(
00113  [FF : standardise_fcl(ordergt_ofcs(m))],
00114   output_fcl_v(
00115     sconcat("GT problem,
00116 c created by the OKlibrary at ", timedate(),":
00117 c with ", m, " vertices.
00118 c Variables and associated edges:"),
00119     FF[1],
00120     filename,
00121     FF[2]))$
00122 /* Providing a standard name: "OrderGT-m.cnf": */
00123 output_ordergt_stdname(m) := output_ordergt(m,
00124   sconcat("OrderGT-",m,".cnf"))$
00125 
00126