OKlibrary  0.2.1.6
ConstraintTemplateRewriteSystem.hpp File Reference

User documentation for the Maxima computer algebra system implementation of a constraint template rewrite system. More...

Go to the source code of this file.


Detailed Description

User documentation for the Maxima computer algebra system implementation of a constraint template rewrite system.

Todo:
General idea
  • We represent a constraint system as a list (conjunction) of constraints which are iteratively rewritten to smaller and smaller constraints; finally the constraints are then translated individually to some problem domain (SAT, CP etc).
  • There are three main stages in this translation:
    1. Local constraint rewriting: iteratively translating single constraints to lists of "smaller" constraints.
    2. Global constraint propagation: propagating the effect of global constraints (for example variable renamings) across the entire constraint list.
    3. Constraint translation: translating single constraints directly to SAT etc.
  • See "Data types" for a list of the data-types involved in each stage.
  • The main functions involved in each case are:
  • In the case of the constraint translation, translation functions are specific to the domain being translated to; there are different translation functions for each different translation "target" (SAT,CSP etc), at both the problem and general level.
  • In the all 3 stages, new variables can be introduced.
  • We translate the AES using this framework; see Cryptanalysis/Rijndael/docus/Translations.hpp.
Todo:
Data types and concepts
  • There are 6 main data-types and concepts in the local constraint rewrite system:
    • A constraint template is a concept which defines a related set of constraints.
      • Constraint templates are not made concrete in code.
      • However, we do consider constraint templates; a constraint has a "constraint template name".
      • The constraint template name allows us to know what "type" of constraint it is.
      • For example, "ss_sbox_cst" is the name of the small scale S-box constraint template. Specific S-box constraints have "ss_sbox_cst" as their constraint template name, and then other parameters defining the specific S-box, the variables and so on.
    • A namespace is a function which is applied to a variable, creating a new unique variable, which doesn't share it's name with any other variable in the constraint template list.
    • A constraint is a list of at least 3 elements:
      • the first element is the name of the constraint template as a string;
      • the second element is the list of variables associated with the constraint;
      • the last element is the "namespace" of the constraint.
      A constraint L may optionally have any number of additional arguments in list positions 3,...,length(L)-1.
    • A constraint template rewrite rule is a function which takes a constraint and returns a list of constraints which represent the input constraint.
    • A constraint template variable rewrite rule is a function which takes a constraint and returns a list of new variables in the constraint list after applying the corresponding rewrite rule to the input constraint.
    • A rewrite bundle is a triple [fr,nsp,fv] where fr is a rewrite rule, nsp is a namespace and fv is variable rewrite rule for fv.
    • A rewrite map is a an ordered (i.e. list) set map which maps a given constraint template name (string) to a rewrite bundle.
  • There is 1 data-type in the global constraint propagation system:
    • A propagation function takes a constraint list, and a list of the variables in the constraint list and returns the pair of the new constraint and variable lists after propagating the constraint(s) it handles.
  • There are 4 data-types in the SAT translation mapping:
    • A translation function takes a constraint and returns a clause-list representing the constraint.
    • A variable translation function takes a constraint and returns a list of the new variables in the clause-list returned by the associated translation function given the input constraint.
    • A rewrite bundle is a pair [ft,fv] where fr a translation function and fv is variable rewrite rule for fv.
    • A rewrite map is a list of rewrite bundles specifying the map from constraint template names to translation functions.
Todo:
Naming conventions
  • Constraint - denoted by postfix "cst".
  • Constraint rewrite function - denoted by "cstr" in function name.
  • Constraint list - denoted by "cstl".
