Logic - Maple Programming Help

Online Help

All Products    Maple    MapleSim


Home : Support : Online Help : System : Information : Updates : Maple 2016 : updates/Maple2016/Logic

Logic

 

Boolean Satisfiability

Truth Tables

Boolean Satisfiability

Given a Boolean formula ϕx__1,,x__n, the Boolean satisfiability problem asks whether there exists some choice of true and false values for x__1,x__n such that ϕx__1,,x__n=true.  This choice of variables is called a satisfying assignment, and the formula is said to be satisfiable. The satisfiability problem is known to be computationally difficult and was one of the first problems shown to be NP-complete.

 

Maple 2016 introduces new efficient heuristics for determining satisfiability and testing equivalence of Boolean expressions.

withLogic:

Satisfiable x and y xor not z

true

(1.1)

Satisfyx and y xor not z

x=false,y=false,z=false

(1.2)

Satisfiablex and y and not x

false

(1.3)

formula  Randoms,t,u,v,w,x,y,z,clauses=20,literals=3,form=CNF

stysuwsw¬xsyztwyt¬u¬wt¬v¬wuwzuy¬zvy¬uw¬t¬zx¬t¬wx¬t¬zz¬t¬v¬s¬t¬w¬s¬u¬w¬s¬v¬y¬t¬u¬z¬t¬x¬z¬u¬w¬y

(1.4)

Satisfyformula

s=false,t=false,u=true,v=false,w=false,x=false,y=true,z=false

(1.5)

Truth Tables

The Logic:-TruthTable command now returns a DataFrame with the truth assignments for a given formula.

TruthTablex and y xor not z

xyzvalue1falsefalsefalsetrue2falsefalsetruefalse3falsetruefalsetrue4falsetruetruefalse5truefalsefalsetrue6truefalsetruefalse7truetruefalsefalse8truetruetruetrue

(2.1)