{"id":"W2397288865","doi":"10.29007/28ww","title":"Boosting the Performance of SLS and CDCL Solvers by Preprocessor Tuning","year":2018,"lang":"en","type":"article","venue":"EPiC series in computing","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":6,"is_retracted":false,"has_abstract":true,"ca_institutions":"Artificial Intelligence in Medicine (Canada)","funders":"Deutsche Forschungsgemeinschaft","keywords":"Preprocessor; Solver; Computer science; Boosting (machine learning); Data pre-processing; Algorithm; 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":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.001403327,0.0000909939,0.0001248355,0.00004741632,0.000253915,0.00006299836,0.0005978823,0.00003656383,0.000002821804],"category_scores_gemma":[0.0003577229,0.00007530049,0.00001361015,0.0003738177,0.0002645253,0.0005444863,0.0004212235,0.0001360449,0.000001853635],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00002285939,"about_ca_system_score_gemma":0.00002721513,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001927512,"about_ca_topic_score_gemma":0.000001983713,"domain_scores_codex":[0.9989859,0.00009254442,0.0002943292,0.0002559724,0.0001531842,0.0002180721],"domain_scores_gemma":[0.9991118,0.0002295398,0.0002004623,0.0003623182,0.00007329218,0.00002263668],"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.00006790992,0.00006110483,0.1283091,0.00046184,0.00003542161,0.000002719092,0.06052584,0.001922494,0.02226089,0.03984707,0.0004098581,0.7460957],"study_design_scores_gemma":[0.0001692681,0.0001722367,0.01512221,0.0001767524,0.000002479645,0.00002670467,0.0005180171,0.9229252,0.05941252,0.0004581897,0.0008660395,0.0001503955],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.7999752,0.0001320881,0.1978222,0.0001380634,0.0002987097,0.00009361086,2.436429e-7,0.0000553141,0.001484605],"genre_scores_gemma":[0.7482294,0.000009339074,0.251598,0.00007430284,0.00005349488,0.000001966184,2.447416e-7,0.000004459071,0.00002877887],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.9210027,"threshold_uncertainty_score":0.3070665,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0180842090583107,"score_gpt":0.2764689635167606,"score_spread":0.2583847544584499,"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."}}