= Translation of RSF-Files into DIMACS Format =

== Translation of ''depends'' Constraints ==
Each variable can have multiple depends statements, specifying when the variable can be configured. The variable must remain unconfigured (in case of a Boolean or Tristate variable, it must be set to ''n''), if none of the depends statements is fulfilled.
Conditions will be translated as follows:
1. One Condition:
 * In RSF:
{{{
depends Variable Condition
}}}
 * In Boolean formula:
{{{
Not(Condition) implies Not(Variable)
}}}
 * In DIMACS
{{{
Condition or Not(Variable)
}}}
1. Multiple Conditions
 * In RSF:
{{{
depends Variable Condition1
depends Variable Condition2
}}}
 * In Boolean formula:
{{{
Not(Condition1) and Not(Condition2) implies Not(Variable)
}}}
 * In DIMACS
{{{
Condition1 or Condition2 or Not(Variable)
}}}

== Translation of ''!ItemSelects'' Constraints ==
The KConfig specification defines select statements as follows:
> reverse dependencies: "select" <symbol> !["if" <expr>]
>  While normal dependencies reduce the upper limit of a symbol (see
>  below), reverse dependencies can be used to force a lower limit of
>  another symbol. The value of the current menu symbol is used as the
>  minimal value <symbol> can be set to. If <symbol> is selected multiple
>  times, the limit is set to the largest selection.
>  Reverse dependencies can only be used with boolean or tristate
>  symbols.