@inproceedings{Wan-Son-Stu_CPAIOR16,
  author    = {Wenxi Wang and 
		Harald S{\o}ndergaard and 
		Peter J. Stuckey},
  title     = {A Bit-Vector Solver with Word-Level Propagation},
  editor    = {C.-G. Quimper},
  booktitle = {Integration of AI and OR Techniques in Constraint Programming:
                Proceedings of the 13th International Conference},
  series    = {Lecture Notes in Computer Science},
  volume    = {9676},
  pages     = {374--391},
  publisher = {Springer International Publishing},
  year      = {2016},
  isbn      = {978-3-319-33953-5},
  doi       = {10.1007/978-3-319-33954-2_27},
  abstract  = {Reasoning with bit-vectors arises in a variety of 
		applications in verification and cryptography. 
		Michel and Van Hentenryck have proposed an interesting 
		approach to bit-vector constraint propagation on the 
		word level. Each of the operations except comparison 
		are constant time, assuming the bit-vector fits in a 
		machine word. In contrast, bit-vector SMT solvers 
		usually solve bit-vector problems by bit-blasting, 
		that is, mapping the resulting operations to conjunctive 
		normal form clauses, and using SAT technology to solve 
		them. This also means generating intermediate variables 
		which can be an advantage, as these can be searched on 
		and learnt about. Since each approach has advantages 
		it is important to see whether we can benefit from 
		these advantages by using a word-level propagation 
		approach with learning. In this paper we describe an 
		approach to bit-vector solving using word-level 
		propagation with learning. We provide alternative 
		word-level propagators to Michel and Van Hentenryck, 
		and give the first empirical evaluation of their approach
		that we are aware of. We show that, with careful 
		engineering, a word-level propagation based approach 
		can compete with (or complement) bit-blasting.},
  keywords  = {SMT solving, Constraint propagation, Program verification},
}

{"_id":"JHTaeoTEi5RhrhrWb","bibbaseid":"wang-sndergaard-stuckey-abitvectorsolverwithwordlevelpropagation-2016","author_short":["Wang, W.","Søndergaard, H.","Stuckey, P. J."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Wenxi"],"propositions":[],"lastnames":["Wang"],"suffixes":[]},{"firstnames":["Harald"],"propositions":[],"lastnames":["Søndergaard"],"suffixes":[]},{"firstnames":["Peter","J."],"propositions":[],"lastnames":["Stuckey"],"suffixes":[]}],"title":"A Bit-Vector Solver with Word-Level Propagation","editor":[{"firstnames":["C.-G."],"propositions":[],"lastnames":["Quimper"],"suffixes":[]}],"booktitle":"Integration of AI and OR Techniques in Constraint Programming: Proceedings of the 13th International Conference","series":"Lecture Notes in Computer Science","volume":"9676","pages":"374–391","publisher":"Springer International Publishing","year":"2016","isbn":"978-3-319-33953-5","doi":"10.1007/978-3-319-33954-2_27","abstract":"Reasoning with bit-vectors arises in a variety of applications in verification and cryptography. Michel and Van Hentenryck have proposed an interesting approach to bit-vector constraint propagation on the word level. Each of the operations except comparison are constant time, assuming the bit-vector fits in a machine word. In contrast, bit-vector SMT solvers usually solve bit-vector problems by bit-blasting, that is, mapping the resulting operations to conjunctive normal form clauses, and using SAT technology to solve them. This also means generating intermediate variables which can be an advantage, as these can be searched on and learnt about. Since each approach has advantages it is important to see whether we can benefit from these advantages by using a word-level propagation approach with learning. In this paper we describe an approach to bit-vector solving using word-level propagation with learning. We provide alternative word-level propagators to Michel and Van Hentenryck, and give the first empirical evaluation of their approach that we are aware of. We show that, with careful engineering, a word-level propagation based approach can compete with (or complement) bit-blasting.","keywords":"SMT solving, Constraint propagation, Program verification","bibtex":"@inproceedings{Wan-Son-Stu_CPAIOR16,\n author = {Wenxi Wang and \n\t\tHarald S{\\o}ndergaard and \n\t\tPeter J. Stuckey},\n title = {A Bit-Vector Solver with Word-Level Propagation},\n editor = {C.-G. Quimper},\n booktitle = {Integration of AI and OR Techniques in Constraint Programming:\n Proceedings of the 13th International Conference},\n series = {Lecture Notes in Computer Science},\n volume = {9676},\n pages = {374--391},\n publisher = {Springer International Publishing},\n year = {2016},\n isbn = {978-3-319-33953-5},\n doi = {10.1007/978-3-319-33954-2_27},\n abstract = {Reasoning with bit-vectors arises in a variety of \n\t\tapplications in verification and cryptography. \n\t\tMichel and Van Hentenryck have proposed an interesting \n\t\tapproach to bit-vector constraint propagation on the \n\t\tword level. Each of the operations except comparison \n\t\tare constant time, assuming the bit-vector fits in a \n\t\tmachine word. In contrast, bit-vector SMT solvers \n\t\tusually solve bit-vector problems by bit-blasting, \n\t\tthat is, mapping the resulting operations to conjunctive \n\t\tnormal form clauses, and using SAT technology to solve \n\t\tthem. This also means generating intermediate variables \n\t\twhich can be an advantage, as these can be searched on \n\t\tand learnt about. Since each approach has advantages \n\t\tit is important to see whether we can benefit from \n\t\tthese advantages by using a word-level propagation \n\t\tapproach with learning. In this paper we describe an \n\t\tapproach to bit-vector solving using word-level \n\t\tpropagation with learning. We provide alternative \n\t\tword-level propagators to Michel and Van Hentenryck, \n\t\tand give the first empirical evaluation of their approach\n\t\tthat we are aware of. We show that, with careful \n\t\tengineering, a word-level propagation based approach \n\t\tcan compete with (or complement) bit-blasting.},\n keywords = {SMT solving, Constraint propagation, Program verification},\n}\n\n","author_short":["Wang, W.","Søndergaard, H.","Stuckey, P. J."],"editor_short":["Quimper, C."],"key":"Wan-Son-Stu_CPAIOR16","id":"Wan-Son-Stu_CPAIOR16","bibbaseid":"wang-sndergaard-stuckey-abitvectorsolverwithwordlevelpropagation-2016","role":"author","urls":{},"keyword":["SMT solving","Constraint propagation","Program verification"],"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"people.eng.unimelb.edu.au/harald/bibbase.bib","dataSources":["yWvm3kzg5vKQAPLm7","ofmsZryxNDBSpE7j5","9aC4cxLD8D6oJ3FLN","wpkuJrZJJtqra3FbL","XqcrNTrCCBr9mSd37","W7ih7WyQivP4EDh83"],"keywords":["smt solving","constraint propagation","program verification"],"search_terms":["bit","vector","solver","word","level","propagation","wang","søndergaard","stuckey"],"title":"A Bit-Vector Solver with Word-Level Propagation","year":2016}