约束满足问题

Question

我正在努力通过人工智能:现代方法,以减轻我的自然愚蠢.在尝试解决一些练习时,我遇到了"谁拥有斑马"问题,第5章练习5.13 .这是一个关于SO的主题,但回答主要是针对"如果您可以自由选择解决问题的软件,您将如何解决这个问题？"

我接受Prolog是一种非常适合这类问题的编程语言,并且有一些很好的软件包可用,例如在Python中,如排名靠前的答案所示,也是独立的.唉,这一切都没有帮助我以书中概述的方式"强硬".

本书似乎建议构建一组双重或全局约束,然后实现一些提到的算法以找到解决方案.我遇到了一系列适用于建模问题的约束,我遇到了很多麻烦.我正在研究这个问题,所以我无法接触到教授或TA让我超过驼峰 - 这就是我要求你帮助的地方.

---

我认为本章中的例子几乎没有相似之处.

我渴望建立双重约束,开始了创建(逻辑等价)25个变量:nationality1,nationality2,nationality3,... nationality5,pet1,pet2,pet3,... pet5,drink1... drink5等等,其中数字是表示房子的的位置.

这对于构建一元约束是很好的,例如

挪威人住在第一宫:

nationality1 = { :norway }.

但是大多数约束是通过共同的门牌号码组合两个这样的变量,例如

瑞典人有一条狗:

nationality[n] = { :sweden } AND pet[n] = { :dog }

n显然,在哪里可以从1到5.或者说另一种方式:

    nationality1 = { :sweden } AND pet1 = { :dog } 
XOR nationality2 = { :sweden } AND pet2 = { :dog } 
XOR nationality3 = { :sweden } AND pet3 = { :dog } 
XOR nationality4 = { :sweden } AND pet4 = { :dog } 
XOR nationality5 = { :sweden } AND pet5 = { :dog } 

...与本书所倡导的"元组列表"有着截然不同的感觉:

( X1, X2, X3 = { val1, val2, val3 }, { val4, val5, val6 }, ... )

---

我本身并不是在寻求解决方案; 我正在寻找一个如何以与本书的方法兼容的方式来模拟这个问题的开始.任何帮助赞赏.

Answer 1

感谢大家提供一些有用的信息！

\n\n

我真正需要的提示是在交通堵塞时出现的。我需要做的不是将国籍、宠物等分配给房屋（变量名为country1、country2、pet1、pet2），而是将房屋分配给域的元素！例子：

\n\n

(9) norway = 1        ; unary constraint: The Norwegian lives in the 1st house\n(2) britain = dog     ; binary constraint: Dog is in same house as the Brit\n(4) green - ivory = 1 ; relative positions\n

\n\n

这使我能够找到适合我的约束的简单公式，如下所示：

\n\n

