Weighted MAX SAT CC-BY Fabian M. Suchanek
2 likes envies likes Refresh: Atoms and KBs An atom Ａ  is a propositional statement. Ａ  is a positive literal, and ¬ Ａ  is a negative literal. The polarity is positive for Ａ , and negative for  ¬ Ａ . A positive literal holds (“is true”) in a KB, if it appears in the KB. A negative literal ¬ Ａ  holds in a KB if Ａ  does not hold. ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ）   ? ¬ ｅｎｖｉｅｓ（Ｒｏｎ， Ｈａｒｒｙ）   ? We work here under the closed world assumption: what is not in the KB is assumed to be false
3 Refresh: Atoms and KBs An positive literal holds (“is true”) in a KB, if it appears in the KB. A negative literal ¬ Ａ  holds in a KB if Ａ  does not hold. A conjunction Ａ ∧ Ｂ ∧．．． ∧ Ｚ  holds in a KB, if all of its elements hold. ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ）   ? ¬ ｅｎｖｉｅｓ（Ｒｏｎ， Ｈａｒｒｙ）   ? ¬ ｅｎｖｉｅｓ（Ｒｏｎ， Ｈａｒｒｙ） ∧ ｌｉｋｅｓ（Ｈａｒｒｙ， Ｈｅｒｍｉｏｎｅ）  ｅｎｖｉｅｓ（Ｈａｒｒｙ， Ｒｏｎ） ∧ ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ） ∧ ｌｉｋｅｓ（Ｈａｒｒｙ， Ｅｌｖｉｓ）  likes envies likes
ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ） ⇒ ｌｉｋｅｓ（Ｈａｒｒｙ，Ｒｏｎ）  ｌｉｋｅｓ（Ｈａｒｒｙ， Ｒｏｎ） ⇒ ｈａｓＳｐｏｕｓｅ（Ｈａｒｒｙ，Ｈｅｒｍｉｏｎｅ）  ¬ ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｈａｒｒｙ） ⇒ ｅｎｖｉｅｓ（Ｈａｒｒｙ，Ｒｏｎ）  ¬ ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｈａｒｒｙ） ⇒ ｈａｓＳｐｏｕｓｅ（Ｈａｒｒｙ，Ｒｏｎ）  ｌｉｋｅｓ（Ｈｅｒｍ．， Ｒｏｎ）∧ ¬ ｅｎｖｉｅｓ（Ｈａｒｒｙ，Ｒｏｎ）⇒ ｆｆｅ（Ｈａｒｒｙ，Ｒｏｎ）  4 Refresh: Implications If   is a conjunction (called the body), and Ｈ  is an atom (called the head), then an implication   holds in a KB if   does not hold or Ｈ  holds. likes envies likes
ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ）  5 Refresh: Implications If   is a conjunction (called the body), and Ｈ  is an atom (called the head), then an implication   holds in a KB if   does not hold or Ｈ  holds. The body can also be empty. is a body‐less rule, i.e., equivalent to: ⇒ ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ）  likes envies likes
6 Def: Rules, Disjunctions, Clauses An implication (also: rule)  is equivalent to a disjunction  which we also write as a clause  . ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ） ⇒ ｌｉｋｅｓ（Ｈａｒｒｙ，Ｒｏｎ）  ¬ ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ） ∨ ｌｉｋｅｓ（Ｈａｒｒｙ，Ｒｏｎ）  ｛¬ ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ）， ｌｉｋｅｓ（Ｈａｒｒｙ，Ｒｏｎ） ｝  “at least one of  these has to hold” is equivalent to is equivalent to likes envies likes
Refresh:Universal quantification 7 hasSpouse hasSpouse hasSpouse A universally quantified formula holds in a KB, if all of its instantiations hold. ｈａｓＳｐｏｕｓｅ（ｘ， ｙ）  ｈａｓＳｐｏｕｓｅ（ｘ， ｙ） ⇒ ｈａｓＳｐｏｕｓｅ（ｙ， ｘ）  ｈａｓＳｐｏｕｓｅ（Ｅｌｖｉｓ， ｙ） ⇒ ｈａｓＳｐｏｕｓｅ（ｙ， Ｅｌｖｉｓ）  ｈａｓＳｐｏｕｓｅ（Ｈｅｒｍｉｏｎｅ， ｙ） ⇒ ｈａｓＳｐｏｕｓｅ（ｙ， Ｈｅｒｍｉｏｎｅ） 
ｈａｓＳｐｏｕｓｅ（ｘ， ｙ） ⇒ ｈａｓＳｐｏｕｓｅ（ｙ， ｘ）  8 hasSpouse hasSpouse In the following, we consider only instantiated rules. A universally quantified rule is a shorthand notation for all relevant instantiations, i.e., those with known entities. ｈａｓＳｐｏｕｓｅ（Ｅｌｖｉｓ， Ｐｒｉｓｃｉｌｌａ） ⇒ ｈａｓＳｐｏｕｓｅ（Ｐｒｉｓｃｉｌｌａ， Ｅｌｖｉｓ）  ｈａｓＳｐｏｕｓｅ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ） ⇒ ｈａｓＳｐｏｕｓｅ（Ｒｏｎ， Ｈｅｒｍｉｏｎｅ）  ... ｈａｓＳｐｏｕｓｅ（ｄｏｇ， ｃａｔ） ⇒ ｈａｓＳｐｏｕｓｅ（ｃａｔ， ｄｏｇ）  relevant instantiations irrelevant ｈａｓＳｐｏｕｓｅ（Ｅｌｖｉｓ， Ｅｌｖｉｓ） ⇒ ｈａｓＳｐｏｕｓｅ（Ｅｌｖｉｓ， Ｅｌｖｉｓ）  Refresh:Universal quantification hasSpouse
Def: Weighted Rule ｈａｓＳｐｏｕｓｅ（Ｅｌｖｉｓ，Ｐｒｉｓｃｉｌｌａ） ⇒ ｈａｓＳｐｏｕｓｅ（Ｐｒｉｓｃｉｌｌａ， Ｅｌｖｉｓ）［３．１４］  A weighted rule is a rule with an associated real-valued weight. 9 A weighted rule can also be seen as a weighted disjunction... ...or a weighted clause. ¬ ｈａｓＳｐｏｕｓｅ（Ｅｌｖｉｓ，Ｐｒｉｓｃｉｌｌａ） ∨ ｈａｓＳｐｏｕｓｅ（Ｐｒｉｓｃｉｌｌａ， Ｅｌｖｉｓ）［３．１４］  ｛¬ ｈａｓＳｐｏｕｓｅ（Ｅｌｖｉｓ，Ｐｒｉｓｃｉｌｌａ）， ｈａｓＳｐｏｕｓｅ（Ｐｒｉｓｃｉｌｌａ， Ｅｌｖｉｓ）｝ ［３．１４］ 
Def: Weight of a KB Given a set of atoms (= possible world, KB) and a set of instantiated rules with weights, the weight of the KB is the sum of the weights of all rules that hold in the KB. ｈａｓＳｐｏｕｓｅ（Ｅｌｖｉｓ，Ｐｒｉｓｃｉｌｌａ） ⇒ ｈａｓＳｐｏｕｓｅ（Ｐｒｉｓｃｉｌｌａ，Ｅｌｖｉｓ）［３］  ｈａｓＳｐｏｕｓｅ（ｃａｔ，ｄｏｇ） ⇒ ｈａｓＳｐｏｕｓｅ（ｄｏｇ，ｃａｔ）［２］  10 hasSpouse hasSpouse hasSpouse KB1 KB2
Def: Weight of a KB Given a set of atoms (= possible world, KB) and a set of instantiated rules with weights, the weight of the KB is the sum of the weights of all rules that hold in the KB. ｈａｓＳｐｏｕｓｅ（Ｅｌｖｉｓ，Ｐｒｉｓｃｉｌｌａ） ⇒ ｈａｓＳｐｏｕｓｅ（Ｐｒｉｓｃｉｌｌａ，Ｅｌｖｉｓ）［３］  ｈａｓＳｐｏｕｓｅ（ｃａｔ，ｄｏｇ） ⇒ ｈａｓＳｐｏｕｓｅ（ｄｏｇ，ｃａｔ）［２］  11 hasSpouse hasSpouse hasSpouse KB1 KB2 Weight: 2 Weight: 5
Def: Weighted MAX SAT ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ［１０］  ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ） ［４］  ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ∧ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ） ⇒ ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ） ［３］  12 Given a set of instantiated rules with weights, weighted MAX SAT is the problem of finding the KB with the highest weight. If there are several, find the one with the least number of atoms.
Def: Weighted MAX SAT ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ［１０］  13 ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ，ｓｏｒｃｅｒｅｓｓ）  ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）  ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ，Ｒｏｎ）  weight: 17 Best world: Given a set of instantiated rules with weights, weighted MAX SAT is the problem of finding the KB with the highest weight. If there are several, find the one with the least number of atoms. ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ） ［４］  ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ∧ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ） ⇒ ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ） ［３］ 
Task: Weighted MAX SAT Find the KB with the highest weight: ｉｓ（Ｈｅｒｍｉｏｎｅ，ｓｍａｒｔ）［１］  ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ，Ｒｏｎ） ⇒ ¬ ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ，Ｈａｒｒｙ）［１００］  ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ，Ｒｏｎ）［２０］  ｉｓ（Ｈａｒｒｙ，ｓｍａｒｔ）［１０］  ｉｓ（Ｈｅｒｍ．，ｓｍａｒｔ） ∧ ｉｓ（Ｈａｒｒｙ，ｓｍａｒｔ） ⇒ ｌｉｋｅｓ（Ｈｅｒｍ．，Ｈａｒｒｙ）［３］  14
Def: Exhaustive search Exhaustive search is an algorithm for the Weighted MAX SAT problem that tries out all possible worlds with the atoms that appear in the rules in order to find the possible world with the maximal weight. ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ［１０］  ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ，ｓｏｒｃｅｒｅｓｓ） ［４］  ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ∧ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ） ⇒ ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ） ［３］  15 ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）， ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ）， ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ）  Atoms:
Def: Exhaustive search ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ［１０］  ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ，ｓｏｒｃｅｒｅｓｓ） ［４］  16 Atoms: Possible worlds: ｛｝ : weight 3 ｛ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）｝ : weight 13, ｛ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）， ｔｙｐｅ （Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ）｝ : weight 14, etc. Exhaustive search is an algorithm for the Weighted MAX SAT problem that tries out all possible worlds with the atoms that appear in the rules in order to find the possible world with the maximal weight. ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ∧ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ） ⇒ ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ） ［３］  ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）， ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ）， ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ） 
Def: Exhaustive search ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ［１０］  ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ，ｓｏｒｃｅｒｅｓｓ） ［４］  17 Atoms: Exhaustive search is a correct and complete algorithm for the Weighted Max Sat problem. However, it has to analyze   possible worlds, where ｎ  is the number of atoms. Exhaustive search is an algorithm for the Weighted MAX SAT problem that tries out all possible worlds with the atoms that appear in the rules in order to find the possible world with the maximal weight. ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ∧ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ） ⇒ ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ） ［３］  ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）， ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ）， ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ） 
Intuition of unit propagation ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ［１０］  ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ，ｓｏｒｃｅｒｅｓｓ） ［４］  18 >example&unitcl Unit propagation repeatedly (1) adds the head of a body-less rule to the KB, (2) removes this atom from the bodies of the other rules, and (3) removes definitively satisfied rules. ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ∧ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ） ⇒ ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ） ［３］ 
ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ［１０］  ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ，ｓｏｒｃｅｒｅｓｓ） ［４］  19 KB: ｛ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）｝  Intuition of unit propagation >example&unitcl Unit propagation repeatedly (1) adds the head of a body-less rule to the KB, (2) removes this atom from the bodies of the other rules, and (3) removes definitively satisfied rules. ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ∧ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ） ⇒ ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ） ［３］ 
ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ［１０］  ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ，ｓｏｒｃｅｒｅｓｓ） ［４］  20 KB: ｛ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）｝  Intuition of unit propagation >example&unitcl Unit propagation repeatedly (1) adds the head of a body-less rule to the KB, (2) removes this atom from the bodies of the other rules, and (3) removes definitively satisfied rules. ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ∧ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ） ⇒ ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ） ［３］ 
ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ［１０］  ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ，ｓｏｒｃｅｒｅｓｓ） ［４］  21 KB: ｛ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）， ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ，ｓｏｒｃｅｒｅｓｓ）｝  Intuition of unit propagation >example&unitcl Unit propagation repeatedly (1) adds the head of a body-less rule to the KB, (2) removes this atom from the bodies of the other rules, and (3) removes definitively satisfied rules. ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ∧ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ） ⇒ ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ） ［３］ 
22 >unitcl Intuition of unit propagation ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ［１０］  ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ，ｓｏｒｃｅｒｅｓｓ） ［４］  KB: ｛ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）， ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ，ｓｏｒｃｅｒｅｓｓ）， ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ｝  Unit propagation repeatedly (1) adds the head of a body-less rule to the KB, (2) removes this atom from the bodies of the other rules, and (3) removes definitively satisfied rules. ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ） ∧ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ） ⇒ ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ） ［３］ 
Unit propagation for clauses Unit propagation repeatedly (1) adds the literal of a unit-clause to the KB, (2) removes the negation of the literal from the other clauses, and (3) removes all clauses that contain this literal. ｛ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）｝ ［１０］  ｛ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ）｝ ［４］  ｛ ¬ ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）， ¬ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ）， ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ）｝ ［３］  23
｛ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）｝ ［１０］  24 KB: ｛ｉｓ（Ｒｏｎ， ｉｍｍａｔｕｒｅ）｝  Unit propagation for clauses ｛ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ）｝ ［４］  ｛ ¬ ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）， ¬ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ）， ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ）｝ ［３］  Unit propagation repeatedly (1) adds the literal of a unit-clause to the KB, (2) removes the negation of the literal from the other clauses, and (3) removes all clauses that contain this literal.
｛ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）｝ ［１０］  25 KB: ｛ｉｓ（Ｒｏｎ， ｉｍｍａｔｕｒｅ）｝  Unit propagation for clauses ｛ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ）｝ ［４］  ｛ ¬ ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）， ¬ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ）， ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ）｝ ［３］  Unit propagation repeatedly (1) adds the literal of a unit-clause to the KB, (2) removes the negation of the literal from the other clauses, and (3) removes all clauses that contain this literal.
｛ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）｝ ［１０］  26 KB: ｛ｉｓ（Ｒｏｎ， ｉｍｍａｔｕｒｅ）｝  etc. Unit propagation for clauses ｛ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ）｝ ［４］  ｛ ¬ ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）， ¬ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ）， ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ）｝ ［３］  Unit propagation repeatedly (1) adds the literal of a unit-clause to the KB, (2) removes the negation of the literal from the other clauses, and (3) removes all clauses that contain this literal.
｛ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）｝ ［１０］  27 Def: Unit propagation for clauses Unit propagation is a correct (but not complete) algorithm for the Weighted Max Sat Problem if a unit clause is propagated only when its weight is higher than the sum of the weights of the rules where the literal appears with inverse polarity. Wikipedia/Unit propagation with a partial model ｛ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ）｝ ［４］  ｛ ¬ ｉｓ（Ｒｏｎ，ｉｍｍａｔｕｒｅ）， ¬ ｔｙｐｅ（Ｈｅｒｍｉｏｎｅ， ｓｏｒｃｅｒｅｓｓ）， ｌｉｋｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ）｝ ［３］  Unit propagation repeatedly (1) adds the literal of a unit-clause to the KB, (2) removes the negation of the literal from the other clauses, and (3) removes all clauses that contain this literal.
Solving Weighted MAX SAT 28 To always find the optimal solution, one has to do an exhaustive search. Since SAT is NP-complete, so is MAX SAT and Weighted MAX SAT. To find an approximate solution, possible strategies are: •  do an exhaustive search if there are few atoms •  try out several random KBs •  apply unit propagation wherever possible •  give preference to rules/unit clauses with higher weights •  add atoms to the KB that appear only positive,     add the negation of all atoms that appear only negative
Summary: Weighted MAX SAT A weighted formula is a logical formula with a real‐valued weight. ｄｕｍｂ（Ｒｏｎ）  [10],      ｄｕｍｂ（ｘ） ⇒ ｌｏｖｅｓ（Ｈｅｒｍｉｏｎｅ， ｘ）  [3.2] equivalently written as a clause: instantiated: ｛¬ ｄｕｍｂ（ｘ）， ｌｏｖｅｓ（Ｈｅｒｍｉｏｎｅ， ｘ）｝  [3.2] Given a set of instantiated clauses with weights, weighted MAX SAT is the problem of finding the KB with the highest weight. If there are several, find the one with the least number of atoms. ｛¬ ｄｕｍｂ（Ｒｏｎ）， ｌｏｖｅｓ（Ｈｅｒｍｉｏｎｅ， Ｒｏｎ）｝  [3.2] Given weighted clauses, the weight of a KB (= set of facts) is the sum of the weights of the clauses that are satisfied in the KB. is dumb weight: 10 is dumb weight: 13.2 loves ->Ie-by-reasoning ->Markov-logic