{"id":"W2068567751","doi":"10.1109/dsd.2013.31","title":"An Efficient Hardware Implementation of a SAT Problem Solver on FPGA","year":2013,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":15,"is_retracted":false,"has_abstract":true,"ca_institutions":"Université de Montréal","funders":"","keywords":"Computer science; Field-programmable gate array; Scalability; Parallel computing; VHDL; Boolean satisfiability problem; Solver; Compiler; Memory footprint; Computer hardware; Backtracking; Algorithm; Embedded system; Programming language","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0003369835,0.0009498191,0.0005496122,0.0006806296,0.0003471151,0.0008656416,0.001315339,0.0004174381,0.02321849],"category_scores_gemma":[0.0008397079,0.0003702466,0.0005492131,0.0006727076,0.0001958595,0.0005535708,0.0003721324,0.0007120319,0.004980948],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0006379191,"about_ca_system_score_gemma":0.001071977,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001852544,"about_ca_topic_score_gemma":0.002904787,"domain_scores_codex":[0.9995919,0.00007757836,0.00003209931,0.00008063873,0.0001296531,0.00008826583],"domain_scores_gemma":[0.9996756,0.0001355317,0.00002137117,0.00006524458,0.00008193281,0.00002026077],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.001331188,0.0004304102,0.002877356,0.00113513,0.0002460875,0.001053894,0.0001985812,0.1275259,0.1455681,0.03147687,0.03386104,0.6542953],"study_design_scores_gemma":[0.0006161308,0.001052545,0.002653553,0.000128014,0.0001671116,0.0009365567,0.0001258029,0.7858217,0.1444706,0.00669317,0.05726692,0.00006793866],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.08060961,0.000507948,0.8472723,0.0002974947,0.0002463053,0.0005239171,0.001364006,0.03165654,0.03752186],"genre_scores_gemma":[0.4291759,0.0002159647,0.5580139,0.0001735143,0.00004025275,0.0004391949,0.001874386,0.0005420101,0.009524912],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.02321849,"threshold_uncertainty_score":0.07767355,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02523391197592975,"score_gpt":0.3300692443921049,"score_spread":0.3048353324161751,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}