{"id":"W2785870089","doi":"10.29007/3pxg","title":"Improving SAT Solver Performance with Structure-based Preferential Bumping","year":2018,"lang":"en","type":"article","venue":"EPiC series in computing","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":5,"is_retracted":false,"has_abstract":true,"ca_institutions":"Simon Fraser University","funders":"Natural Sciences and Engineering Research Council of Canada","keywords":"Bumping; Solver; Exploit; Computer science; Boolean satisfiability problem; Computational science; Parallel computing; Theoretical computer science; Programming language; Engineering","routes":{"ca_aff":true,"ca_fund":true,"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.002452307,0.001422311,0.001148532,0.001633613,0.0008231339,0.001579961,0.004043581,0.001023346,0.009236298],"category_scores_gemma":[0.01891991,0.00112831,0.001162372,0.00185076,0.001412975,0.004698896,0.004284681,0.002803521,0.001883764],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001130211,"about_ca_system_score_gemma":0.00297554,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00239424,"about_ca_topic_score_gemma":0.005334128,"domain_scores_codex":[0.9973668,0.0008947984,0.0001913771,0.0004270452,0.0007433114,0.0003765821],"domain_scores_gemma":[0.9893292,0.005336556,0.0008097969,0.003225294,0.001031778,0.0002673681],"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.001886568,0.0004549293,0.007873099,0.001009721,0.0002115847,0.0003902909,0.0006555647,0.1454276,0.05871524,0.06520959,0.01441363,0.7037522],"study_design_scores_gemma":[0.0004011214,0.0006923961,0.0009539597,0.0001062893,0.0001980193,0.000242844,0.0001996957,0.8277661,0.07753012,0.08024389,0.01159116,0.00007436225],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.1462493,0.00106058,0.8223335,0.0009744574,0.0002577839,0.0003529034,0.0004399701,0.01848935,0.009842088],"genre_scores_gemma":[0.5243254,0.0003010658,0.4701031,0.000392186,0.00006579085,0.0002793927,0.0008623962,0.0009375665,0.002732971],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.009236298,"threshold_uncertainty_score":0.03089851,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0164611457732456,"score_gpt":0.2527593542021823,"score_spread":0.2362982084289367,"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."}}