Changes between Version 15 and Version 16 of Specification/RSF2DIMACS

Timestamp:

Sep 25, 2014, 2:30:15 PM (10 years ago)

Author:

elshar

Comment:

--

Specification/RSF2DIMACS

@@ -1 +1 @@
 = Translation of RSF-Files into DIMACS Format =
+This section specifies the translation of RSF files into DIMACS files.
 [[PageOutline(2-5, Table of Contents, pullout)]]
 
@@ -41 +42 @@
 {{{
 Not(VARIABLE=n) OR Not(VARIABLE=value1)
-Not(VARIABLE=n) OR (VARIABLE=value2)
-...
-Not(VARIABLE=n) OR (VARIABLE=valueN)
-Not(VARIABLE=value1) OR (VARIABLE=value2)
-...
-Not(VARIABLE=value1) OR (VARIABLE=valueN)
+Not(VARIABLE=n) OR Not(VARIABLE=value2)
+...
+Not(VARIABLE=n) OR Not(VARIABLE=valueN)
+Not(VARIABLE=value1) OR Not(VARIABLE=value2)
+...
+Not(VARIABLE=value1) OR Not(VARIABLE=valueN)
 ...
 VARIABLE=n OR VARIABLE=value1 OR ... OR VARIABLE=valueN
@@ -116 +117 @@
 A Tristate Choice can be selected as permanently selected ('y') or as a module ('m').
 * If the Choice is permanently selected ('y'), exactly one of its !ChoiceItems must also be permanently selected ('y').
-* If the Choice is selected as a module ('m'), an arbitrary number (0 - n) of !ChoiceItems can also be selected as modules ('m').
+* If the Choice is selected as a module ('m'), an arbitrary number (0 - n) of !ChoiceItems can also be selected as modules ('m'). The permanently selection of !ChoiceItems ('y') is not allowed. [[BR]] 
+The translation of Tristate Choices includes the translation of Boolean Choices (for the 'y' part). Additional constraints are needed to model the constraints for the modules:
+* In RSF:
+{{{
+Choice CHOICE
+ChoiceItem Item1 CHOICE
+...
+ChoiceItem ItemN CHOICE
+}}}
+* In Boolean formula (only the module part):
+{{{
+Not(CHOICE_MODULE) implies Not(Item1_MODULE)
+Not(CHOICE_MODULE) implies Not(Item2_MODULE)
+...
+Not(CHOICE_MODULE) implies Not(ItemN_MODULE)
+CHOICE implies Not(Item1_MODULE)
+CHOICE implies Not(Item2_MODULE)
+...
+CHOICE implies Not(ItemN_MODULE)
+CHOICE_MODULE implies Not(Item1)
+CHOICE_MODULE implies Not(Item2)
+...
+CHOICE_MODULE implies Not(ItemN)
+}}}
+* In RSF (only the module part):
+{{{
+CHOICE_MODULE or Not(Item1_MODULE)
+CHOICE_MODULE or Not(Item2_MODULE)
+...
+CHOICE_MODULE or Not(ItemN_MODULE)
+Not(CHOICE) or Not(Item1_MODULE)
+Not(CHOICE) or Not(Item2_MODULE)
+...
+Not(CHOICE) or Not(ItemN_MODULE)
+Not(CHOICE_MODULE) or Not(Item1)
+Not(CHOICE_MODULE) or Not(Item2)
+...
+Not(CHOICE_MODULE) or Not(ItemN)
+}}}
 
 == Translation of ''depends'' Constraints ==