Changes between Version 13 and Version 14 of Specification/RSF2DIMACS

Timestamp:

Sep 25, 2014, 12:02:14 PM (11 years ago)

Author:

elshar

Comment:

--

Specification/RSF2DIMACS

@@ -69 +69 @@
 >then you may define the same choice (ie. with the same entries) in another place.
 === Translation of Boolean Choices ===
-If a boolean choice is selected, exactly one of the related !ChoiceItems has to be selected. For each !ChoiceItems the individual conditions has to be considered.
+If a boolean choice is selected, exactly one of the related !ChoiceItems has to be selected. For each !ChoiceItems the individual conditions has to be considered. A Choice with n !ChoiceItems {{{Item1}}} - {{{ItemN}}} must be translated as follows (conditions are not considered here):
+* In RSF:
+{{{
+Choice CHOICE
+ChoiceItem Item1 CHOICE
+...
+ChoiceItem ItemN CHOICE
+}}}
+* In Boolean formula:
+{{{
+CHOICE implies (Item1 or Item2 or ... or ItemN)
+Not(CHOICE) implies Not(Item1)
+Not(CHOICE) implies Not(Item2)
+...
+Not(CHOICE) implies Not(ItemN)
+Item1 xor Item2
+Item1 xor Item3
+...
+Item1 xor ItemN
+Item2 xor Item3
+...
+ItemN-1 xor ItemN
+}}}
+* In DIMACS:
+{{{
+Not(CHOICE) or Item1 or Item2 or ... or ItemN
+CHOICE or Not(Item1)
+CHOICE or Not(Item2)
+...
+CHOICE or Not(ItemN)
+Not(Item1) or Not(Item2)
+Not(Item1) or Not(Item3)
+...
+Not(Item1) or Not(ItemN)
+Not(Item2) or Not(Item3)
+...
+Not(ItemN-1) or Not(ItemN)
+}}}
+
 === Translation of Tristate Choices ===
 A Tristate Choice can be selected as permanently selected ('y') or as a module ('m').
@@ -112 +150 @@
  * In Boolean formula:
 {{{
-Not(TRISTATE_VAR) and Not(TRISTATE_VAR_MODULE) implies Not(VARIABLE )
-}}}
- * In DIMACS:
-{{{
-TRISTATE_VAR or TRISTATE_VAR_MODULE or Not(VARIABLE )
+Not(TRISTATE_VAR) and Not(TRISTATE_VAR_MODULE) implies Not(VARIABLE)
+}}}
+ * In DIMACS:
+{{{
+TRISTATE_VAR or TRISTATE_VAR_MODULE or Not(VARIABLE)
 }}}
 1. Tristate variable depends of Condition