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.Simple

Description

A simple baseline SAT algorithm.

Synopsis

satSimple :: Eq a => Formula a -> Bool
satAssignmentSimple :: Ord a => Formula a -> Maybe (Map a Bool)

Documentation

satSimple :: Eq a => Formula a -> Bool Source #

A simple baseline satisfiability algorithm.

This algorithm is based on the observation that if \(a\) is a propositional formula and \(x\) is a propositional variable, then \(a\) is satisfiable if and only if either \(a[\top/x]\) is satisfiable or \(a[\bot/x]\) is satisfiable.

Examples

Expand

>>> satSimple $ Var "a"
True

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

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

A simple baseline satisfiability algorithm, returning a satisfying truth assignment if there is one.

This algorithm is based on the observation that if \(a\) is a propositional formula and \(x\) is a propositional variable, then \(a\) is satisfiable if and only if either \(a[\top/x]\) is satisfiable or \(a[\bot/x]\) is satisfiable.

Examples

Expand

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

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