Skip to content

Latest commit

 

History

History
51 lines (44 loc) · 1.88 KB

README.md

File metadata and controls

51 lines (44 loc) · 1.88 KB

simpleCDCL

graded project for 'Logic and program verification'

This code is essentially a loyal implementation of GRASP(Joa˜o P. Marques-Silva et al) algorithm in python, without the unique implication points optimization.

Key points in implementation

  • several dicts(inside var_info, var_value) are maintained for fast lookup for unit clauses
  • use of python generator(source: step.inflate_clause()) when calculating causes_of (see the paper in page #5, formula (3))
  • iterative(not recursive)(source: step() push() pop()) approach of main DFS procedure
    • note: instead of exact undoing the side-effects(removing the entire clause when satisfied or removing the literal when unsatisfied, before_unmount() after_mounted()) of assignments during pop() process, one must follow the reverse mapping rev from variables to clauses in order to cover the newly-learned clause. see 1f4aaf1
  • the ever-true clause where a variable exists in both positive and negative form just hurts the program, and must be got rid of, see also #1

Benchmarks

open tests: python3.61/archlinux/HyperV/Core i7 [email protected] (time in seconds)

BMC fl100 fl30 sw100 uf100
>30s 1.41 0.04 0.29 0.72
bf26 h6 h7 pret uf100
1.47 0.72 8.73 3.77 1.75