{"id":"W1551380792","doi":"10.1007/978-3-642-14186-7_23","title":"Dynamic Scoring Functions with Variable Expressions: New SLS Methods for Solving SAT","year":2010,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":17,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of British Columbia","funders":"","keywords":"Benchmark (surveying); Computer science; Variable (mathematics); Generalization; Satisfiability; Weighting; Selection (genetic algorithm); Algorithm; Software; Theoretical computer science; Artificial intelligence; Mathematics; 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.002834526,0.001344732,0.001220192,0.00159775,0.0008769133,0.001962423,0.003832685,0.001096918,0.01594545],"category_scores_gemma":[0.007414635,0.0008477859,0.001752203,0.002098932,0.002216492,0.004367637,0.003375488,0.003608135,0.003625264],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001436673,"about_ca_system_score_gemma":0.001544907,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00156524,"about_ca_topic_score_gemma":0.003998576,"domain_scores_codex":[0.9977633,0.0009641819,0.0001269601,0.0003032988,0.0006704027,0.0001719943],"domain_scores_gemma":[0.9974461,0.001609261,0.0001028296,0.0004731494,0.000288667,0.0000799705],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0001169551,0.000143112,0.0003804424,0.000318606,0.00006822036,0.00004651923,0.0003394695,0.05194876,0.002079532,0.5632609,0.01324314,0.3680544],"study_design_scores_gemma":[0.0000680868,0.00002595752,0.00009261482,0.00006132837,0.00003597114,0.00003547938,0.00005166302,0.4273014,0.001608584,0.5561659,0.01453278,0.00002018291],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.001649921,0.0001227862,0.9910237,0.0001343681,0.00005739335,0.00004757341,0.00006563998,0.0008936086,0.006005092],"genre_scores_gemma":[0.08636828,0.0003073375,0.8942012,0.0002899837,0.0001514219,0.0004369543,0.0004536641,0.001375209,0.01641591],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.01594545,"threshold_uncertainty_score":0.05334282,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03028256369701329,"score_gpt":0.3246639566711262,"score_spread":0.2943813929741129,"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."}}