Final CSU 670 
Fall 2006
December 11, 2006				Karl Lieberherr
=================================================================


Question 1:
==========================================================
13 UNKNOWNs
3 points each, except UNKNOWN13 = 30 points
66 points = 12*3 + 30


Class dictionary design

Consider the following input and the corresponding cd.
Find the UNKNOWNs.

A little bit of context: The class dictionary is defining
a module language for class dictionaries and their
compositions.

module
  di TreeICG(ElementICG e) { 
    Tree : Leaf | Branch .
    Leaf = Data @ e.
    Branch = Data @ e ListOfTree.
    ListOfTree : Empty | NonEmpty.
    Empty = .
    NonEmpty = <f> Tree <r> ListOfTree.
  } 
  aspect TreeWalker { 
    declare strategy
    declare traversal
    declare constraints
  }
  // visitor classes
end
module
  di ElementICG { 
    Data = Name_ValuePair_List.
    NameValuePair = Name Value.
    Name = .
    Value = .
    Name_ValuePair_List : Empty | NonEmpty.
    Empty = .
    NonEmpty = <f> NameValuePair <r> Name_ValuePair_List.
  }
  aspect ElementWalker { 
    declare constraints
    declare strategy
    declare traversal
  }
  // visitor classes
end
module
  di Decide {
    F = Constraints.
    Constraints : E | N.
    E = .
    N = <f> Constraint <r> Constraints.
    Constraint = RelNumber <v1> Variable <v2> Variable.
    RelNumber = int.
    Variable = .
  }
  aspect Chooser {
    declare strategy
    declare constraints
    declare traversal
  }
end
cd XMLSubset implements TreeICG(ElementICG) {
  XMLDef = A <b> B.
  A : X | Y common <u> U V.

  map treeMap = for TreeICG { 
   use Tree as XMLDef
   use Leaf as EmptyTag
  }
  map elementMap = for ElementICG {
   use Data as OpenTag
   use Data as OpenCloseTag
  }
}

Here comes the cd:
==================================================

Input =
 List(Module)
 ConcreteCd EOF.
Module = "module" 
 UNKNOWN1 List(UNKNOWN2) 
 // list of visitor classes
"UNKNOWN3". 
DI = "di" DIName [UNKNOWN4] "{" UNKNOWN5 "}".
ParameterDI = "(" DIName DIVariable ")".
Aspect = "aspect" AspectName 
  UNKNOWN6.
Declaration UNKNOWN7.
Strategy UNKNOWN8.
Traversal UNKNOWN9.
Constraints UNKNOWN10.

ConcreteCd = "cd" CDName "implements" DIName [ActualDI] 
  "{" UNKNOWN11 "}".
ActualDI = "(" DIName ")".
Map = "map" MapName "=" "for" DIName UNKNOWN12(Basic). 
Basic = "use" <use> Cd_Vertex "as" <as> Cd_Vertex.

Cd_Graph = UNKNOWN13. // this is a big UNKNOWN
Cd_Vertex = < vertex_name > Cd_ClassName ["@" DIName] .

DIName = Ident.
DIVariable = Ident.
AspectName = Ident.
CDName = Ident.
MapName = Ident.

List(S) ~ {S}.
CList(S) ~ "{" {S} "}".
Main = <s> String.


Question 2:
Understanding Project Requirements
==========================================================

25 UNKNOWNs: 3 points each: 75 points

Consider the following formula F;
Notice the identation to make the structure of the
formula more apparent.

22(v1 v2 v3)
22                (v4 v5 v6)
22                                (v7 v8 v9)
22(v1              v4              v7)
22(   v2              v5              v8)
22(      v3              v6              v9)
22(v1                 v5                 v9)
22(      v3           v5           v7)

Part 1: unsatisfiable
---------------------------------

Enclosed is the proof for the unsatisfiability of the formula F produced by one of your programs.
I replaced the long formula by F to make the proof more readable.
Find the UNKNOWNs. 
Sort the literals lexicographically within the unknowns. For example,
write "UNKNOWN105 = v7 v37 !v40" instead of "UNKNOWN105 = !v40 v7 v37"
In the proof below, multiple Unit Propagate rules are combined
into Unit Propagate*.

UNSAT
{{
v5*  || F 
=>      UNKNOWN1

v5* UNKNOWN2 || F
=>      UNKNOWN3

Contradiction
Put an unsatisfied clause in UNKNOWN4

UNKNOWN5 || F 240(!v5 ) 
=>      Semi-Super Resolution

 || F UNKNOWN6
=>      UNKNOWN7

!v5  || F 240(!v5 ) 
=>      Unit Propagate*

!v5 v9*  || F 240(!v5 ) 
=>      Decide

!v5 v9* UNKNOWN8 || F 240(!v5 ) 
=>      Unit Propagate*

Contradiction
Put an unsatisfied clause in UNKNOWN9

!v5 v9* UNKNOWN10 || F 240(!v5 ) UNKNOWN11
=>      UNKNOWN12

 || F 240(!v5 ) 240(!v9 ) 
=>      UNKNOWN13

UNKNOWN14 || F 240(!v5 ) UNKNOWN15
=>      Unit Propagate*

Contradiction
Put an unsatisfied clause in UNKNOWN16

FAILSTATE       
=>      Fail

F  = 22(v1 v2 v3 ) 22(v4 v5 v6 ) 22(v7 v8 v9 ) 22(v1 v4 v7 ) 
     22(v2 v5 v8 ) 22(v3 v6 v9 ) 22(v1 v5 v9 ) 22(v3 v5 v7 ) 

}}

Part 2: satisfiable
-------------------------------------------

