{"id":145451,"date":"2008-05-01T00:00:00","date_gmt":"2008-05-01T00:00:00","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/msr-research-item\/designing-an-efficient-hardware-implication-accelerator-for-sat-solving\/"},"modified":"2018-10-16T20:17:19","modified_gmt":"2018-10-17T03:17:19","slug":"designing-an-efficient-hardware-implication-accelerator-for-sat-solving","status":"publish","type":"msr-research-item","link":"https:\/\/www.microsoft.com\/en-us\/research\/publication\/designing-an-efficient-hardware-implication-accelerator-for-sat-solving\/","title":{"rendered":"Designing an Efficient Hardware Implication Accelerator for SAT Solving"},"content":{"rendered":"<div class=\"asset-content\">\n<p>This paper discusses the design of a hardware accelerator for Boolean Constraint Propagation (BCP) using Field Programmable Gate Arrays (FPGA). In particular, we describe the detailed implementation of the inference engine, a key component of the accelerator that performs implications. Unlike previous efforts in FPGA assisted SAT solving, our design uses Block RAM (BRAM) to store instance information. This novel design not only facilitates fast lookup and update, but also avoids synthesizing overhead for each SAT instance. We demonstrate that SAT instances can be easily partitioned into multiple groups that can be processed by multiple inference engines in parallel. By exploiting parallelism in hardware, the BCP accelerator can infer implications in 6 to 17 clock cycles for a new variable assignment. In addition, our design supports dynamic insertion and deletion of learned clauses. Cycle accurate simulation shows that our BCP accelerator is 5~16 times faster than the conventional software based approach for BCP.<\/p>\n<\/div>\n<p><!-- .asset-content --><\/p>\n","protected":false},"excerpt":{"rendered":"<p>This paper discusses the design of a hardware accelerator for Boolean Constraint Propagation (BCP) using Field Programmable Gate Arrays (FPGA). In particular, we describe the detailed implementation of the inference engine, a key component of the accelerator that performs implications. Unlike previous efforts in FPGA assisted SAT solving, our design uses Block RAM (BRAM) to [&hellip;]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr-author-ordering":null,"msr_publishername":"Springer","msr_publisher_other":"","msr_booktitle":"International Conference on Theory and Applications of Satisfiability Testing (SAT)","msr_chapter":"","msr_edition":"International Conference on Theory and Applications of Satisfiability Testing (SAT)","msr_editors":"","msr_how_published":"","msr_isbn":"978-3-540-79718-0","msr_issue":"","msr_journal":"","msr_number":"","msr_organization":"","msr_pages_string":"48-62","msr_page_range_start":"48","msr_page_range_end":"62","msr_series":"Lecture Notes in Computer Science","msr_volume":"4996","msr_copyright":"","msr_conference_name":"International Conference on Theory and Applications of Satisfiability Testing (SAT)","msr_doi":"","msr_arxiv_id":"","msr_s2_paper_id":"","msr_mag_id":"","msr_pubmed_id":"","msr_other_authors":"Zhangxi Tan","msr_other_contributors":"","msr_speaker":"","msr_award":"","msr_affiliation":"","msr_institution":"","msr_host":"","msr_version":"","msr_duration":"","msr_original_fields_of_study":"","msr_release_tracker_id":"","msr_s2_match_type":"","msr_citation_count_updated":"","msr_published_date":"2008-05-01","msr_highlight_text":"","msr_notes":"","msr_longbiography":"","msr_publicationurl":"http:\/\/dx.doi.org\/10.1007\/978-3-540-79719-7_6","msr_external_url":"","msr_secondary_video_url":"","msr_conference_url":"","msr_journal_url":"","msr_s2_pdf_url":"","msr_year":2008,"msr_citation_count":0,"msr_influential_citations":0,"msr_reference_count":0,"msr_s2_match_confidence":0,"msr_microsoftintellectualproperty":true,"msr_s2_open_access":false,"msr_s2_author_ids":[],"msr_pub_ids":[],"msr_hide_image_in_river":0,"footnotes":""},"msr-research-highlight":[],"research-area":[13547],"msr-publication-type":[193716],"msr-publisher":[],"msr-focus-area":[],"msr-locale":[268875],"msr-post-option":[],"msr-field-of-study":[],"msr-conference":[],"msr-journal":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-145451","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-systems-and-networking","msr-locale-en_us"],"msr_publishername":"Springer","msr_edition":"International Conference on Theory and Applications of Satisfiability Testing (SAT)","msr_affiliation":"","msr_published_date":"2008-05-01","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"International Conference on Theory and Applications of Satisfiability Testing (SAT)","msr_pages_string":"48-62","msr_chapter":"","msr_isbn":"978-3-540-79718-0","msr_journal":"","msr_volume":"4996","msr_number":"","msr_editors":"","msr_series":"Lecture Notes in Computer Science","msr_issue":"","msr_organization":"","msr_how_published":"","msr_notes":"","msr_highlight_text":"","msr_release_tracker_id":"","msr_original_fields_of_study":"","msr_download_urls":"","msr_external_url":"","msr_secondary_video_url":"","msr_longbiography":"","msr_microsoftintellectualproperty":1,"msr_main_download":"","msr_publicationurl":"http:\/\/dx.doi.org\/10.1007\/978-3-540-79719-7_6","msr_doi":"","msr_publication_uploader":[{"type":"url","title":"http:\/\/dx.doi.org\/10.1007\/978-3-540-79719-7_6","viewUrl":false,"id":false,"label_id":0}],"msr_related_uploader":"","msr_citation_count":0,"msr_citation_count_updated":"","msr_s2_paper_id":"","msr_influential_citations":0,"msr_reference_count":0,"msr_arxiv_id":"","msr_s2_author_ids":[],"msr_s2_open_access":false,"msr_s2_pdf_url":null,"msr_attachments":[{"id":0,"url":"http:\/\/dx.doi.org\/10.1007\/978-3-540-79719-7_6"}],"msr-author-ordering":[{"type":"user_nicename","value":"joda","user_id":32353,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=joda"},{"type":"text","value":"Zhangxi Tan","user_id":0,"rest_url":false},{"type":"user_nicename","value":"fangyu","user_id":31779,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=fangyu"},{"type":"user_nicename","value":"lintaoz","user_id":32693,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=lintaoz"}],"msr_impact_theme":[],"msr_research_lab":[],"msr_event":[],"msr_group":[],"msr_project":[169466],"publication":[],"video":[],"msr-tool":[],"msr_publication_type":"inproceedings","related_content":{"projects":[{"ID":169466,"post_title":"BEE3","post_name":"bee3","post_type":"msr-project","post_date":"2008-02-26 11:25:38","post_modified":"2017-06-01 18:42:27","post_status":"publish","permalink":"https:\/\/www.microsoft.com\/en-us\/research\/project\/bee3\/","post_excerpt":"The BEE3 (Berkeley Emulation Engine, version 3) is a multi-FPGA system with up to 64 GB of DRAM and several I\/O subsystems that can be used to enable faster, larger and higher fidelity computer architecture or other systems research. Objective: Revitalizing Computer Architecture Research The Problem Computer Architecture is increasingly incremental, and boring. Many papers study a tiny feature, and report 5% improvements. Simulation is too slow to allow full-system experiments running real software. Researchers&hellip;","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/169466"}]}}]},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/145451","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-research-item"}],"version-history":[{"count":1,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/145451\/revisions"}],"predecessor-version":[{"id":525706,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/145451\/revisions\/525706"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=145451"}],"wp:term":[{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=145451"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=145451"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=145451"},{"taxonomy":"msr-publisher","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publisher?post=145451"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=145451"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=145451"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=145451"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=145451"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=145451"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=145451"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=145451"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=145451"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}