| - Up - | Next >> |
Each solver object has several attributes. @counter allows us to give each variable occurring in the description a distinct integer to encode it. @var2int is a dictionary mapping each atom naming a variable to the corresponding integer encoding it. @int2node is a dictionary mapping an integer encoding a variable
to the record representing
. @vars is a set variable representing the set of all variables occurring in the description. @labs represents the subset of these variables that are explicitly labeled in the description. @choices is a dictionary that allows us to map a pair of variables
to the corresponding
representing the relationship between them. Since
is the inverse of
, we only need to represent one of them: we only represent
when
are respectively encoded by integers I,J and I is larger than J. For simplicity, we assume that there are fewer than 1000 variables in the description and use index I*1000+J to retrieve
from @choices.
attr counter:0 var2int int2node vars labs choices| - Up - | Next >> |