{"id":"W4401633153","doi":"10.22215/etd/2024-16034","title":"Hardware-Accelerated SAT Solvers","year":2024,"lang":"en","type":"dissertation","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Carleton University","funders":"","keywords":"Computer science; Bottleneck; Parallel computing; Field-programmable gate array; DPLL algorithm; Boolean satisfiability problem; Solver; Hardware acceleration; Algorithm; Computer hardware; 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.0004167294,0.0009908746,0.0004512341,0.0007216595,0.0003620115,0.0009995369,0.001595377,0.0006484356,0.01771533],"category_scores_gemma":[0.001808997,0.0004000354,0.0008227602,0.0009047894,0.0003556233,0.00118547,0.0009677251,0.001308166,0.003443595],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0008260333,"about_ca_system_score_gemma":0.001663083,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002369327,"about_ca_topic_score_gemma":0.006527253,"domain_scores_codex":[0.9991422,0.0001741134,0.00004431146,0.000161094,0.0003485898,0.0001297111],"domain_scores_gemma":[0.9991222,0.0003035486,0.00006882856,0.0001919792,0.0002745714,0.0000388434],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"bench_or_experimental","study_design_scores_codex":[0.0004609457,0.0003989713,0.001894863,0.001023699,0.0001384369,0.0003911706,0.0001666304,0.2507061,0.06110435,0.0728419,0.04350967,0.5673632],"study_design_scores_gemma":[0.0002000906,0.000252262,0.000574531,0.00007245828,0.0000599567,0.0002361728,0.00005838728,0.895005,0.03179665,0.02497091,0.04674762,0.00002590892],"study_design_candidate":"bench_or_experimental","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.05682646,0.001532465,0.8739302,0.0009963643,0.0004186469,0.0002425977,0.0008640715,0.01628558,0.04890353],"genre_scores_gemma":[0.2647792,0.0006367566,0.7189925,0.0004049442,0.0001114175,0.0002125458,0.001893437,0.0007494666,0.01221964],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.01771533,"threshold_uncertainty_score":0.05926371,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04327861835523929,"score_gpt":0.3346166273715036,"score_spread":0.2913380090162643,"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."}}