Data.Algorithm.SatSolver.Fml.Some

Contents

Synopsis

# Testing Var Int

fml1 :: Fml Int Source #

Satisfiable empty CNF formula.

>>> fml1
[]


fml2 :: Fml Int Source #

Satisfiable CNF formula. $(x_1 \vee \neg x_2 \vee \neg x_3 \vee x_4)$

>>> fml2
[[+1,-2,-3,+4]]


fml3 :: Fml Int Source #

Satisfiable CNF formula. $(x_1 \vee \neg x_3) \wedge (x_1 \vee x_4 \vee \neg x_5) \wedge (x_2 \vee x_3 \vee x_4) \wedge (\neg x_1 \vee \neg x_3 \vee \neg x_5) \wedge (x_4 \vee x_5) \wedge (\neg x_3 \vee \neg x_4 \vee x_5) \wedge (x_2)$

>>> fml3
[[+1,-3],[+1,+4,-5],[+2,+3,+4],[-1,-3,-5],[+4,+5],[-3,-4,+5],[+2]]


fml4 :: Fml Int Source #

Satisfiable CNF formula. $(x_1 \vee \neg x_1 \vee \neg x_3) \wedge (x_1 \vee x_4 \vee \neg x_5 \vee x_6 \vee \neg x_7) \wedge (x_2 \vee x_3 \vee x_4 \vee x_8 \vee x_9)$

>>> fml4
[[+1,-1,-3],[+1,+4,-5,+6,-7],[+2,+3,+4,+8,+9]]


fml5 :: Fml Int Source #

Satisfiable CNF formula. $(x_1 \vee \neg x_2) \wedge (x_1 \vee x_4) \wedge (x_8 \vee x_9) \wedge (\neg x_1 \vee \neg x_8) \wedge (x_4 \vee x_5)$

>>> fml5
[[+1,-2],[+1,+4],[+8,+9],[-1,-8],[+4,+5]]


fml6 :: Fml Int Source #

Unsatisfiable CNF formula. $(x_1 \vee x_2) \wedge (\neg x_1 \vee x_2) \wedge (x_1 \vee \neg x_2) \wedge (\neg x_1 \vee \neg x_2)$

>>> fml6
[[+1,+2],[-1,+2],[+1,-2],[-1,-2]]


fml7 :: Fml Int Source #

Satisfiable CNF formula $(x_1) \wedge (\neg x_2 ) \wedge (x_3) \wedge (x_4) \wedge (\neg x_5) \wedge (x_6) \wedge (\neg x_7) \wedge (\neg x_8) \wedge (\neg x_9)$

>>> fml7
[[+1],[-2],[+3],[+4],[-5],[+6],[-7],[-8],[-9]]


fml8 :: Fml Int Source #

Satisfiable CNF formula $(x_1 \vee x_2) \wedge (x_2 \vee \neg x_3) \wedge (\neg x_3 \vee x_4) \wedge (x_4 \vee \neg x_5) \wedge (\neg x_5 \vee x_6) \wedge (x_6 \vee \neg x_7) \wedge (\neg x_7 \vee x_8) \wedge (x_8 \vee \neg x_9) \wedge (\neg x_9 \vee \neg x_1)$

>>> fml8
[[+1,+2],[+2,-3],[-3,+4],[+4,-5],[-5,+6],[+6,-7],[-7,+8],[+8,-9],[-1,-9]]


fml9 :: Fml Int Source #

Satisfiable CNF formula $(x_1) \wedge (\neg x_2) \wedge (x_3) \wedge (\neg x_1 \vee x_2 \vee \neg x_4) \wedge (\neg x_3 \vee \neg x_5) \wedge (x_4 \vee x_5 \vee \neg x_6) \wedge (x_6 \vee x_7) \wedge (\neg x_7 \vee x_8) \wedge (\neg x_8 \vee x_9)$

>>> fml9
[[+1],[-2],[+3],[-1,+2,-4],[-3,-5],[+4,+5,-6],[+6,+7],[-7,+8],[-8,+9]]


fml10 :: Fml Int Source #

Unsatisfiable CNF formula $(x_1) \wedge (x_2) \wedge (x_3) \wedge (\neg x_1 \vee x_4) \wedge (\neg x_2 \vee x_5) \wedge (\neg x_3 \vee x_6) \wedge (\neg x_4 \vee x_7) \wedge (\neg x_5 \vee x_8) \wedge (\neg x_7 \vee \neg x_8)$

>>> fml10
[[+1],[+2],[+3],[-1,+4],[-2,+5],[-3,+6],[-4,+7],[-5,+8],[-7,-8]]


fml11 :: Fml Int Source #

Satisfiable CNF formula $(x_1 \vee x_2) \wedge (\neg x_2 \vee \neg x_3) \wedge (x_3 \vee x_4) \wedge (\neg x_4 \vee \neg x_5) \wedge (x_5 \vee x_6) \wedge (\neg x_6 \vee \neg x_7) \wedge (x_7 \vee x_8) \wedge (\neg x_8 \vee \neg x_9) \wedge (x_9 \vee \neg x_1)$

>>> fml11
[[+1,+2],[-2,-3],[+3,+4],[-4,-5],[+5,+6],[-6,-7],[+7,+8],[-8,-9],[-1,+9]]


# Teting Var String

fmlEvt1 :: Fml String Source #

Satisfiable CNF formula $(\texttt{evt A} \vee \texttt{evt B}) \wedge (\neg \texttt{evt A} \vee \texttt{evt C}) \wedge (\texttt{evt A} \vee \neg \texttt{evt B} \neg \texttt{evt C})$

>>> fmlEvt2
[[+"Evt A"],[-"Evt A",+"Evt B"],[-"Evt B",-"Evt C"],[-"Evt A",-"Evt B",+"Evt C"]]


fmlEvt2 :: Fml String Source #

Unsatisfiable CNF formula $(\texttt{evt A}) \wedge (\neg \texttt{evt A} \vee \texttt{evt B}) \wedge (\neg \texttt{evt B} \vee \neg \texttt{evt C}) \wedge (\texttt{evt A} \vee \neg \texttt{evt B} \vee \texttt{evt C})$

>>> fmlEvt2
[[+"Evt A"],[-"Evt A",+"Evt B"],[-"Evt B",-"Evt C"],[-"Evt A",-"Evt B",+"Evt C"]]