Safe HaskellSafe

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"]]