|
Logic[Satisfy] - find a valuation satisfying an expression
|
|
Calling Sequence
|
|
Satisfy(expr, alpha)
|
|
|
Parameters
|
|
|
expr
|
-
|
Boolean expression
|
|
alpha
|
-
|
(optional) list or set of names
|
|
|
|
|
|
Description
|
|
|
•
|
The Satisfy command returns a set of equations representing an assignment to the variables of the given Boolean expression expr that satisfy the expression expr. If expr is not satisfiable, then NULL is returned.
|
|
•
|
If the optional second parameter is present, the valuation includes all variable names in alpha.
|
|
|
|
Examples
|
|
|
>
|
|
|
>
|
|
|
| (1) |
|
>
|
|
|
| (2) |
|
>
|
|
|
>
|
|
|
| (3) |
|
|
