TruthAssignment () a Source #	Assigns all propositional variables the truth value `False`. Can be used to evaluate closed formulas. Examples Expand `>>>` `() \|= (Var "a")`False `>>>` `() \|= (Or (Lit True) (Lit False))`True
Instance details Defined in AutoProof.Internal.Classical.SAT.TruthAssignment Methods evalVar :: () -> a -> Bool Source # evalFormula :: () -> Formula a -> Bool Source #
Ord a => TruthAssignment (Map a Bool) a Source #	Truth assignments where a missing key in the map is interpreted as `False`. Examples Expand `>>>` `t = Map.fromList $ [("a", True), ("b", False)]``>>>` `t \|= And (Var "a") (Not (Var "b"))`True `>>>` `t = Map.fromList $ [("a", True)]``>>>` `t \|= Imp (Var "a") (Var "b")`False
Instance details Defined in AutoProof.Internal.Classical.SAT.TruthAssignment Methods evalVar :: Map a Bool -> a -> Bool Source # evalFormula :: Map a Bool -> Formula a -> Bool Source #

(|=) :: TruthAssignment t a => t -> Formula a -> Bool infix 5 Source #

Semantic entailment relation. This is an infix alias of evalFormula.

Examples

Expand

>>> t = Map.fromList $ [("a", True), ("b", False)]
>>> t |= And (Var "a") (Not (Var "b"))
True

Satisfiability algorithms

Check satisfiability

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

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

Satisfying assignment search

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

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