{"id":"W2814827538","doi":"10.24963/ijcai.2018/723","title":"Reduced Cost Fixing for Maximum Satisfiability","year":2018,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":6,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"Helsingin Yliopisto","keywords":"Maximum satisfiability problem; Boolean satisfiability problem; Satisfiability; Solver; Computer science; Integer programming; Set (abstract data type); Mathematical optimization; Theoretical computer science; Algorithm; Mathematics; Boolean function; 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.001126431,0.00006234049,0.00007294476,0.00003258947,0.00012675,0.00007331112,0.0005072911,0.00003921827,0.00004274489],"category_scores_gemma":[0.0004868886,0.00005519938,0.00003214466,0.0001839809,0.00006916953,0.0003926994,0.0001034166,0.00003764671,0.00006870552],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00004466694,"about_ca_system_score_gemma":0.00003473006,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001336329,"about_ca_topic_score_gemma":0.000005076692,"domain_scores_codex":[0.9992164,0.00006635844,0.0001590271,0.000270493,0.0001042161,0.0001834936],"domain_scores_gemma":[0.9990198,0.0001269916,0.00004967942,0.0006074882,0.0001482193,0.00004784776],"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.0000126855,0.00003154297,0.0004008274,0.00001746332,0.000005244837,1.192989e-7,0.0004780432,0.000003229705,0.01254347,0.4029875,0.003043032,0.5804769],"study_design_scores_gemma":[0.0004168356,0.0002967008,0.01622008,0.00001257172,0.000004496937,0.000007764957,0.0000371297,0.4026819,0.3982025,0.1378554,0.04394816,0.0003164524],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.009922148,0.000003119204,0.9748842,0.000436382,0.000705138,0.0003662382,0.000001184387,0.000181818,0.01349978],"genre_scores_gemma":[0.2317915,3.235039e-7,0.7676248,0.0002120179,0.00009643407,0.00004656229,6.779615e-7,0.000003416412,0.0002242754],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.5801604,"threshold_uncertainty_score":0.2250965,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05785960665417542,"score_gpt":0.3490497924107515,"score_spread":0.2911901857565761,"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."}}