Working with the Maple Logic package
Written: Nov 25, 2008
Since version 9.5, Maple has included a "Logic" package. Nevertheless, when I attempted to find some documentation on the package, I couldn't find anything beyond the help files of the Maple application itself, which don't go into much depth. My specific need was to convert from Maple's version of logical expressions to the DIMACS format (here is the best description of that I could find).
First consider a typical boolean expression using the Logic package:
> with(Logic):
> e := (a &iff b) &and (b &xor c);
e := (a &iff b) &and (b &xor c)
There are a few interesting procedures in the package, such as Satisfy, which will test whether a given expression can be satisfied, and return satisfying assignments if it can be, for example:
> Satisfy(a &and ¬(a));(nothing returned)
> Satisfy(e);
{c = true, a = false, b = false}
But my tests have convinced me that the SAT solver in the Logic package is a slow, crash-happy memory hog, which is most of the reason why I was motivated to export these expressions to DIMACS format in the first place.
To convert an expression to CNF (conjunctive normal form), use the Normalize procedure:
> enormal := Normalize(e, form=CNF);
(((a &or ¬(b)) &and (b &or ¬(a))) &and (b &or c)) &and
(¬(b) &or ¬(c))
Another interesting conversion is to “modulo 2 canonical form“ (Warning: modulo 2 canonical forms seem to take a very long time to compute):
> Canonicalize(e, form=MOD2);
c a + c + b a + b c
This allows us to use the indets procedure to get a list of all the variables in the expression:
> indets(Canonicalize(e, form=MOD2));
{a, b, c}
(Note: applying indets to a Boolean expression by itself does something completely bizarre.)
Quite to my annoyance, Maple does not define such things as e[1] for Boolean expressions e, which makes it quite a pain to pick them apart, as we will need to. However, converting them to lists does help a bit:
> el := convert(enormal, list);
el := [a &or ¬(b), b &or ¬(a), b &or c, ¬(b) &or ¬(c)]
> nops(elist);
4
Note that you will want to make sure to convert your expressions to CNF (or some other normal form) before you try to convert them to lists! In doing the expression to list conversion, Maple will break along all of the top-level operations, e.g.,
> e;
(a &iff b) &and (b &xor c)
> convert(e, list);
[a &iff b, b &xor c]
Assuming we are dealing with something in CNF though, we know that the result of convert(enormal, list) will be a list of disjunctions, and that we can break up each of these disjunctions by converting them to lists:
> el1 := convert(el[1], list);
el1 := [a, ¬(b)]
Something a bit funny happens when we convert these to lists though:
> el11 := convert(el1[1], list);
el11 := [a]
> el12 := convert(el1[2], list);
el12 := [b]
(And if you are using variables with subscripts, something even worse happens, but we won't get into that particular bug.) This is therefore a good place to use the MOD2 conversion trick:
> el1m1 := Canonicalize(el1[1], form=MOD2);
el1m2 := a
> el1m2 := Canonicalize(el1[2], form=MOD2);
el1m2 := b + 1
Now to tell the difference between a and ¬(a), we can check whether the MOD2 form is equal to the single indeterminant that it contains:
> evalb(el1m1 = indets(el1m1)[1]);
true
> evalb(el1m2 = indets(el1m2)[1]);
false
Having explained how we can pick apart one of Maple's boolean expressions, it remains only to explain the DIMACS CNF format. Each variable in our expression is assigned a number, starting with 1 (so for us, a, b, and c will recieve the numbers 1, 2, and 3, respectively). A DIMACS formatted file may start with any number of comment lines, which are prefaced with c's. It then contains the a line "p cnf num_vars num_clauses", where num_vars is the number of variables and num_clauses is the number of clauses. Following this, each line contains a list of variable numbers (and their negatives), which represent those variables (and their negations) that are contained in that disjunction, followed by the number 0. For example, the DIMACS format for our example e would be:
c Comments... c In Maple, e := (a &iff b) &and (b &xor c); p cnf 3 4 1 -2 0 2 -1 0 2 3 0 -2 -3 0
The Maple procedure bool2dimacs, below, will do this conversion automatically, using the decomposition we have discussed above:
bool2dimacs := proc(e)
local Vars,
varlookup,
var,
disj,
disjvar,
Disjvars,
Disjset;
# First find a list of all the variables in use.
# varlookup(var) will give the variable's number
# To get the list of variables, we could simply use
# Vars := [op(indets(Canonicalize(e, form=MOD2)))];
# but the performance is terrible, so instead
# we build a set of all the disjunctions, and work through them one by one
Vars := {};
Disjset := {op(convert(Normalize(e, form=CNF), list))};
for disj in Disjset do
Vars := Vars union indets(Canonicalize(disj, form=MOD2));
od;
Vars := [op(Vars)];
varlookup := proc(v)
local i;
for i from 1 to nops(Vars) do
if Vars[i] = v then
return(i);
fi;
od;
error("invalid variable name");
end:
printf("p cnf %a %a\n", nops(Vars), nops(Disjset));
for disj in Disjset do
Disjvars := {op(convert(disj, list))};
for disjvar in Disjvars do
# These can either be of the form "a" or "¬(a)".
var := Canonicalize(disjvar, form=MOD2);
# The following line will test for whether the variable occurs by itself
# (without a not).
if var = indets(var)[1] then
printf("%a ", varlookup(var));
else
printf("-%a ", varlookup(simplify(var - 1)));
fi;
od;
printf("0 \n");
od;
end:
Running this on our expression e generates the output expected:
> e := (a &iff b) &and (b &xor c);
e := (a &iff b) &and (b &xor c)
> bool2dimacs(e);
p cnf 3 4
1 -2 0
2 -1 0
-2 -3 0
2 3 0
From here, you can use a more sophisticated SAT solver, like MiniSat to test for satisfaction, for example:
$ ./minisat This is MiniSat 2.0 beta Reading from standard input... Use '-h' or '--help' for help. p cnf 3 4 1 -2 0 2 -1 0 -2 -3 0 2 3 0 ============================[ Problem Statistics ]============================= | | | Number of variables: 3 | | Number of clauses: 4 | | Parsing time: 0.00 s | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 0 | 3 4 8 | 1 0 nan | 0.000 % | =============================================================================== Verified 4 original clauses. restarts : 1 conflicts : 0 (0 /sec) decisions : 2 (0.00 % random) (2571 /sec) propagations : 3 (3856 /sec) conflict literals : 0 ( nan % deleted) CPU time : 0.000778 s SATISFIABLE