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

Contents

Simple baseline algorithm
DPLL

Description

Satisfiability algorithms.

Synopsis

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

Simple baseline algorithm

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

DPLL

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