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)
     

2. 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)