satcore

(ns sat.core
  (:gen-class)
  (:use satlib)
)


(defn -main
	"SAT solver"
	[& args]
	(let
		[
			raw-cnf (simplify (dimacs-cnf))
			infinity (+ 1 (get-size raw-cnf))
			options {:which-first {:first true :second false :jump :false-side}}
			cnf (make-cnf raw-cnf infinity)
		]
(display-cnf "input" cnf)
		(let
			[
				result (scan-cnf options infinity cnf 0 init-assert init-stats)
				sat (get result :sat)
			]
			(if sat
				(println "SAT" (get result :answer))
				(println "UNSAT")
			)

			(println (sort (get result :stats)))
		)
	)
)