Safe Haskell	None
Language	Haskell2010

Application.SAT

Contents

Data types
Solving
Examples

Description

A very bad SAT solver written by reduction to ECTA

Also a constructive proof of the NP-hardness of finding a term represented by an ECTA

Synopsis

data Var
mkVar :: Text -> Var
data CNF = And [Clause]
data Clause = Or [Lit]
data Lit
- = PosLit Var
- | NegLit Var
toEcta :: CNF -> Node
allSolutions :: CNF -> HashSet (HashMap Var Bool)
ex1 :: CNF
ex2 :: CNF
ex3 :: CNF

Data types

data Var Source #

Instances

Instances details

Eq Var Source #
Instance details Defined in Application.SAT Methods (==) :: Var -> Var -> Bool # (/=) :: Var -> Var -> Bool #
Ord Var Source #
Instance details Defined in Application.SAT Methods compare :: Var -> Var -> Ordering # (<) :: Var -> Var -> Bool # (<=) :: Var -> Var -> Bool # (>) :: Var -> Var -> Bool # (>=) :: Var -> Var -> Bool # max :: Var -> Var -> Var # min :: Var -> Var -> Var #
Show Var Source #
Instance details Defined in Application.SAT Methods showsPrec :: Int -> Var -> ShowS # show :: Var -> String # showList :: [Var] -> ShowS #
IsString Var Source #
Instance details Defined in Application.SAT Methods fromString :: String -> Var #
Generic Var Source #
Instance details Defined in Application.SAT Associated Types type Rep Var :: Type -> Type # Methods from :: Var -> Rep Var x # to :: Rep Var x -> Var #
Hashable Var Source #
Instance details Defined in Application.SAT Methods hashWithSalt :: Int -> Var -> Int # hash :: Var -> Int #
type Rep Var Source #
Instance details Defined in Application.SAT type Rep Var = D1 ('MetaData "Var" "Application.SAT" "ecta-1.0.0.3-GsgcdoZGkFZA4oJqDsbHRS" 'True) (C1 ('MetaCons "Var" 'PrefixI 'True) (S1 ('MetaSel ('Just "unVar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)))

mkVar :: Text -> Var Source #

data CNF Source #

Our construction generalizes to arbitrary NNF formulas, and possibly to arbitrary SAT, but we don't need to bother; just CNF is good enough

Constructors

And [Clause]

Instances

Instances details

Eq CNF Source #
Instance details Defined in Application.SAT Methods (==) :: CNF -> CNF -> Bool # (/=) :: CNF -> CNF -> Bool #
Ord CNF Source #
Instance details Defined in Application.SAT Methods compare :: CNF -> CNF -> Ordering # (<) :: CNF -> CNF -> Bool # (<=) :: CNF -> CNF -> Bool # (>) :: CNF -> CNF -> Bool # (>=) :: CNF -> CNF -> Bool # max :: CNF -> CNF -> CNF # min :: CNF -> CNF -> CNF #
Show CNF Source #
Instance details Defined in Application.SAT Methods showsPrec :: Int -> CNF -> ShowS # show :: CNF -> String # showList :: [CNF] -> ShowS #
Generic CNF Source #
Instance details Defined in Application.SAT Associated Types type Rep CNF :: Type -> Type # Methods from :: CNF -> Rep CNF x # to :: Rep CNF x -> CNF #
Hashable CNF Source #
Instance details Defined in Application.SAT Methods hashWithSalt :: Int -> CNF -> Int # hash :: CNF -> Int #
type Rep CNF Source #
Instance details Defined in Application.SAT type Rep CNF = D1 ('MetaData "CNF" "Application.SAT" "ecta-1.0.0.3-GsgcdoZGkFZA4oJqDsbHRS" 'False) (C1 ('MetaCons "And" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause])))

data Clause Source #

Constructors

Or [Lit]

Instances

Instances details

Eq Clause Source #
Instance details Defined in Application.SAT Methods (==) :: Clause -> Clause -> Bool # (/=) :: Clause -> Clause -> Bool #
Ord Clause Source #
Instance details Defined in Application.SAT Methods compare :: Clause -> Clause -> Ordering # (<) :: Clause -> Clause -> Bool # (<=) :: Clause -> Clause -> Bool # (>) :: Clause -> Clause -> Bool # (>=) :: Clause -> Clause -> Bool # max :: Clause -> Clause -> Clause # min :: Clause -> Clause -> Clause #
Show Clause Source #
Instance details Defined in Application.SAT Methods showsPrec :: Int -> Clause -> ShowS # show :: Clause -> String # showList :: [Clause] -> ShowS #
Generic Clause Source #
Instance details Defined in Application.SAT Associated Types type Rep Clause :: Type -> Type # Methods from :: Clause -> Rep Clause x # to :: Rep Clause x -> Clause #
Hashable Clause Source #
Instance details Defined in Application.SAT Methods hashWithSalt :: Int -> Clause -> Int # hash :: Clause -> Int #
type Rep Clause Source #
Instance details Defined in Application.SAT type Rep Clause = D1 ('MetaData "Clause" "Application.SAT" "ecta-1.0.0.3-GsgcdoZGkFZA4oJqDsbHRS" 'False) (C1 ('MetaCons "Or" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Lit])))

data Lit Source #

Constructors

PosLit Var
NegLit Var

Instances

Instances details

Eq Lit Source #
Instance details Defined in Application.SAT Methods (==) :: Lit -> Lit -> Bool # (/=) :: Lit -> Lit -> Bool #
Ord Lit Source #
Instance details Defined in Application.SAT Methods compare :: Lit -> Lit -> Ordering # (<) :: Lit -> Lit -> Bool # (<=) :: Lit -> Lit -> Bool # (>) :: Lit -> Lit -> Bool # (>=) :: Lit -> Lit -> Bool # max :: Lit -> Lit -> Lit # min :: Lit -> Lit -> Lit #
Show Lit Source #
Instance details Defined in Application.SAT Methods showsPrec :: Int -> Lit -> ShowS # show :: Lit -> String # showList :: [Lit] -> ShowS #
Generic Lit Source #
Instance details Defined in Application.SAT Associated Types type Rep Lit :: Type -> Type # Methods from :: Lit -> Rep Lit x # to :: Rep Lit x -> Lit #
Hashable Lit Source #
Instance details Defined in Application.SAT Methods hashWithSalt :: Int -> Lit -> Int # hash :: Lit -> Int #
Pretty Lit Source #
Instance details Defined in Application.SAT Methods pretty :: Lit -> Text Source #
type Rep Lit Source #
Instance details Defined in Application.SAT type Rep Lit = D1 ('MetaData "Lit" "Application.SAT" "ecta-1.0.0.3-GsgcdoZGkFZA4oJqDsbHRS" 'False) (C1 ('MetaCons "PosLit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Var)) :+: C1 ('MetaCons "NegLit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Var)))

Solving

toEcta :: CNF -> Node Source #

Encoding: formula(assnNode, formulaNode)

assnNode: * One edge, with one child per literal (2*numVars total) * Each literal has two choices, true or false * Use constraints to force each positive/negative pair of literals to match. * E.g.: x1 node = choice of (0, a) or (1, b). ~x1 node = choice of (0, b) or (1, a) If x1~x1 have indices 01, then the constraint 0.1=1.1 constrains x1~x1 to be either truefalse or false/true

formulaNode: * One edge, having one child per clause

Clause nodes: * One edge per literal in the clause, each corresponding to a choice of which variable makes the clause true. * Each edge has 2*numVars children containing a copy of the assnNode, followed by a single child containing "1" * Constrain said final child to be equal to the truth value of the corresponding literal in those 2*numVars children which copy the assnNode

Top level constraints: * Constrain the variable nodes in each clause node to be equal to the global variable assignments.

allSolutions :: CNF -> HashSet (HashMap Var Bool) Source #

Examples

ex1 :: CNF Source #

ex2 :: CNF Source #

ex3 :: CNF Source #