Copyright	(c) Artem Mavrin 2021
License	BSD3
Maintainer	artemvmavrin@gmail.com
Stability	experimental
Portability	POSIX
Safe Haskell	Safe
Language	Haskell2010

AutoProof.Internal.Classical.SAT.Algorithms.DPLL

Description

DPLL satisfiability algorithm.

Synopsis

satDPLL :: Ord a => Formula a -> Bool
satAssignmentDPLL :: Ord a => Formula a -> Maybe (Map a Bool)

Documentation

satDPLL :: Ord a => Formula a -> Bool Source #

DPLL satisfiability algorithm.

Examples

Expand

>>> import AutoProof.Internal.Formula
>>> satDPLL $ Var "a"
True

>>> satDPLL $ And (Var "a") (Not (Var "a"))
False

satAssignmentDPLL :: Ord a => Formula a -> Maybe (Map a Bool) Source #

DPLL satisfiability algorithm, returning a satisfying truth assihnment, if there is one.

Examples

Expand

>>> a = And (Not (Var "a")) (Or (Var "b") (Var "c")) -- satisfiable
>>> Just t = satAssignmentDPLL a
>>> t
fromList [("a",False),("c",True)]
>>> t |= a
True

Note: The variable "b" is missing in the map above, which means that it's implictly assigned the value False.

>>> satAssignmentDPLL $ And (Var "a") (Not (Var "a")) -- unsatisfiable
Nothing