{"id":"W2564001612","doi":"10.1609/aaai.v30i1.10439","title":"Exponential Recency Weighted Average Branching Heuristic for SAT Solvers","year":2016,"lang":"en","type":"article","venue":"Proceedings of the AAAI Conference on Artificial Intelligence","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":67,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"","keywords":"Heuristics; Heuristic; Branching (polymer chemistry); Computer science; Hash function; Benchmark (surveying); Exponential function; Theoretical computer science; Algorithm; Mathematics; Artificial intelligence; 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.002992206,0.001314527,0.001177268,0.001397001,0.0006936719,0.001356537,0.002385614,0.001367823,0.005983329],"category_scores_gemma":[0.010811,0.0007078224,0.001073709,0.001739197,0.001128991,0.002337346,0.001339506,0.003482911,0.001237304],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00202946,"about_ca_system_score_gemma":0.003089144,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.004352357,"about_ca_topic_score_gemma":0.008227794,"domain_scores_codex":[0.9980939,0.0008693718,0.00009662884,0.000298038,0.0004100681,0.000232],"domain_scores_gemma":[0.9939434,0.004654277,0.0002864901,0.0004954124,0.000423331,0.0001970017],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0005428503,0.0003298715,0.00203478,0.0003573224,0.0001057723,0.0001288117,0.000203023,0.6389019,0.003938026,0.065805,0.0104467,0.2772059],"study_design_scores_gemma":[0.00008838598,0.00006714489,0.0001307117,0.00003103522,0.00002166343,0.00002759132,0.00002989904,0.9579946,0.001129206,0.03856017,0.001909583,0.000009987663],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.05583769,0.001478861,0.9253277,0.001122404,0.000146914,0.0003005163,0.0003642335,0.003374012,0.01204763],"genre_scores_gemma":[0.3195892,0.0005255864,0.6730819,0.0007547639,0.00009647089,0.0004772591,0.001037945,0.0006303519,0.003806517],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.005983329,"threshold_uncertainty_score":0.02001619,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.08381016544744409,"score_gpt":0.3122846525582125,"score_spread":0.2284744871107685,"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."}}