For example, if we have a logic function F = (x1 or x2) and (not x2) then we can verify a solution [x1=true, x2=false] of equation F = true this way:
[> F:=(x1 or x2) and (not x2):
subs({x1=true,x2=false},F);
true
Maple Logic package has a nice function Satisfy, which can find a solution, but function F (now it's named as G) has to be written using symbol & (before and, or, not):
[> G:=(x1 &or x2) &and (¬ x2):
A:=Logic[Satisfy](G);
A := {x1 = true, x2 = false}
But I don't know an easy way how to verify a solution (I mean not in this specific case, but in general, functions may have hundreds of variables). My attempt was to use substitution and then use evalb, but it didn't work:
[> G1:=subs(A,G);
evalb(G1);
G1:= (true &or false) &and ¬(false)
(true &or false) &and ¬(false)
But for function F the substitution worked (even without evalb):
[> F1:=subs(A,F);
F1:=true
Also I couldn't find an easy way to remove ampersand symbol & from an expression (in order to construct function F from function G).
G := (x1 &or x2) &and (¬ x2):
cand := {x1=true, x2=false}:
Given the logical expression assigned to G
in form of used by the Logic
package (ie. operators with names prefixed by &
), then the candidate solution assigned to cand
can be tested as follows:
BG := Logic:-Export(G, form=boolean);
BG := (x1 or x2) and not x2
eval(BG, cand);
true
Combining those two steps,
eval(Logic:-Export(G, form=boolean), cand);
true