Todo:
Example
  • As an example, consider that one has the EVEN-PARITY constraint over n=4 variables:
    declare(even_par_ns, posfun);
    declare(even_par_ns, noun);
    even_par_cstt : ["even_parity",['v1,'v2,'v3,'v4], even_par_ns];
       
    Then "even_par_ns" would be the namespace and "even_par_cst" would be the constraint.
  • We can an EVEN-PARITY constraint to three even parity constraints and an odd parity constraint, using new variables:
    EVEN-PARITY(v1,v2,v3,v4) = EVEN-PARITY(v5,v6) and EVEN-PARITY(v1,v2,v5) and EVEN-PARITY(v3,v4,v6)
       
  • As EVEN-PARITY(v,v') is true iff v == v', we can use equality constraints to enforce this.
  • Implementing this as rewrite rules:
    kill(even_par_ns)$
    declare(even_par_ns,noun)$
    declare(even_par_ns,posfun)$
    even_par_split_namespace([arg_l]) := apply(nounify(even_par_ns),arg_l)$
    
    even_par_split_cstrb :
      [even_par_split_cstr_cstl,even_par_split_namespace,even_par_split_ns_var_l]$
    
    even_par_split_ns_var_l(cst) :=
     if length(cst[2]) <= 3 then []
     else block(
      [ns : cstt_namespace_new(even_par_split_namespace,cst)],
      [ns(1),ns(2)])$
    even_par_split_cstr_cstl(cst) := block([ns, split_index],
     ns : cstt_namespace_new(even_par_split_namespace,cst),
     new_vars : even_par_split_ns_var_l(cst),
     split_index : floor(length(cst[2])/2),
     if length(cst[2]) = 2 then [["eq_cst",cst[2], ns]]
     else if length(cst[2]) <= 3 then
       [["ternary_even_parity",cst[2], ns]]
     else
       [["even_parity",
         endcons(new_vars[1],
                 take_elements(split_index,cst[2])),1, ns],
        ["even_parity",
         endcons(new_vars[2], rest(cst[2],split_index)), ns],
        ["even_parity", even_par_split_ns_var_l(cst),2,ns]])$
       
  • Using the constraint rewrite rule:
    cstl : rewrite_all_csttl([even_par_cstt],[["even_parity",even_par_split_cstrb]]);
    [["eq_cst",
             [even_par_ns(even_par_ns(1,["even_parity",cstt_id_ns])),
              even_par_ns(even_par_ns(2,["even_parity",cstt_id_ns]))],
             lambda([a],
                    lambda([a],even_par_ns(even_par_split_namespace(a,["even_parity",cstt_id_ns])))(
                     even_par_split_namespace(a,["even_parity",cstt_id_ns])))],
            ["ternary_even_parity",[v3,v4,even_par_ns(even_par_ns(2,["even_parity",cstt_id_ns]))],
             lambda([a],
                    lambda([a],even_par_ns(even_par_split_namespace(a,["even_parity",cstt_id_ns])))(
                     even_par_split_namespace(a,["even_parity",cstt_id_ns])))],
            ["ternary_even_parity",[v1,v2,even_par_ns(even_par_ns(1,["even_parity",cstt_id_ns]))],
             lambda([a],
                    lambda([a],even_par_ns(even_par_split_namespace(a,["even_parity",cstt_id_ns])))(
                     even_par_split_namespace(a,["even_parity",cstt_id_ns])))]]
    cstl_vars : rewrite_all_cstt_vars_l([even_par_cstt],[["even_parity",even_par_split_cstrb]]);
      [even_par_ns(even_par_ns(1,["even_parity",cstt_id_ns])),
       even_par_ns(even_par_ns(2,["even_parity",cstt_id_ns]))]
       
  • We can then remove the equivalence constraint "eq_cst", by propagating a renaming of even_par_ns(even_par_ns(1,["even_parity",cstt_id_ns])) to even_par_ns(even_par_ns(2,["even_parity",cstt_id_ns])):
    csttl: prop_all_csttl(cstl,append(even_par_cstt[2],cstl_vars),[prop_eq_csttl]);
      [[["ternary_even_parity",
              [v3,v4,
               veq(even_par_ns(even_par_ns(1,["even_parity",cstt_id_ns])),
                   even_par_ns(even_par_ns(2,["even_parity",cstt_id_ns])))],
              lambda([a],
                     lambda([a],even_par_ns(even_par_split_namespace(a,["even_parity",cstt_id_ns])))(
                      even_par_split_namespace(a,["even_parity",cstt_id_ns])))],
        ["ternary_even_parity",
              [v1,v2,
               veq(even_par_ns(even_par_ns(1,["even_parity",cstt_id_ns])),
                   even_par_ns(even_par_ns(2,["even_parity",cstt_id_ns])))],
              lambda([a],
                     lambda([a],even_par_ns(even_par_split_namespace(a,["even_parity",cstt_id_ns])))(
                      even_par_split_namespace(a,
                                               ["even_parity",1,
                                                lambda([a],
                                                       even_par_ns(
                                                        even_par_split_namespace(
                                                         a,["even_parity",cstt_id_ns])))])))]],
            [v1,v2,v3,v4,
             veq(even_par_ns(even_par_ns(1,["even_parity",cstt_id_ns])),
                 even_par_ns(even_par_ns(2,["even_parity",cstt_id_ns])))]]
       
  • The variables:
    even_par_ns(even_par_ns(1,["even_parity",cstt_id_ns]))
    even_par_ns(even_par_ns(2,["even_parity",cstt_id_ns]))
       
    have been replaced with the single variable:
    veq(even_par_ns(even_par_ns(1,["even_parity",cstt_id_ns])),
        even_par_ns(even_par_ns(2,["even_parity",cstt_id_ns])))
       

Definition in file ConstraintTemplateRewriteSystem.hpp.