(def constraints\n  #{\n   [:con-eq :england :red]\n   [:con-eq :spain :dog]\n   [:abs-pos :norway 1]\n   [:con-eq :kools :yellow]\n   [:next-to :chesterfields :fox]\n   [:next-to :norway :blue]\n   [:con-eq :winston :snails]\n   [:con-eq :lucky :oj]\n   [:con-eq :ukraine :tea]\n   [:con-eq :japan :parliaments]\n   [:next-to :kools :horse]\n   [:con-eq :coffee :green]\n   [:right-of :green :ivory]\n   [:abs-pos :milk 3]\n   })\n

\n\n

我还没有完成（这只是部分时间的推杆），但一旦我解决了，我将发布一个完整的解决方案。

\n\n\n\n

更新：大约两周后，我在 Clojure 中提出了一个可行的解决方案：

\n\n

(ns houses\n  [:use [htmllog] clojure.set]  \n  )\n\n(comment\n  [ 1] The Englishman lives in the red house.\n  [ 2] The Spaniard owns the dog.\n  [ 3] The Norwegian lives in the \xef\xac\x81rst house on the left.\n  [ 4] Kools are smoked in the yellow house.\n  [ 5] The man who smokes Chester\xef\xac\x81elds lives in the house next to the man with the fox.\n  [ 6] The Norwegian lives next to the blue house.\n  [ 7] The Winston smoker owns snails.\n  [ 8] The Lucky Strike smoker drinks orange juice.\n  [ 9] The Ukrainian drinks tea.\n  [10] The Japanese smokes Parliaments.\n  [11] Kools are smoked in the house next to the house where the horse is kept.\n  [12] Coffee is drunk in the green house.\n  [13] The Green house is immediately to the right (your right) of the ivory house.\n  [14] Milk is drunk in the middle house.\n\n  \xe2\x80\x9cWhere does the zebra live, and in which house do they drink water?\xe2\x80\x9d\n)\n\n(def positions #{1 2 3 4 5})\n\n(def categories {\n          :country #{:england :spain :norway :ukraine :japan}\n          :color #{:red :yellow :blue :green :ivory}\n          :pet #{:dog :fox :snails :horse :zebra}\n          :smoke #{:chesterfield :winston :lucky :parliament :kool}\n          :drink #{:orange-juice :tea :coffee :milk :water}\n})\n\n(def constraints #{\n                    ; -- unary\n          \'(at :norway 1) ; 3\n          \'(at :milk 3) ; 14\n                    ; -- simple binary\n          \'(coloc :england :red) ; 1\n          \'(coloc :spain :dog) ; 2\n          \'(coloc :kool :yellow) ; 4\n          \'(coloc :winston :snails) ; 7\n          \'(coloc :lucky :orange-juice) ; 8\n          \'(coloc :ukraine :tea) ; 9\n          \'(coloc :japan :parliament) ; 10\n          \'(coloc :coffee :green) ; 12\n                    ; -- interesting binary\n          \'(next-to :chesterfield :fox) ; 5\n          \'(next-to :norway :blue) ; 6\n          \'(next-to :kool :horse) ; 11\n          \'(relative :green :ivory 1) ; 13\n})\n\n; ========== Setup ==========\n\n(doseq [x (range 3)] (println))\n\n(def var-cat    ; map of variable -> group \n      ; {:kool :smoke, :water :drink, :ivory :color, ... \n    (apply hash-map (apply concat \n        (for [cat categories vari (second cat)] \n      [vari (first cat)]))))\n\n(prn "var-cat:" var-cat)\n\n(def initial-vars    ; map of variable -> positions\n      ; {:kool #{1 2 3 4 5}, :water #{1 2 3 4 5}, :ivory #{1 2 3 4 5}, ...\n    (apply hash-map (apply concat \n        (for [v (keys var-cat)] [v positions]))))\n\n(prn "initial-vars:" initial-vars)\n\n(defn apply-unary-constraints\n   "This applies the \'at\' constraint. Separately, because it only needs doing once." \n   [vars]\n   (let [update (apply concat\n      (for [c constraints :when (= (first c) \'at) :let [[v d] (rest c)]]\n   [v #{d}]))]\n      (apply assoc vars update)))\n\n(def after-unary (apply-unary-constraints initial-vars))\n\n(prn "after-unary:" after-unary)\n\n(def binary-constraints (remove #(= \'at (first %)) constraints))\n\n(prn "binary-constraints:" binary-constraints)\n\n; ========== Utilities ==========\n\n(defn dump-vars\n   "Dump map `vars` as a HTML table in the log, with `title`." \n   [vars title]\n  (letfn [\n        (vars-for-cat-pos [vars var-list pos]\n          (apply str (interpose "<br/>" (map name (filter #((vars %) pos) var-list)))))]\n      (log-tag "h2" title)\n    (log "<table border=\'1\'>")\n    (log "<tr>")\n    (doall (map #(log-tag "th" %) (cons "house" positions)))\n    (log "</tr>")\n    (doseq [cat categories]\n      (log "<tr>")\n          (log-tag "th" (name (first cat)))\n          (doseq [pos positions]\n          (log-tag "td" (vars-for-cat-pos vars (second cat) pos)))\n      (log "</tr>")\n      )\n    (log "</table>")))\n\n(defn remove-values\n   "Given a list of key/value pairs, remove the values from the vars named by key." \n   [vars kvs]\n   (let [names (distinct (map first kvs))\n      delta (for [n names]\n      [n (set (map second (filter #(= n (first %)) kvs)))])\n      update (for [kv delta\n         :let [[cname negative] kv]]\n      [cname (difference (vars cname) negative)])]\n      (let [vars (apply assoc vars (apply concat update))]\n   vars)))\n\n(defn siblings\n   "Given a variable name, return a list of the names of variables in the same category."\n   [vname]\n   (disj (categories (var-cat vname)) vname))\n\n(defn contradictory?\n   "Checks for a contradiction in vars, indicated by one variable having an empty domain." \n   [vars]\n   (some #(empty? (vars %)) (keys vars)))\n\n(defn solved?\n   "Checks if all variables in \'vars\' have a single-value domain."\n   [vars]\n   (every? #(= 1 (count (vars %))) (keys vars)))\n\n(defn first-most-constrained\n   "Finds a variable having the smallest domain size > 1."\n   [vars]\n   (let [best-pair (first (sort (for [v (keys vars) :let [n (count (vars v))] :when (> n 1)] [n v])))]\n      (prn "best-pair:" best-pair)\n      (second best-pair)))   \n\n;========== Constraint functions ==========\n\n   (comment\n      These functions make an assertion about the domains in map \'bvars\', \n      and remove any positions from it for which those assertions do not hold. \n      They all return the (hopefully modified) domain space \'bvars\'.)\n\n   (declare bvars coloc next-to relative alldiff solitary)\n\n   (defn coloc\n      "Two variables share the same location." \n      [vname1 vname2]\n      (if (= (bvars vname1) (bvars vname2)) bvars\n   (do\n      (let [inter (intersection (bvars vname1) (bvars vname2))]\n         (apply assoc bvars [vname1 inter vname2 inter])))))\n\n   (defn next-to \n      "Two variables have adjoining positions"\n      [vname1 vname2]\n      ; (prn "doing next-to" vname1 vname2)\n      (let [v1 (bvars vname1) v2 (bvars vname2)\n            bad1 (for [j1 v1 :when (not (or (v2 (dec j1)) (v2 (inc j1))))] [vname1 j1])\n        bad2 (for [j2 v2 :when (not (or (v1 (dec j2)) (v1 (inc j2))))] [vname2 j2])\n         allbad (concat bad1 bad2)]\n   (if (empty? allbad) bvars \n      (do\n         (remove-values bvars allbad)))))\n\n   (defn relative\n      "(position vname1) - (position vname2) = diff"  \n      [vname1 vname2 diff]\n      (let [v1 (bvars vname1) v2 (bvars vname2)\n       bad1 (for [j1 v1 :when (not (v2 (- j1 diff)))] [vname1 j1])\n         bad2 (for [j2 v2 :when (not (v1 (+ j2 diff)))] [vname2 j2])\n         allbad (concat bad1 bad2)]\n   (if (empty? allbad) bvars\n      (do\n         (remove-values bvars allbad)))))\n\n   (defn alldiff\n      "If one variable of a category has only one location, no other variable in that category has it."\n      []\n      (let [update (apply concat\n   (for [c categories v (val c) :when (= (count (bvars v)) 1) :let [x (first (bvars v))]]\n      (for [s (siblings v)]\n         [s x])))]\n   (remove-values bvars update)))\n\n   (defn solitary\n      "If only one variable of a category has a location, then that variable has no other locations."\n      []\n      (let [loners (apply concat\n   (for [c categories p positions v (val c) \n      :when (and \n         ((bvars v) p)\n         (> (count (bvars v)) 1)\n         (not-any? #((bvars %) p) (siblings v)))]\n      [v #{p}]))]\n      (if (empty? loners) bvars\n   (do\n      ; (prn "loners:" loners)\n      (apply assoc bvars loners)))))\n\n;========== Solving "engine" ==========\n\n(open)\n\n(dump-vars initial-vars "Initial vars")\n\n(dump-vars after-unary "After unary")\n\n(def rules-list (concat (list \'(alldiff)) binary-constraints (list \'(solitary))))\n\n(defn apply-rule\n   "Applies the rule to the domain space and checks the result." \n   [vars rule]\n   (cond\n      (nil? vars) nil\n      (contradictory? vars) nil\n      :else \n   (binding [bvars vars]\n   (let [new-vars (eval rule)]\n      (cond\n         (contradictory new-vars) (do \n      (prn "contradiction after rule:" rule) \n      nil)\n         (= new-vars vars) vars  ; no change\n         :else (do \n      (prn "applied:" rule)\n      (log-tag "p" (str "applied: " (pr-str rule))) \n      (prn "result: " new-vars) \n      new-vars))))))\n\n(defn apply-rules \n   "Uses \'reduce\' to sequentially apply all the rules from \'rules-list\' to \'vars\'."\n   [vars]\n   (reduce apply-rule vars rules-list))\n\n(defn infer\n   "Repeatedly applies all rules until the var domains no longer change." \n   [vars]\n   (loop [vars vars]\n      (let [new-vars(apply-rules vars)]\n      (if (= new-vars vars) (do \n         (prn "no change")\n         vars)\n      (do (recur new-vars))))))\n\n(def after-inference (infer after-unary))\n\n(dump-vars after-inference "Inferred")\n\n(prn "solved?" (solved? after-inference))\n\n(defn backtrack\n   "solve by backtracking."\n   [vars]\n   (cond\n      (nil? vars) nil\n      (solved? vars) vars\n      :else\n      (let [fmc (first-most-constrained vars)]\n   (loop [hypotheses (seq (vars fmc))]\n      (if (empty? hypotheses) (do\n         (prn "dead end.")\n         (log-tag "p" "dead end.")\n         nil)\n         (let [hyp (first hypotheses) hyp-vars (assoc vars fmc #{hyp})]\n      (prn "hypothesis:" fmc hyp)\n      (log-tag "p" (str "hypothesis: " hyp))\n      (dump-vars hyp-vars (str "Hypothesis: " fmc " = " hyp))\n      (let [bt (backtrack (infer hyp-vars))]\n         (if bt (do\n      (prn "success!")\n         (dump-vars bt "Solved")\n         bt)\n      (recur (rest hypotheses))))))))))\n\n(prn "first-most-constrained:" (first-most-constrained after-inference))\n\n(def solution (backtrack after-inference))\n\n(prn "solution:" solution)\n\n(close)\n\n(println "houses loaded.")\n

\n\n

这是 292 行，但是里面有很多调试/诊断代码。总而言之，我很高兴能够在 Clojure 中管理出一个相当简短的解决方案。函数式编程带来了一些挑战，但我设法保持了相当一致的函数式风格。

\n\n

不过欢迎批评！

\n\n\n\n

对于任何关心的人，这里是解决方案：

\n\n

house       1       2               3       4             5\ncountry     norway  ukraine         england spain         japan\ncolor       yellow  blue            red     ivory         green\npet         fox     horse           snails  dog           zebra\nsmoke       kool    chesterfield    winston lucky         parliament\ndrink       water   tea             milk    orange-juice  coffee\n

\n