OKlibrary  0.2.1.6
general.hpp File Reference

Plans for Maxima-components regarding clause-sets. More...

Go to the source code of this file.


Detailed Description

Plans for Maxima-components regarding clause-sets.

Todo:
Update output_pa
  • The function "output_pa" outputs a partial assignment in the style used by SplittingViaOKsolver, and Satisfiability/Interfaces/InputOutput/PartialAssignments.hpp.
  • This function should be properly linked, and specified.
  • Such specification includes the order of the literals in the output; currently, the order given by Maxima is used.
  • This function belongs to the input-output-module to be established; see "Input and output" below.
Bug:
DONE (new implementation of print_nlb doesn't have this problem) print_nlb doesn't allow lines more than 10000 characters long
  • We get the following error:
    > print_nlb(apply(sconcat,create_list(1,i,1,10000)));
    assignment: cannot assign 10001 to linel
    #0: print_nlb(s=1111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111...)
     -- an error. To debug this try: debugmode(true);
       
  • This bug causes problems with the AES generation scripts, where we get a similar error with print_nlb:
    > output_ss_fcl_std(1,4,4,4,false,aes_ts_box,aes_mc_bidirectional);
    #0: print_nlb(s=c 1173 : ss_ctr_ns(ss_round_ns(ss_mixcolumns_ns(ss_bi_mixcolumn_ns(ss_inv_mixcolumn_ns(ss_mul_ts_ns(...)
    #1: print_fcl_v(comment=Small Scale AES with r=1,c=4,rw=4,e=4,final=false,box_tran=aes_ts_box,mc_tran=aes_mc_bidirectional,ff=[[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36...,
       
  • print_nlb sets the maxima linel variable to the length of the string but with:
    > linel : 10000;
    10000
    > linel : 10001;
    assignment: cannot assign 10001 to linel
     -- an error. To debug this try: debugmode(true);
       
    we get an error.
  • According to Robert Dodler on the Maxima mailing list, we can do the following to set linel via lisp directly:
    :lisp (setq $linel 10001 linel 10001)
       
    however, it is not clear how we can do the same from a loaded Maxima file.
  • Robert Dodler says that there is currently a hard limit of 10000 in the Maxima code, which is what triggers this error and according to Dieter Kalser, this is because Maxima crashes when linel is set to certain large values (unspecified).
Todo:
Create milestones
Todo:
Write tests
Todo:
Write docus
Todo:
Notions for clauses, clause-sets etc.
  • See "Better general naming conventions" in ComputerAlgebra/Satisfiability/Lisp/plans/general.hpp for the general naming-discussion.
  • See ComputerAlgebra/Satisfiability/Lisp/plans/Literals.hpp for general discussions on "literals".
  • See ComputerAlgebra/Satisfiability/Lisp/plans/Clauses.hpp for general discussions on "clauses".
  • See ComputerAlgebra/Satisfiability/Lisp/plans/PartialAssignments.hpp for general discussions on "partial assignments".
  • All variations on clause-sets should still be "syntactical objects", so the discussion in ComputerAlgebra/Satisfiability/Lisp/plans/SatisfactionProblems.hpp is not relevant yet.
  • At the base level we have
    1. "clause-sets" as now;
    2. "ordered clause-sets", repetition-free lists of clauses;
    3. "clause-lists" (lists of clauses).
  • "Formal" versions (just adding variables):
    1. "formal clause-sets" as now;
    2. "ordered formal clause-sets";
    3. "formal clause-lists".
    Additionally, the formal clause-sets also exist as "formal multi-clause-sets" and "formal labelled clause-sets".
  • Should we also allow "multi-clause-sets" and "labelled clause-sets" without the variables?
    1. Otherwise the "formal" in this context is superfluous.
    2. On the other hand, the multi- and labelled versions are introduced in the graph-theoretical context, and there we always have the set of vertices given (except of set-systems).
  • "Multi-clause-sets":
    1. A triple [V,F,c] s.t. [V,F] is a formal clause-set and c: F -> NN.
    2. Accordingly "ordered multi-clause-sets".
    3. However, perhaps the clause-function is better defined on all possible clauses over V (and returns 0 for clauses which are not contained.
  • Labelled clause-sets (not "general clause-sets" to avoid confusion)
    1. A "labelled clause-set" is a triple [V,F,f], where V is a set of variables, F a set of clause-labels, and f assigns to each element of F a clause over V.
    2. Accordingly, "ordered labelled clause-sets are triples [V,F,f], where now V,F are repetition-free lists.
    3. DONE Labelled clause-sets should always have sets of variables, so we can drop the "formal".
  • Relations to hypergraphs (see ComputerAlgebra/Hypergraphs/Lisp/plans/general.hpp):
    1. fcs <-> hg, ofcs <-> ohg
    2. mucs <-> muhg, omucs <-> omuhg
    3. lcs <-> ghg, olcs <-> oghg.
    Additionally we have
    1. "cs" corresponds to "set-systems"
    2. "ocs" corresponds to "ordered set-systems"
    3. "cl" corresponds to "lists of sets".
    A somewhat subtle point: clause-sets here are the only type of objects which are deeply copied (as sets!), while the rest is, since we have lists, copied in the shallow way.
  • Formal clause-lists (fcl) have no correspondence at the hypergraph side:
    1. If we have a list V of vertices and a list E of hyperedges, then we use the ghg [V,E,identity].
    2. Seems alright.
    3. So perhaps also for clause-sets we should abandon "fcl" (but keep "cl"), since we have already "lcs".
    4. On the other hand, a formal clause-list seems to be a very natural concept, perhaps the most natural one from the point of view of SAT solving, so we should keep it.
  • Conversions:
    1. "cs2cl": from clause-sets to clause-lists
    2. Likely "cs_to_fcs" should become "cs2fcs".
  • For non-boolean literals see "Notions for generalised literals" in ComputerAlgebra/Satisfiability/Lisp/ClauseSets/plans/NonBoolean.hpp.
Todo:
Organisation
  • Inclusion
    1. Currently, the outsourced files are "inclusions-wise equivalent" to ClauseSets/BasicOperations.mac, i.e., they include it and are automatically included.
    2. This is because it is too much work to sort out the real dependencies for all the Maxima-files in the library.
    3. It would be good to have a refactoring tool, which would find out about the dependencies:
      • If it is too hard to find out about the functions (and names in general) defined in a file, that it needs to explicitly given as input.
      • And then we can just search for files using some of these functions, whether they correctly include them.
      • And we search for files which use some of them but don't include it.
  • DONE We should have "Substitutions.mac":
    1. See "Applying substitutions" in ComputerAlgebra/Satisfiability/Lisp/Symmetries/plans/general.hpp.
    2. Everything currently under "Substitution and renaming" goes there.
  • DONE We should create "Statistics.mac".
    1. DONE : move.
    2. A problem is now how to handle inclusion.
    3. For the moment, "Statistics.mac" and "BasicOperations.mac" are inclusions-wise equivalent.
  • See "Input and output" below.
  • DONE We should create "PartialAssignments.mac".
Todo:
Input and output
  • See Interfaces/InputOutput/plans/Dimacs.hpp.
  • Input-output-functions currently in ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac shall move to their own file "InputOutput.mac".
  • See also the above "Update output_pa" for further functions to include.
  • DONE The usage of "print" likely should be replaced by "printf" from package "stringproc".
    1. Then the trailing space on every printed line should be removed.
  • We should have options for output:
    1. Instead of for example "php(3,2)" print out "php_3_2".
    2. DONE And also print it out in strict Dimacs format, optionally with the mapping from natural numbers to original variables given in the comments.
  • We need also reading from Dimacs-files.
    • DONE (We used Maxima's readline and read_list functions - see read_fcs_f in ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac) A simple function for reading from a standard "cnf" DIMACS file might be:
      oklib_plain_include("stringproc")$
      
      read_fcs_f(n) := block([fh, line, ll, cs : [], l,b,c],
        fh : openr(n),
        while stringp(line : readline(fh)) do (
          ll : tokens(line),
          if length(ll) >= 1 then
            if not(first(ll) = "c" or first(ll) = "p") then
              cs : cons(setify(rest(map(parse_string,ll),-1)), cs)
        ),
        cs : setify(cs),
        return(cs_to_fcs(cs))
      )$
           
    • The above function should better return a clause-list.
    • Perhaps even more appropriate a formal clause-list, where the set of variables reflects the n-value from the p-line.
    • Maxima likely has no parsing capabilities, but there should be Lisp-libraries for parsing?
      1. It would be interesting to explore them (they should be useful for many occassions).
    • What to do with syntax checking?
      1. Typically, at the Maxima level we do not check inputs.
      2. However we do provide (dedicated) tests.
      3. So we should write a syntax checking functions.
    • How to test this function?
      1. Most appropriate seems to use an application test.
    • Additionally, there is the possibility of reading Extended DIMACS files, where the variables might be non-integer names. In such a case there seem to be several possibilities
      • The file is read into a normal formal clause set, and the variables are treated directly as maxima nouns, where they are also declared "posfun" etc, so that operations such as "abs" and so on work correctly.
      • The file is read into a formal clause set, but the variables are translated to integer variables with the mapping from the variable name to the integer variable being returned in a hash or setmap (so a pair of the fcs and setmap is returned).
      • Most appropriate seems to me to use the (formal) function "edim" (for "extended Dimacs"), which is used with one string-parameter ( the variable-name).

Definition in file general.hpp.