{"id":"W4399058346","doi":"10.1007/978-3-031-60597-0_12","title":"UNSAT Solver Synthesis via Monte Carlo Forest Search","year":2024,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Distributed and Parallel Computing Systems","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of British Columbia","funders":"","keywords":"Computer science; Solver; Monte Carlo method; Monte Carlo tree search; Problem solver; Algorithm; Computational science; Theoretical computer science; Programming language; Mathematics; Statistics","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.0005345672,0.001350082,0.0009865735,0.0009377846,0.0008200927,0.001344063,0.001402828,0.001588157,0.03826173],"category_scores_gemma":[0.003063889,0.0008225639,0.00115933,0.0009751641,0.0008156197,0.001167793,0.001075325,0.001719643,0.006390869],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0007136223,"about_ca_system_score_gemma":0.00222069,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.004008263,"about_ca_topic_score_gemma":0.01107151,"domain_scores_codex":[0.9995346,0.0001287766,0.00002118309,0.00009230721,0.000144937,0.00007819009],"domain_scores_gemma":[0.9987431,0.0008537061,0.00005504038,0.000149708,0.0001644023,0.00003411586],"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.0002935293,0.0001244151,0.0003769799,0.0002776578,0.00007260116,0.0001369495,0.000065031,0.6857556,0.00461006,0.05427666,0.02132034,0.2326902],"study_design_scores_gemma":[0.00004794871,0.00002763568,0.0000338591,0.00001983372,0.00001499214,0.00002171316,0.00001457554,0.9781213,0.001557427,0.01667521,0.003459103,0.00000641898],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.007937906,0.0002564426,0.9545158,0.0002777403,0.0001813798,0.0001200576,0.0003655509,0.004430855,0.03191426],"genre_scores_gemma":[0.13823,0.0001402458,0.8444475,0.0003210911,0.00007959652,0.0002870636,0.0009562488,0.001511663,0.01402666],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.03826173,"threshold_uncertainty_score":0.1279983,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01878252922314536,"score_gpt":0.2428699387091239,"score_spread":0.2240874094859785,"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."}}