  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!




























 Let's generalize our problem a bit:
 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:
 take an example clause 
 and a sample variable assignment
 and we can see whether the assignment satisfies either of the 
 conditions in the clause
-> (false true)
 That allows us to make a function that tells us whether an
 assignment satisfies a particular clause.
-> true
 We can try each of the clauses in our example problem on our sample assignment
-> true
-> true
-> nil
-> true
 Another way to do that would be:
-> (true true nil true)
 And so a way to check whether they're all satisfied at once is:
-> false
 So here's a general mechanism to check whether an assignment is a
 solution to a problem
-> false
 Just to check, here's an assignment that isn't a solution
-> false
 And here's one that is
-> true
 How should we do our exhaustive search now?
 Firstly find all the variables mentioned in the problem
-> (:x2 :x1 :x4 :x3)
 Then find a way of generating all possible assignments of true and false to 
 those variables
-> ({})
-> ({:x1 true} {:x1 false})
-> ({:x1 true, :x2 true} {:x1 false, :x2 true} {:x1 true, :x2 false} {:x1 false, :x2 false})
-> ({: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})
 {:x2 true, :x1 false, :x4 false, :x3 true} 
 {:x2 false, :x1 true, :x4 true, :x3 false}
 We can now generate some test cases for future use:
 If we just say that either x1 or x2 needs to be true
-> ({:x2 true, :x1 true} {:x2 false, :x1 true} {:x2 true, :x1 false})
-> ({:x2 false, :x1 true} {:x2 true, :x1 false})
 Or we could specify that we want one with :x1 true
-> ({:x2 false, :x1 true})
 Or even demand that x1 is true and x2 is 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.
-> ({:x2 false, :x1 true, :x4 false, :x5 true, :x3 true})
 Good Old Clojure!
  2 - SAT : Generalizing a Bit


  The instance of 2 - SAT from last time :



(def problem [{:x1 true  :x2 true}
              {:x3 true  :x4 true}
              {:x1 false :x3 false}
              {:x2 false :x4 false}])


(def example-clause {:x1 true :x2 true})


(def sample-assignment {:x1 true :x2 false :x3 true :x4 false})


(for [[k v] example-clause] 

  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 .


(defn satisfies [assignment clause]
  (some identity (for [[k v] clause] 
                   (= (assignment k) v))))




  And we find as before that it satisfies the first , second and
  fourth clauses but not the third one .



(defn solves [assignment problem]
  (every? identity 
          (map (partial satisfies assignment) problem)))





(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))))))
        
      


  This gets back the two possible satisfying assignments that we worked out earlier :
(filter #(solves % problem) (all-assignments (distinct (mapcat keys problem))))


(defn exhaustive-search-solve [problem]
  (filter #(solves % problem) 
          (all-assignments (distinct (mapcat keys problem)))))



(exhaustive-search-solve
 [{:x1 true  :x2 true}]) 

  Then there are three ways of doing that

  But if we want one of them true and one of them false
(exhaustive-search-solve
 [{:x1 true  :x2 true} {:x1 false  :x2 false}]) 

  Then there are only two ways

(exhaustive-search-solve
 [{:x1 true  :x2 true} {:x1 false  :x2 false} {:x1 true}]) 

(exhaustive-search-solve
 [{:x1 true  :x2 true} {:x1 false  :x2 false} {:x1 true} {:x2 true}]) 



(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}
  ]) 





























