;; 2-SAT : Generalizing a Bit ;; Let's generalize our problem a bit: ;; The instance of 2-SAT from last time: ;; Either x1 must be true or x2 must be true ;; Either x3 must be true or x4 must be true ;; Either x1 must be false or x3 must be false ;; Either x2 must be false or x4 must be false ;; in a more general form might look like: (def problem [{:x1 true :x2 true} {:x3 true :x4 true} {:x1 false :x3 false} {:x2 false :x4 false}]) ;; take an example clause (def example-clause {:x1 true :x2 true}) ;; and a sample variable assignment (def sample-assignment {:x1 true :x2 false :x3 true :x4 false}) ;; and we can see whether the assignment satisfies either of the ;; conditions in the clause (for [[k v] example-clause] (= (sample-assignment k) v)) ;-> (false true) ;; In this case, the clause says that either variable 1 must be true ;; (which is true) or variable 2 must be true (which is false). Since ;; one of the clauses' conditions is satisfied, this clause overall is happy. ;; That allows us to make a function that tells us whether an ;; assignment satisfies a particular clause. (defn satisfies [assignment clause] (some identity (for [[k v] clause] (= (assignment k) v)))) (satisfies sample-assignment example-clause) ;-> true ;; We can try each of the clauses in our example problem on our sample assignment (satisfies sample-assignment {:x1 true :x2 true}) ;-> true (satisfies sample-assignment {:x3 true :x4 true}) ;-> true (satisfies sample-assignment {:x1 false :x3 false}) ;-> nil (satisfies sample-assignment {:x2 false :x4 false}) ;-> true ;; And we find as before that it satisfies the first, second and ;; fourth clauses but not the third one. ;; Another way to do that would be: (map (partial satisfies sample-assignment) problem ) ;-> (true true nil true) ;; And so a way to check whether they're all satisfied at once is: (every? identity (map (partial satisfies sample-assignment) problem)) ;-> false ;; So here's a general mechanism to check whether an assignment is a ;; solution to a problem (defn solves [assignment problem] (every? identity (map (partial satisfies assignment) problem))) (solves sample-assignment problem) ;-> false ;; Just to check, here's an assignment that isn't a solution (solves {:x1 true :x2 false :x3 true :x4 false} problem) ;-> false ;; And here's one that is (solves {:x1 true :x2 false :x3 false :x4 true} problem) ;-> true ;; How should we do our exhaustive search now? ;; Firstly find all the variables mentioned in the problem (distinct (mapcat keys problem)) ;-> (:x2 :x1 :x4 :x3) ;; Then find a way of generating all possible assignments of true and false to ;; those variables (defn all-assignments [vars] (if (empty? vars) '({}) (apply concat (for [a (all-assignments (rest vars))] (list (assoc a (first vars) true) (assoc a (first vars) false)))))) (all-assignments '()) ;-> ({}) (all-assignments '(:x1)) ;-> ({:x1 true} {:x1 false}) (all-assignments '(:x1 :x2)) ;-> ({:x1 true, :x2 true} {:x1 false, :x2 true} {:x1 true, :x2 false} {:x1 false, :x2 false}) (all-assignments '(:x1 :x2 :x3)) ;-> ({:x1 true, :x2 true, :x3 true} {:x1 false, :x2 true, :x3 true} {:x1 true, :x2 false, :x3 true} {:x1 false, :x2 false, :x3 true} {:x1 true, :x2 true, :x3 false} {:x1 false, :x2 true, :x3 false} {:x1 true, :x2 false, :x3 false} {:x1 false, :x2 false, :x3 false}) ;; This gets back the two possible satisfying assignments that we worked out earlier: (filter #(solves % problem) (all-assignments (distinct (mapcat keys problem)))) ;; {:x2 true, :x1 false, :x4 false, :x3 true} ;; {:x2 false, :x1 true, :x4 true, :x3 false} (defn exhaustive-search-solve [problem] (filter #(solves % problem) (all-assignments (distinct (mapcat keys problem))))) ;; We can now generate some test cases for future use: ;; If we just say that either x1 or x2 needs to be true (exhaustive-search-solve [{:x1 true :x2 true}]) ;; Then there are three ways of doing that ;-> ({:x2 true, :x1 true} {:x2 false, :x1 true} {:x2 true, :x1 false}) ;; But if we want one of them true and one of them false (exhaustive-search-solve [{:x1 true :x2 true} {:x1 false :x2 false}]) ;-> ({:x2 false, :x1 true} {:x2 true, :x1 false}) ;; Then there are only two ways ;; Or we could specify that we want one with :x1 true (exhaustive-search-solve [{:x1 true :x2 true} {:x1 false :x2 false} {:x1 true}]) ;-> ({:x2 false, :x1 true}) ;; Or even demand that x1 is true and x2 is true (exhaustive-search-solve [{:x1 true :x2 true} {:x1 false :x2 false} {:x1 true} {:x2 true}]) ;-> () ;; That leads to an unsatifiable problem. ;; I've just realized that I've accidentally over-generalised this to ;; be able to represent the general problem of boolean satisfiability. (exhaustive-search-solve [{:x1 false :x2 false} {:x2 false :x3 false :x4 false :x5 true} {:x1 true} {:x4 false :x1 false} {:x3 true :x2 false} {:x3 true :x4 true} {:x4 true :x5 true} ]) ;-> ({:x2 false, :x1 true, :x4 false, :x5 true, :x3 true}) ;; Good Old Clojure!

## Search This Blog

## Wednesday, October 16, 2013

### 2-SAT : Generalizing a Bit

Subscribe to:
Post Comments (Atom)

## No comments:

## Post a Comment