{"id":"W3038610974","doi":"10.1007/978-3-030-51825-7_17","title":"Towards a Complexity-Theoretic Understanding of Restarts in SAT Solvers","year":2020,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":5,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Toronto; University of Waterloo","funders":"","keywords":"Computer science; Theoretical computer science","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.005026837,0.001425709,0.00151847,0.002488022,0.002088316,0.008158429,0.006076871,0.003410658,0.01231737],"category_scores_gemma":[0.01932088,0.001787849,0.003135733,0.002930363,0.009017539,0.01780675,0.00534958,0.0119934,0.002108962],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00401769,"about_ca_system_score_gemma":0.001929568,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00239325,"about_ca_topic_score_gemma":0.002532006,"domain_scores_codex":[0.9942238,0.002759714,0.0003589041,0.0006477281,0.001522837,0.0004870874],"domain_scores_gemma":[0.9833144,0.01255581,0.000587453,0.002328981,0.0008613238,0.0003519945],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.00001813905,0.00001259514,0.00005893844,0.00005693583,0.000008541885,0.00002728876,0.0001293455,0.007064868,0.0002110908,0.9861885,0.001446742,0.004777098],"study_design_scores_gemma":[0.00000767664,0.000007681685,0.00004838362,0.00002442021,0.000008795361,0.00002528393,0.00003665006,0.0278808,0.000287531,0.9681088,0.003555422,0.000008375106],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.007241251,0.001515269,0.9277748,0.003723903,0.0002438037,0.00009899466,0.0001927076,0.0005807884,0.0586285],"genre_scores_gemma":[0.4649417,0.003188124,0.4832825,0.002833932,0.001547652,0.0008366585,0.00119724,0.001309398,0.0408629],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.01231737,"threshold_uncertainty_score":0.04120564,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.09338436767244732,"score_gpt":0.2992194355844736,"score_spread":0.2058350679120263,"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."}}