Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
Data types
Our construction generalizes to arbitrary NNF formulas, and possibly to arbitrary SAT, but we don't need to bother; just CNF is good enough
Instances
Eq Lit Source # | |
Ord Lit Source # | |
Show Lit Source # | |
Generic Lit Source # | |
Hashable Lit Source # | |
Defined in Application.SAT | |
Pretty Lit Source # | |
type Rep Lit Source # | |
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.