Delete the last constraint 
22(      v3           v5           v7)
from F and find a satisfying assignment.

Put your answer into the UNKNOWNs:

v1 = UNKNOWN17
v2 = UNKNOWN18
v3 = UNKNOWN19
v4 = UNKNOWN20
v5 = UNKNOWN21
v6 = UNKNOWN22
v7 = UNKNOWN23
v8 = UNKNOWN24
v9 = UNKNOWN25


Question 3:
==========================================================

11 UNKNOWNs:
UNKNOWNs 1 - 4: 5 points each
UNKNOWN 5: 15 points
remaining UNKNOWNs: 3 points each:
20 + 15 + 18 = 53

This question is about semantic 
checking in the context of a planning application. 
Such plans are successfully solved by
translating the plans to CSP instances
(but here we are not concerned with the translation).
The structure of a plan is given by the class dictionary
called Plans. A plan consists of objects, predicates and
operators.

The objects part defines the objects that may be used elsewhere
in the plan.
The predicates part defines the predicate namess that may be used elsewhere
in the plan.
The operators part defines the operator names
that may be used elsewhere
in the plan and it gives the definies of the operators in terms
of preconditions and effects.

The class dictionary, program and input and output are given
below. Find the UNKNOWNs.
UNKNOWN1 to UNKNOWN4  are titles that get printed.
They have a special status and must be derived
from understanding the semantic checking problem. Each
appears twice in the text.
The titles must succinctly describe the nature of the output
that follows.
UNKNOWN5 is a short piece of program text.


// class dictionary Plans

import edu.neu.ccs.demeter.dj.*;
import java.util.*;

Plans = Set(Plan).
Plan = "objects" <objects> Set(Obj) 
  "predicates" <predicates> Set(PredName) 
  "operators" <operators> Set(Op) 
  "initial" <initial> Set(PosLit) 
  "goal" <goal> Set(Literal)
  "solution" Set(OpName).
Literal : PosLit | NegLit common PredName <args> Set(Obj).
PosLit = .
NegLit = "!".
Op = OpName "preconditions" <preconditions> Set(Literal) 
            "effects" <effects> Set(Literal).

Obj = Ident.
PredName = Ident.
OpName = Ident.

Set(S) ~ "(" {S} ")".
Main = .


PROGRAM
-------------------------------------------------------------------

Main {
  public static void main(String args[]) throws Exception {{
    Plans m = Plans.parse(System.in);
    ClassGraph cg1 = new ClassGraph(true, false);
    final ClassGraph cg = new ClassGraph(cg1,
        "from Plans bypassing -> *,tail,* to *");
    cg.traverse(m, "from Plans to Plan", new Visitor(){
      void before(Plan host) {
        host.process(cg); }
      });

    System.out.println("done");
  }}
}
Plan {
{{
  void process(ClassGraph cg){
    System.out.println(" UNKNOWN1 ");
    cg.traverse(this
    ,"from Plan via ->*,objects,* to Obj", new Visitor(){
      void before (Obj host) {System.out.println(host.get_ident());}
      });
    System.out.println(" UNKNOWN2 ");
    cg.traverse(this
    ,"from Plan bypassing ->*,objects,* to Obj", new Visitor(){
      void before (Obj host) {System.out.println(host.get_ident());}
      });
    System.out.println(" UNKNOWN3 ");
    cg.traverse(this
    ,"from Plan via ->*,predicates,* to PredName", new Visitor(){
      void before (PredName host) {System.out.println(host.get_ident());}
      });
    System.out.println(" UNKNOWN4 ");
    cg.traverse(this
    ,"from Plan bypassing ->*,predicates,* to PredName", new Visitor(){
      void before (PredName host) {System.out.println(host.get_ident());}
      });
    System.out.println("The number of operators defined by the plan ");
    UNKNOWN5;
  }
}}
}

INPUT
-------------------------------------------------------------

(
objects (Battery1 Battery2 Cap Flashlight)
predicates (On In)
operators (
  PlaceCap 
  preconditions (!On(Cap Flashlight))
  effects (On(Cap Flashlight))
  RemoveCap 
  preconditions (On(Cap Flashlight))
  effects (!On(Cap Flashlight))
  Insert1
  preconditions (!On(Cap Flashlight) !In(Battery1 Flashlight))
  effects (In(Battery1 Flashlight))
  Insert2
  preconditions (!On(Cap Flashlight) !In(Battery2 Flashlight))
  effects (In(Battery2 Flashlight))
  )
initial (On(Cap Flashlight))
goal ( 
       On(Cap Flashlight) 
       In(Battery1 Flashlight)
       In(Battery2 Flashlight)
     )
solution(RemoveCap Insert1 Insert2 PlaceCap)
)

OUTPUT
-------------------------------------------------------------


 UNKNOWN1 
UNKNOWN6
UNKNOWN7
UNKNOWN8
UNKNOWN9
 UNKNOWN2 
Cap
Flashlight
Cap
Flashlight
Cap
Flashlight
Cap
Flashlight
Cap
Flashlight
Battery1
Flashlight
Battery1
Flashlight
Cap
Flashlight
Battery2
Flashlight
Battery2
Flashlight
Cap
Flashlight
Cap
Flashlight
Battery1
Flashlight
Battery2
Flashlight
 UNKNOWN3 
UNKNOWN10
UNKNOWN11
 UNKNOWN4 
On
On
On
On
On
In
In
On
In
In
On
On
In
In
The number of operators defined by the plan 
4
done


Question 4:
=========================================================

Describe how you would express the Sudoku game 
as a constraint satisfaction problem. Which relations would you use
and which constraints would you produce?
How would you use a solver we developed for the class to
solve Sudoku?