MIT OpenCourseWarehttp://ocw.mit.edu 6.005 Elements of Software Construction Fall 2008 For information about citing these materials or our Terms of Use, visit: http://ocw.mit.edu/terms. 6.005elements ofsoftwareconstruction how to design a SAT solver, part 2Daniel Jackson plan for todaytopics ‣ designing a naive solver ‣ more recursive functions over datatypes today’s patterns ‣ Interpreter: recursive traversals (again) ‣ Backtracking Search ‣ Facade for simpler use of API 2 © Daniel Jackson 2008 where we aredatatype productionslast time we saw ‣ how to model formulas using datatype productions ‣ like a grammar, but abstract structure only productions Formula = OrFormula + AndFormula + Not(formula:Formula)+ Var(name:String)OrFormula = OrVar(left:Formula,right:Formula)AndFormula = And(left:Formula,right:Formula)sample formula: (P ∨ Q) ∧ (¬P ∨ R) ‣ as a term: And(Or(Var(“P”), Var(“Q”)), (Not(Var(“P”)), Var(“R”))) 4 © Daniel Jackson 2008 Variant as Class patternlast time we saw ‣ how to define a datatype to model a set of values ‣ how to build a class structure representing it ‣ how to implement recursive functions over the datatype example ‣ production List = Empty + Cons (first: E, rest: List) ‣ code public abstract class List {}public class Empty extends List {}public class Cons extends List { private final E first; private final List rest; public Cons (E e, List r) {first = e;rest = r;} public E first () {return first;} public List rest () {return rest;}} 5 © Daniel Jackson 2008 Interpreter patternhow to build a recursive traversal ‣ write type declaration of function size: List -> int ‣ break function into cases, one per variant List = Empty + Cons(first:E, rest: List)size (Empty) = 0size (Cons(first:e, rest: l)) = 1 + size(rest)‣ implement with one subclass method per case public abstract class List { public abstract int size ();}public class Empty extends List { public int size () {return 0;}}public class Cons extends List { private final E first; private final List rest; public int size () {return 1 + rest.size();}}6 © Daniel Jackson 2008 SAT solver functionsfunctions for SATgenerate and test strategy ‣ steps extract set of variables from formula try all environments over those vars evaluate the formula for each ‣ functions vars: Formula -> Set solve: Formula -> Option eval: Formula, Env -> Bool 8 © Daniel Jackson 2008 set and envwhat are the Set and Env types? ‣ can define as datatypes too Set = ListEnv = List>Boolean = True + Falsesomething new going on here ‣ what is the meaning of equals in Set = List ? ‣ representation (on right) is hidden from clients ‣ not all terms are acceptable: no duplicates, eg ‣ more on this later when we discuss abstract types 9 © Daniel Jackson 2008 set and env specsassume for now ‣ Set and Env implemented as classes, with list representations ‣ but offering special methods: public class Set { public Set () {...} public Set add (E e) {...} public Set remove (E e) {...} public Set addAll (Set s) {...} public boolean contains (E e) {...} public E choose () {...} public boolean isEmpty () {...} public int size () {...}}public class Env {public Env() {...}public Env put(Var v, boolean b) {...}public boolean get(Var v) {...} //requires: v is bound in this environment}10 © Daniel Jackson 2008 computing var set applying strategy ‣ write type declaration of function vars: Formula -> Set ‣ break function into cases, one per variant F = Var(name:String) + Or(left:F,right:F) + And(left:F,right:F) + Not(formula:F)vars (Var(n)) = {Var(n)}vars (Or(fl, fr)) = vars(fl) ∪ vars(fr)vars (And(fl, fr)) = vars(fl) ∪ vars(fr)vars (Not(f)) = vars(f)‣ implement with one subclass method per case, eg public class AndFormula extends Formula {private final Formula left, right;public Set vars () {return left.vars().addAll(right.vars()); }}11 © Daniel Jackson 2008 vars in full public abstract class Formula {public abstract Set vars ();}public class AndFormula extends Formula {private final Formula left, right;public Set vars () {return left.vars().addAll(right.vars()); }}public class OrFormula extends Formula {private final Formula left, right;public Set vars () {return left.vars().addAll(right.vars()); }}public class NotFormula extends Formula {private final Formula formula;public Set vars () {return formula.vars(); }}public class Var extends Formula {public Set vars () {return new ListSet().add(this);}}12 © Daniel Jackson 2008 in-class exerciseapply the strategy for eval ‣ write type declaration of function eval: Formula, Env -> Boolean ‣ break function into cases, one per variant F = Var(name:String) + Or(left:F,right:F) + And(left:F,right:F) + Not(formula:F)eval (Var(n), e) = e.get(Var(n))eval (Or(fl, fr), e) = eval(fl,e) || evals(fr,e)eval (And(fl, fr), e) = eval(fl,e) && eval(fr,e)eval (Not(f), e) = ! eval(f,e)‣ implement with one subclass method per case, eg public class AndFormula extends Formula {private final Formula left, right;public boolean eval (Env e) {return left.eval (e) && right.eval (e); }}13 © Daniel Jackson 2008 eval in full public abstract class Formula { public abstract boolean eval (Env e);}public class AndFormula extends Formula {private final Formula left, right;public boolean eval (Env e) {return left.eval (e) && right.eval (e); }}public class OrFormula extends Formula {private final Formula left, right;public boolean eval(Env e) {return left.eval(e) || right.eval(e); }}public class NotFormula extends Formula {private final Formula formula;public boolean eval (Env e) {return !formula.eval (e); }public class Var extends Formula {public boolean eval (Env e) {return e.get(this); }}© Daniel Jackson 2008 14 a naive solvernaive SATbacktracking search ‣ pick a var, and try setting to false and then to true if that fails ‣ do this recursively, evaluating the formula when no vars left implementation public abstract class Formula { ...public Env solve () { return solve (new Env (), this.vars()); }private Env solve(Env env, Set vars) {if (vars.isEmpty())return eval(env) ? env : null; Var v = vars.choose(); Set restVars = vars.remove(v); Env e = solve (env.put(v, false), restVars); if (e != null) return e; return solve (env.put(v, true), restVars); }}16 © Daniel Jackson 2008 example ‣ formula f = Socrates⇒Human ∧ Human⇒Mortal ∧ ¬ (Socrates⇒Mortal) ‣ vars(f) = {Socrates, Human, Mortal} ‣ possible environments {Socrates->False, Human->False, Mortal->False} {Socrates->False, Human->False, Mortal->True} {Socrates->False, Human->True, Mortal->False} {Socrates->False, Human->True, Mortal->True} {Socrates->True, Human->False, Mortal->False} {Socrates->True, Human->False, Mortal->True} {Socrates->True, Human->True, Mortal->False} {Socrates->True, Human->True, Mortal->True} ‣ formula evaluates to false on all, so theorem holds 17© Daniel Jackson 2008 class exercisewhat order are environments checked in?‣ depends on behaviour of Set.choose ‣ assume it returns vars in this order Socrates, Human, Mortal 18© Daniel Jackson 2008running the example public static void main (String[] args) { Var s = new Var ("Socrates");Var h = new Var ("Human"); Var m = new Var ("Mortal");Formula old_f = new AndFormula (new OrFormula (new NotFormula (s), h), new AndFormula (new OrFormula (new NotFormula (h), m), new NotFormula (new OrFormula (new NotFormula (s), m))));Environment e = f.solve(); } System.out.println ("Solution: " + (e == null ? "none" : e)); Courtesy of The Eclipse Foundation. Used with permission. 19 © Daniel Jackson 2008 solving a Latin square long started = System.nanoTime(); Sudoku s = new Sudoku (2); System.out.println ("Creating SAT formula..."); Formula f = s.getFormula(); System.out.println ("Solving with naive method..."); Environment e = f.solve(); System.out.println ("Interpreting solution..."); String solution = s.interpretSolution(e); System.out.println ("Solution is: \n" + solution); long time = System.nanoTime(); long timeTaken = (time -started); System.out.println ("Time:" + timeTaken/1000000 + "ms"); Creating SAT formula... Solving with naive method... Interpreting solution... Solution is: |3|4|2|1| |1|2|4|3| |4|3|1|2| |2|1|3|4| Time:797ms20© Daniel Jackson 2008 design extrasan awkward APIlook at how formula is created by client ‣ tedious to have to use constructors and multiple classes Formula f = new AndFormula (new OrFormula (new NotFormula (s), h), new AndFormula (new OrFormula (new NotFormula (h), m), new NotFormula (new OrFormula (new NotFormula (s), m))));define methods in Formula class to avoid this: example of Facade public abstract class Formula {public Formula and (Formula f) {return new AndFormula (this, f);}public Formula or (Formula f) {return new OrFormula (this, f); }public Formula not () {return new NotFormula (this);}}‣ can now write Formula f = s.not().or(h).and(h.not().or(m).and(s.not().or(m).not()));22© Daniel Jackson 2008 module dependency diagram23© Daniel Jackson 2008handling unbound varshow should get method handle unbound var? ‣ one approach: return an arbitrary value ‣ technically correct, but not very robust public class Environment { Map bindings; ... /** * requires that v is bound in this environment * @return the boolean value that v is bound to */public boolean get(Var v){ Boolean b = bindings.get(v); if (b==null) return false; else return b; } }24 © Daniel Jackson 2008 three-valued logican alternative: define 3 logical values Boolean = True + False + Undefined public enum Bool { TRUE, FALSE, UNDEFINED; public Bool and (Bool b) { if (this==FALSE || b==FALSE) return FALSE; if (this==TRUE && b==TRUE) return TRUE; return UNDEFINED; } ...}now we can return undefined /*** @return the boolean value that v is bound to, or* the special UNDEFINED value of it is not bound*/public Bool get(Var v){Bool b = bindings.get(v);if (b==null) return Bool.UNDEFINED;else return b; }25© Daniel Jackson 2008 using Booluse methods of Bool instead of &&, ||, etc public class AndFormula extends Formula { public Bool eval (Environment e) { return left.eval(e).and (right.eval (e)); } }and in solver, can evaluate before all vars are bound public Environment solve () { return solve (new Environment (), this.vars()); }private Environment solve(Environment env, Set vars) { if (eval(env) == Bool.TRUE) return env; if (eval(env) == Bool.FALSE) return null; Var v = vars.choose(); Set restVars = vars.remove(v); Environment e = solve (env.put(v, Bool.FALSE), restVars); if (e != null) return e; return solve (env.put(v, Bool.TRUE), restVars); }26 © Daniel Jackson 2008 puzzleintroduction of Bool ‣ produces dramatic performance improvement ‣ 4x4 Latin square actually doesn’t terminate without it ‣ what’s going on? 27© Daniel Jackson 2008return type of solverecall solve function ‣ prototype is solve: Formula -> Option ‣ recall option datatype Option = Some(value:T) + None how should this be implemented?‣ we used nulls ‣ is there a better way? 28 © Daniel Jackson 2008 look ma, no nulls!public class Option {}public class None extends Option{}public class Some extends Option{ private T value; public Some (T v) {value = v;} public T getValue () {return value;}}public void displaySolution () { Option o = solve (new Environment (), this.vars()); if (o instanceof Some) System.out.println ((Some) o).getValue(); else System.out.println ("No solution"); }private Option solve (Environment env, Set vars) { if (eval(env) == Bool.TRUE) return new Some(env); if (eval(env) == Bool.FALSE) return new None(); Var v = vars.choose();Set restVars = vars.remove(v); Option o = solve (env.put (c, Bool.FALSE), restVars);if (o instanceof Some) return o;return solve (env.put(v, Bool.TRUE), restVars);}29 © Daniel Jackson 2008 comparing optionstwo options for Option ‣ have solve return an Env or a null value ‣ implement Option directly others? ‣ throw an exception if not successful ‣ have solve return a pair (boolean, env) class discussion ‣ advantages and disadvantages of each 30 © Daniel Jackson 2008 abstract classes vs. interfaceswhat’s an abstract class?like a regular class ‣ but can’t be instantiated like an interface ‣ but can contain fields and method bodies ‣ methods not implemented are marked abstract why useful? ‣ can collect fields and methods common across subclasses eg: Formula.solve ‣ can use as Facade eg: Formula.and, Formula.or, Formula.not 32 © Daniel Jackson 2008 using interfaces insteadchanges to List ‣ code is now public interface List {}public class Empty implements List {}public class Cons implements List { private final E first; private final List rest; public Cons (E e, List r) {first = e;rest = r;} public E first () {return first;} public List rest () {return rest;}}33 © Daniel Jackson 2008 !xing size what becomes of this? public abstract class List { int size; public int size () {return size;} }public class Empty extends List { public EmptyList () {size = 0;}}public class Cons extends List { private final E first; private final List rest; private Cons (E e, List r) {first = e;rest = r;size = r.size()+1}} 34 © Daniel Jackson 2008 !xing facadeand what becomes of this? public abstract class Formula {public Environment solve (Formula f) {return ...; }public Formula and (Formula f) {return new AndFormula (this, f); }public Formula or (Formula f) { return new OrFormula (this, f);}public Formula not () { return new NotFormula (this); }}35 © Daniel Jackson 2008 formula facadepublic class Formulas {public static Environment solve (Formula f) { return ...; }public static Formula and (Formula f, Formula g) { return new AndFormula (f, g);}public static Formula or (Formula f, Formula g) {return new OrFormula (f, g); }public static Formula not (Formula f) { return new NotFormula (f);}}36 © Daniel Jackson 2008 interfaces vs. abstract classesadvantages of interfaces ‣ you know at compile time which method is executed ‣ enforces clean specification disadvantages ‣ need extra (singleton) class for facade ‣ can’t share code 37 © Daniel Jackson 2008 what’s wrong with our solver?a missed opportunitylook at what happens ‣ after Socrates⇒Human ∧ Human⇒Mortal ∧ ¬ (Socrates⇒Mortal) ‣ suppose order or evaluation is Socrates, Human, Mortal ‣ and suppose we set Socrates to true ‣ then clearly must set Human to true ‣ and then must set Mortal to true... ‣ but our solver ignores all this next time ‣ a real SAT solver ‣ implements this scheme with unit propagation 39 © Daniel Jackson 2008 summarysummarybig ideas ‣ backtracking search: easy with immutable types patterns ‣ Variant as Class: abstract class for datatype, one subclass/variant ‣ Interpreter: recursive traversal over datatype with method in each subclass ‣ Facade: make client of API dependent on only a single class where we are ‣ built a naive solver that works for small problems ‣ next time, a real SAT solver 41 © Daniel Jackson 2008