GitHub - scm2342/ocamlsat: Toy sat solver in ocaml, that uses robdds (basically it results in (Terminal, true) if your formula does not have any solutions)

scm2342 / ocamlsat Public

Notifications You must be signed in to change notification settings
Fork 0
Star 1

Toy sat solver in ocaml, that uses robdds (basically it results in (Terminal, true) if your formula does not have any solutions) - returns the bdd

1 star 0 forks Branches Tags Activity

Star

Notifications

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 18 Commits
Makefile		Makefile
README		README
bdd.ml		bdd.ml
lexer.mll		lexer.mll
parser.mly		parser.mly
pigeon.hs		pigeon.hs
sat.ml		sat.ml
type.ml		type.ml

Repository files navigation

A toy sat solver I wrote mostly one evening after a class in verified software systems at the TUHH.
Its not fast but it does not require you to enter your formula in cnf or dnf.
Currently it eats memory because the hashmap I use for the ITE algorithm in bdd.ml puts pointers on many objects in the weak hashmap. I do not care...

Have fun,
	Sven