In [1]:

    

1+1


    

    
Out[1]:





2

In [2]:

    

{{1,2,3}}


    

    
Out[2]:





{{1,2,3}}

In [3]:

    

f[1,2,g[3],4,5] //. f[l1__,l2__,g[x_],r__] :> h[r,x,l2,l1]


    

    
Out[3]:





h[4,5,3,2,1]

In [4]:

    

f[g[a1,b,c1],h[a2,b,c2]] //. f[g[___,x_,___],h[___,y_,___]] /; x===y :> {x}


    

    
Out[4]:





{b}

In [5]:

    

(* the bubble sort rule *)
sortRule := {x___,y_,z_,k___}/;(y>z) :> {x,z,y,k}


    

In [6]:

    

{64, 44, 71, 48, 96, 47, 59, 71, 73, 51, 67, 50, 26, 49, 49}//.sortRule


    

    
Out[6]:





{26,44,47,48,49,49,50,51,59,64,67,71,71,73,96}

In [7]:

    

res1 = SatSolve[a&&b && (!a || c||d) && !d];
res1


    

    
Out[7]:





Sat[{a->True,b->True,c->True,d->False}]

In [8]:

    

(* extract the true atoms using a comprehension *)
{x :: Sat[{m___}]<-res1,(x_->True)<<-m}


    

    
Out[8]:





{a,b,c}

In [9]:

    

SatSolve[a&&b&&(!a||!b)]


    

    
Out[9]:





Unsat[]

In [10]:

    

Doc[SatSolve]


    

    





SatSolve
`SatSolve[form]` calls a SAT solver on the formula given as parameter. The formula is reduced to CNF automatically before calling Minisat.
If Minisat is not installed, this does not reduce.
Returns either `Sat[{m___}]` where `m` is the model, as a list of bindings `Atom -> True` or `Atom -> False`, or Unsat[].
example
The following call will return `Unsat[]`.
`SatSolve[(A || B)&& (!A || !B) && !B]`
example
The following call will return `Sat[A -> False,B->True]`, containing a model for each atom appearing in the formulas.
`SatSolve[And[A || B,!A]]`
example
Find a model of `a&&b` and extract the value of `a` in the model using `Let`:
`Let[{___,a->r_,___}<<-SatSolve[a&&b],r]`
also check that the model reduces the formula to `True`:
`Let[Sat[m_]<-SatSolve[a&&b], a&&b//. m]`
convert the model into (possibly negated) atoms:
Let[Sat[m_]<-SatSolve[a&&b,!c], m//.{(x_->False):>!x, (x_->True):>x}]
(yield `{a,b,!c}`)
requires
`minisat` must be on the $PATH

In [11]:

    

Let[Sat[m_]<-SatSolve[a&&b], a&&b//. m]


    

    
Out[11]:





True

In [ ]: