Logic - Maple Programming Help

Online Help

All Products    Maple    MapleSim


Home : Support : Online Help : Programming : Logic : Boolean : Logic Package : Logic/Satisfy

Logic

  

Satisfy

  

find a valuation satisfying an expression

  

Satisfiable

  

determine if expression can be satisfied

 

Calling Sequence

Parameters

Options

Description

Definitions

Examples

References

Compatibility

Calling Sequence

Satisfiable(expr, opts)

Satisfy(expr, alpha, opts)

Parameters

expr

-

Boolean expression

alpha

-

(optional) list or set of names

opts

-

(optional) zero or more options as specified below

Options

• 

method="maplesat" or "legacy"

  

The method option specifies the method which should be used for determining the solvability of the Boolean expression.  The default behavior uses the MapleSAT SAT solver but the Satisfy command also supports a method which uses a legacy Maple implementation.

• 

solveroptions=list(equation)

  

By specifying a list of equations as the value of option solveroptions, it is possible to fine-tune the configuration of the MapleSAT engine. Each such equation must be of the form optionname = value. Available options are described in the following table. Each such option corresponds in name, type, and default value to a configuration option offered by MapleSAT. For more information, consult the MapleSAT and MiniSat documentation.

Name

Type

Default Value

Description

random_var_freq

numeric

0

The frequency with which the decision heuristic tries to choose a random variable

random_seed

numeric

91648253

Used by the random variable selection

ccmin_mode

nonnegint

2

Controls conflict clause minimization (0=none, 1=basic, 2=deep)

phase_saving

nonnegint

2

Controls the level of phase saving (0=none, 1=limited, 2=full)

rnd_init_act

truefalse

false

Randomize the initial activity

luby_restart

truefalse

true

Use the Luby restart sequence

restart_first

posint

100

The base restart interval

restart_inc

numeric

2

Restart interval increase factor

garbage_frac

numeric

0.20

The fraction of wasted memory allowed before a garbage collection is triggered

step_size

numeric

0.4

Initially use this step-size value when calculating the exponentially weighted moving averages

step_size_dec

numeric

1e-06

Decrement the step-size by this value after each conflict

min_step_size

numeric

0.06

Stop decrementing the step-size once it reaches this value

Description

• 

The Satisfiable command returns true if the Boolean expression expr is satisfiable, that is, if a satisfying assignment exists. Otherwise false is returned.

• 

The Satisfy command returns a set of equations representing a satisfying assignment to expr. If expr is not satisfiable, then NULL is returned.

• 

The Satisfy command does not specify which satisfying assignment it returns. Two satisfiable formulae which are logically equivalent may produce different satisfying assignments.

• 

If the optional second parameter to Satisfy is present, the valuation includes all variable names in alpha.

Definitions

• 

A satisfying assignment is an assignment to the variables of a given Boolean expression that satisfies the expression.

• 

The problem of determining whether a Boolean formula has a satisfying assignment is known as the Boolean satisfiability problem or SAT. This is a decision problem which is known to be NP-complete, and consequently no polynomial-time algorithm is presently known.

Examples

Test a simple Boolean expression for satisfiability.

withLogic:

Satisfiablea&orb

true

(1)

Find a satisfying assignment.

Satisfya&orb

a=true,b=false

(2)

Find a satisfying assignment while specifying the variable set to be {a,b,c}.

Satisfya&orb,a,b,c

a=true,b=false,c=false

(3)

Satisfiablea&and&nota

false

(4)

The following returns NULL since it is unsatisfiable.

Satisfya&and&nota

Test a Boolean expression for satisfiability, while providing customized values for the step_size and rnd_init_act MapleSAT parameters.

Satisfya&impliesb&xor&notc,solveroptions=step_size=0.75,rnd_init_act=true

a=false,b=false,c=true

(5)

References

  

Liang, J. H.; Ganesh, V.; Poupart, P.; and Czarnecki, K. "Learning rate based branching heuristic for SAT solvers." International Conference on Theory and Applications of Satisfiability Testing. Springer International Publishing, 2016.

  

Eén, N. and Sörensson, N. "An extensible SAT-solver." International Conference on Theory and Applications of Satisfiability Testing. Springer, Berlin, Heidelberg, 2003.

Compatibility

• 

The Logic[Satisfiable] command was introduced in Maple 2016.

• 

For more information on Maple 2016 changes, see Updates in Maple 2016.

• 

The Logic[Satisfy] and Logic[Satisfiable] commands were updated in Maple 2018.

• 

The method and solveroptions options were introduced in Maple 2018.

• 

For more information on Maple 2018 changes, see Updates in Maple 2018.

See Also

copyright

Logic

Logic/Equivalent

Logic/Tautology