Bug fixes for Java API + Exactly one constraints + Adding support for getting the...

[satune.git] / design / notes.txt

diff --git a/design/notes.txt b/design/notes.txt
index ce399c3dad0558df114fe9188003be550f30124f..f7282be8883bf8bad2ba8e2c1809646ef6ad41df 100644 (file)
--- a/design/notes.txt
+++ b/design/notes.txt
@@ -1,6 +1,8 @@
 (1) Elements/BooleanVars should link back to expressions that use them
 (1) Elements/BooleanVars should link back to expressions that use them

+--> Done

 
 (2) Need to introduce variables in encoding of functions....
 
 (2) Need to introduce variables in encoding of functions....

+--> Done

 
 (3) Some cases can do variable elimination of introduced variables...
 
 
 (3) Some cases can do variable elimination of introduced variables...
 


@@ -9,3 +11,84 @@ future?
 
 (5) Could simplify output of functions...  Maybe several outputs have
 same effect...
 
 (5) Could simplify output of functions...  Maybe several outputs have
 same effect...

+
+
+Work/Passes:
+
+(1) TreeConstruction --- need backwards links...
+BooleanVar/ElementVar should be able to query all of its uses.  Should
+go all the way up...
+
+(2) Naive Encoding Pass --- add an encoding to every Element/Function...
+
+(3) Encoder Pass --- implement encodings into constraint objects...
+
+(4) Test...  Make sure the thing works...
+
+Next basic implementation phase:
+(1) Extend Naive Encoder Pass to test other encodings
+(2) Build more clever function encodings strategies (e.g., equals, add, etc)...
+(3) Test
+
+Actual research:
+
+(1) TreeRewriting --- probably should do Equivalent Subexpression
+Elimination (Don't have the same expression appear twice, instead
+simply link to it again).  Possibly good to do in TreeConstruction...
+This could be lower priority as it isn't really essential to make
+things work.  Should also probably be switchable on/off...
+
+--> Done
+
+(2) Advanced TreeRewriting --- can rewrite functions/predicates to
+eliminate unused entries or to eliminate effectively identical
+outputs...  e.g., consider a function f() that can output the values
+1,3, 5, 7, and its output is only ever compared to 3...  We could
+rewrite the values 1, 5, and 7 to be the same value.
+
+(3) Advanced Encoding Strategies
+  a) encoding alignment --- making binary index encodings over
+different sets work together
+
+  b) Implement K-Map for function encoding
+
+(4) Implement search framework --- probably simulated annealing over a
+population of strategies...  search framework should probably be able
+to turn on/off nearly any optimization we have...
+
+(5) Implement backend translation strategies....do optimizations and
+implement other simplifcation strategies
+
+(6) Convert SATCheck to use Constraint Compiler...not sure about order...
+Started...
+
+(7) Profile system....
+
+---------------------------------------------------------------------
+
+To do:
+
+(0) Support for saving/loading problem instances...
+
+(1) Complete satcheck support
+
+(2) Advance tree rewriting...  Variable value elimination...
+
+(3) Think about undefined semantics...
+
+(4) Smart encoding...
+    Variable Graphs....
+
+    Split graph into connected components
+
+Encoding ideas:
+*    Monotonic increasing index
+*    Matched index (equality)
+*    Bit exposes
+*    Single var
+*    Support arithmetic
+*    Sparse encoding
+
+--------------------------------------------------------------------
+
+