Problematic data structure in functional language

I am trying to build an efficient data structure for representing
boolean expressions in Erlang. I am having trouble producing a good
data structure in a functional context, although there are very fast
data structures for imperative languages like C. The data structure is
to be used for a functional SAT solver.

A boolean expression (always in conjunctive normal form) can be
described as a set of variables, such as {p,q,r...} where each
variable in the set is mapped to one of three values true|false|
indetermined yielding something like {{p->ind},{q->true},{r-
>ind},...}.

The expression is described as a set of sets of literals, where a
literal is a variable with a possible negation (~). So we have
something like {{~p,q},{~q,r}} which describes a formula that would
usually be written (~p v q)&(~q v r). Each of the inner sets has the
property that if one of its literals evaluates to true then the whole
set can be removed from the outer set.

To being with we can represent the expression as a list of lists where
the variable-name, negation and value are all stored in one tuple.
[[{name,negation,value}]]

Now if we assign a value to a variable we then need to traverse every
sublist ensuring a consistent assignment is made for every occurrence
of the varia ble in the expression. However, as a reward for this
effort we can easily check each sublist to see whether one of its
members evaluates to true (meaning the sublist can be removed).

Alternately we could represent the expression as a list of lists where
just the variable name and negation are recorded {name,negation} and
have the assignment values stored as a separate mapping. This makes
assignments fast and safer, but we still need to traverse every
sublist to see that it does not now contain a literal evaluating to
true. Is there a better way, I suspect that I am thinking about it in
the wrong way. Thanks.

Francis wrote:
> I am trying to build an efficient data structure for representing
> boolean expressions in Erlang. I am having trouble producing a good
> data structure in a functional context, although there are very fast
> data structures for imperative languages like C. The data structure is
> to be used for a functional SAT solver.

snip

> Alternately we could represent the expression as a list of lists where
> just the variable name and negation are recorded {name,negation} and
> have the assignment values stored as a separate mapping. This makes
> assignments fast and safer, but we still need to traverse every
> sublist to see that it does not now contain a literal evaluating to
> true. Is there a better way, I suspect that I am thinking about it in
> the wrong way. Thanks.

I haven't implemented this, but:

Construct a set of pairs of indexes, one pair for each variable - One
for the variable and one for its negation.

Pre-process your expression, assigning each sub-expression a unique id
and store those ids in each index that corresponds to a variable (or
negation) in the sub-expression.

You now have a list of ids and a set of indexes.  For each trial
assignment pass over the list removing all ids in the appropriate index,
no re-examination of the sub-expressions required.

Regards,

Geoff.