Guest User

satlib

a guest
Nov 16th, 2018
145
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. (ns satlib.core
  2. (:gen-class)
  3. (:require [clojure.set :refer [intersection difference union]])
  4. (:require [clojure.string :as str])
  5. )
  6.  
  7. (defn extract [clause]
  8. (let
  9. [
  10. true-side (get (get clause :true-side) :sat-set)
  11. false-side (get (get clause :false-side) :sat-set)
  12. ]
  13. {:t true-side :f false-side}
  14. )
  15. )
  16.  
  17. (defn display-cnf [label cnf]
  18. (println label (map extract cnf))
  19. )
  20.  
  21. (def init-stats
  22. {
  23. :count-steps 0
  24. :count-down 0
  25. :count-first 0
  26. :count-second 0
  27. :before-literals-true 0
  28. :before-literals-false 0
  29. :after-literals-true 0
  30. :after-literals-false 0
  31. :unit-true 0
  32. :unit-false 0
  33. :only-true 0
  34. :only-false 0
  35. :max-level 0
  36. :exhausted 0
  37. :contradiction 0
  38. }
  39. )
  40.  
  41. (defn update-stats [stats operation field amount]
  42. (assoc stats field (operation amount (get stats field)))
  43. )
  44.  
  45. (defn count-step [stats]
  46. (update-stats stats + :count-steps 1)
  47. )
  48.  
  49. (defn count-down [stats]
  50. (update-stats stats + :count-down 1)
  51. )
  52.  
  53. (defn count-first [stats]
  54. (update-stats stats + :count-first 1)
  55. )
  56.  
  57. (defn count-second [stats]
  58. (update-stats stats + :count-second 1)
  59. )
  60.  
  61. (defn exhausted [stats]
  62. (update-stats stats + :exhausted 1)
  63. )
  64.  
  65. (defn contradiction [stats]
  66. (update-stats stats + :contradiction 1)
  67. )
  68.  
  69. (defn before-literals [stats true-literals false-literals]
  70. (let [new-stats (update-stats stats + :before-literals-true (count true-literals))]
  71. (update-stats new-stats + :before-literals-false (count false-literals))
  72. )
  73. )
  74.  
  75. (defn after-literals [stats true-literals false-literals]
  76. (let [new-stats (update-stats stats + :after-literals-true (count true-literals))]
  77. (update-stats new-stats + :after-literals-false (count false-literals))
  78. )
  79. )
  80.  
  81. (defn count-units [stats true-units false-units]
  82. (let [new-stats (update-stats stats + :unit-true (count true-units))]
  83. (update-stats new-stats + :unit-false (count false-units))
  84. )
  85. )
  86.  
  87. (defn count-only [stats only-true only-false]
  88. (let [new-stats (update-stats stats + :only-true (count only-true))]
  89. (update-stats new-stats + :only-false (count only-false))
  90. )
  91. )
  92.  
  93. (defn max-level [stats level]
  94. (update-stats stats max :max-level level)
  95. )
  96.  
  97. (defn knuth-clause [line]
  98. (loop [literals (str/split line #" ") sat-true #{} sat-false #{}]
  99. (if (empty? literals)
  100.  
  101. {:sat-true sat-true :sat-false sat-false}
  102.  
  103. (let
  104. [
  105. this-one (first literals)
  106. remaining (rest literals)
  107. ]
  108.  
  109. (if (str/starts-with? this-one "~")
  110. (recur remaining sat-true (conj sat-false (subs this-one 1)))
  111. (recur remaining (conj sat-true this-one) sat-false)
  112. )
  113. )
  114. )
  115. )
  116. )
  117.  
  118. (defn knuth-cnf []
  119. (loop [line (read-line) result ()]
  120. (if line
  121. (if (or (str/starts-with? line "~ ") (str/blank? line))
  122. (recur (read-line) result)
  123. (recur (read-line) (cons (knuth-clause line) result))
  124. )
  125.  
  126. result
  127. )
  128. )
  129. )
  130.  
  131. (defn dimacs-clause [line]
  132. (loop [literals (str/split line #" ") sat-true #{} sat-false #{}]
  133. (if (empty? literals)
  134.  
  135. {:sat-true sat-true :sat-false sat-false}
  136.  
  137. (let
  138. [
  139. this-one (Integer. (first literals))
  140. remaining (rest literals)
  141. ]
  142.  
  143. (if (not (= 0 this-one))
  144. (if (> 0 this-one)
  145. (recur remaining sat-true (conj sat-false (- this-one)))
  146. (recur remaining (conj sat-true this-one) sat-false)
  147. )
  148.  
  149. {:sat-true sat-true :sat-false sat-false}
  150. )
  151. )
  152. )
  153. )
  154. )
  155.  
  156. (defn dimacs-cnf []
  157. (loop [line (read-line) result ()]
  158. (if line
  159. (if (or (str/starts-with? line "c") (str/starts-with? line "p") (str/blank? line))
  160. (recur (read-line) result)
  161. (recur (read-line) (cons (dimacs-clause line) result))
  162. )
  163. result
  164. )
  165. )
  166. )
  167.  
  168. (defn simplify [raw-cnf]
  169. (loop [clause-list raw-cnf result ()]
  170. (if (empty? clause-list)
  171. result
  172. (let
  173. [
  174. clause (first clause-list)
  175. input-sat-true (get clause :sat-true)
  176. input-sat-false (get clause :sat-false)
  177. tautology (intersection input-sat-true input-sat-false)
  178. sat-true (difference input-sat-true tautology)
  179. sat-false (difference input-sat-false tautology)
  180. ]
  181. (if (and (empty? sat-true) (empty? sat-false))
  182. (recur (rest clause-list) result)
  183. (recur (rest clause-list) (cons {:sat-true sat-true :sat-false sat-false} result))
  184. )
  185. )
  186. )
  187. )
  188. )
  189.  
  190. (defn get-size [raw-cnf]
  191. (loop [clause-list raw-cnf literal-set #{}]
  192. (if (empty? clause-list)
  193. (count literal-set)
  194. (let
  195. [
  196. clause (first clause-list)
  197. sat-true (get clause :sat-true)
  198. sat-false (get clause :sat-false)
  199. ]
  200. (recur (rest clause-list) (union literal-set (union sat-true sat-false)))
  201. )
  202. )
  203. )
  204. )
  205.  
  206. (declare scan-cnf)
  207.  
  208. (defn make-side [sat-set jump-level]
  209. {:sat-set sat-set :jump-level jump-level}
  210. )
  211.  
  212. (defn make-clause [sat-true sat-false level-true level-false]
  213. {:true-side (make-side sat-true level-true) :false-side (make-side sat-false level-false)}
  214. )
  215.  
  216. (defn make-cnf [raw-cnf infinity]
  217. (loop [clause-list raw-cnf result ()]
  218. (if (empty? clause-list)
  219. result
  220. (let
  221. [
  222. clause (first clause-list)
  223. sat-true (get clause :sat-true)
  224. sat-false (get clause :sat-false)
  225. ]
  226. (recur (rest clause-list) (cons (make-clause sat-true sat-false infinity infinity) result))
  227. )
  228. )
  229. )
  230. )
  231.  
  232. (defn unit? [sat-first sat-second]
  233. (= 1 (+ (count sat-first) (count sat-second)))
  234. )
  235.  
  236. (def empty-answer {:true-side #{} :false-side #{}})
  237.  
  238. (defn update-answer [assert-literals old-answer]
  239. {
  240. :true-side (union (get assert-literals :true-side) (get old-answer :true-side))
  241. :false-side (union (get assert-literals :false-side) (get old-answer :false-side))
  242. }
  243. )
  244.  
  245. (defn get-try [cnf]
  246. (let
  247. [
  248. clause (first cnf)
  249. sat-true (get (get clause :true-side) :sat-set)
  250. ]
  251. (if (empty? sat-true)
  252. (first (get (get clause :false-side) :sat-set))
  253. (first sat-true)
  254. )
  255. )
  256. )
  257.  
  258. (defn first-try [options cnf]
  259. {:true-side #{(get-try cnf)} :false-side #{}}
  260. )
  261.  
  262. (defn second-try [options cnf]
  263. {:true-side #{} :false-side #{(get-try cnf)}}
  264. )
  265.  
  266. (defn descend [options infinity level cnf accumulator stats]
  267. (let
  268. [
  269. true-set (get accumulator :true-set)
  270. false-set (get accumulator :false-set)
  271. unit-true (get accumulator :true-unit)
  272. unit-false (get accumulator :false-unit)
  273. only-true (difference true-set false-set)
  274. only-false (difference false-set true-set)
  275. assert-true (union only-true unit-true)
  276. assert-false (union only-false unit-false)
  277. new-stats (count-units (count-only stats only-true only-false) unit-true unit-false)
  278. ]
  279. (if (and (empty? assert-true) (empty? assert-false))
  280. (let
  281. [
  282. new-level (+ level 1)
  283. assert-literals (first-try options cnf)
  284. latest-stats (count-first new-stats)
  285. result (scan-cnf options infinity cnf new-level assert-literals latest-stats)
  286. ]
  287. (if (get result :sat)
  288. result
  289. (let
  290. [
  291. try2 (second-try options cnf)
  292. latest-stats (count-second (get result :stats))
  293. ]
  294. (scan-cnf options infinity cnf new-level try2 latest-stats)
  295. )
  296. )
  297. )
  298. (let
  299. [
  300. assert-literals {:true-side assert-true :false-side assert-false}
  301. latest-stats (count-down new-stats)
  302. ]
  303. (scan-cnf options infinity cnf level assert-literals latest-stats)
  304. )
  305. )
  306. )
  307. )
  308.  
  309. (defn end-scan [options infinity sat level cnf assert-literals accumulator stats]
  310. (if sat
  311. (if (empty? cnf)
  312. {:sat true :answer (update-answer assert-literals empty-answer) :stats stats}
  313. (if (empty? (intersection (get accumulator :true-unit) (get accumulator :false-unit)))
  314. (let [result (descend options infinity level cnf accumulator stats)]
  315. (if (get result :sat)
  316. (let
  317. [
  318. new-answer (update-answer assert-literals (get result :answer))
  319. new-stats (get result :stats)
  320. ]
  321. {:sat true :answer new-answer :stats new-stats}
  322. )
  323. result
  324. )
  325. )
  326. {:sat false :level level :stats (contradiction stats)}
  327. )
  328. )
  329. {:sat false :level level :stats stats}
  330. )
  331. )
  332.  
  333. (defn unit [this-side other-side]
  334. (if (unit? this-side other-side)
  335. this-side
  336. #{}
  337. )
  338. )
  339.  
  340. (defn reduce-clause [options cnf sat level clause assert-true assert-false accumulator stats]
  341. (let
  342. [
  343. sat-true (get (get clause :true-side) :sat-set)
  344. sat-false (get (get clause :false-side) :sat-set)
  345. new-sat-true (difference sat-true assert-false)
  346. new-sat-false (difference sat-false assert-true)
  347. new-stats (after-literals stats new-sat-true new-sat-false)
  348. ]
  349. (if (and (empty? new-sat-true) (empty? new-sat-false))
  350. (let
  351. [
  352. tmp-level (get (get clause (get (get options :which-first) :jump)) :jump-level)
  353. new-level (min level tmp-level)
  354. ]
  355. {:sat false :level new-level :cnf () :accumulator {} :stats (exhausted new-stats)}
  356. )
  357. (let
  358. [
  359. level-true (get (get clause :true-side) :jump-level)
  360. level-false (get (get clause :false-side) :jump-level)
  361. new-level-true level-true
  362. new-level-false level-false
  363. true-set (union (get accumulator :true-set) new-sat-true)
  364. false-set (union (get accumulator :false-set) new-sat-false)
  365. true-unit (union (get accumulator :true-unit) (unit new-sat-true new-sat-false))
  366. false-unit (union (get accumulator :false-unit) (unit new-sat-false new-sat-true))
  367. ]
  368. {
  369. :sat sat
  370. :level level
  371. :cnf (cons (make-clause new-sat-true new-sat-false new-level-true new-level-false) cnf)
  372. :accumulator
  373. {
  374. :true-set true-set
  375. :false-set false-set
  376. :true-unit true-unit
  377. :false-unit false-unit
  378. }
  379. :stats new-stats
  380. }
  381. )
  382. )
  383. )
  384. )
  385.  
  386. (defn do-clause [options sat level clause cnf assert-literals accumulator stats]
  387. (let
  388. [
  389. sat-true (get (get clause :true-side) :sat-set)
  390. sat-false (get (get clause :false-side) :sat-set)
  391. assert-true (get assert-literals :true-side)
  392. assert-false (get assert-literals :false-side)
  393. new-stats (before-literals stats sat-true sat-false)
  394. ]
  395. (if (and
  396. (empty? (intersection assert-true sat-true))
  397. (empty? (intersection assert-false sat-false))
  398. )
  399. (reduce-clause options cnf sat level clause assert-true assert-false accumulator new-stats)
  400. {:sat sat :level level :cnf cnf :accumulator accumulator :stats new-stats}
  401. )
  402. )
  403. )
  404.  
  405. (defn scan-cnf [options infinity base-cnf level assert-literals start-stats]
  406. (loop
  407. [
  408. clause-list base-cnf
  409. sat true
  410. jump-level infinity
  411. cnf ()
  412. accumulator {:true-set #{} :false-set #{} :true-unit #{} :false-unit #{}}
  413. stats start-stats
  414. ]
  415. (if (empty? clause-list)
  416. (end-scan options infinity sat level cnf assert-literals accumulator stats)
  417. (let
  418. [
  419. clause (first clause-list)
  420. clause-result (do-clause options sat level clause cnf assert-literals accumulator stats)
  421. new-sat (get clause-result :sat)
  422. new-level (get clause-result :level)
  423. new-cnf (get clause-result :cnf)
  424. new-accumulator (get clause-result :accumulator)
  425. new-stats (max-level (count-step (get clause-result :stats)) level)
  426. ]
  427. (recur (rest clause-list) new-sat new-level new-cnf new-accumulator new-stats)
  428. )
  429. )
  430. )
  431. )
  432.  
  433. (def init-assert {:true-side #{} :false-side #{}})
RAW Paste Data