{"id":"W37002918","doi":"10.1609/aaai.v28i1.9124","title":"Maximum Satisfiability Using Core-Guided MaxSAT Resolution","year":2014,"lang":"en","type":"article","venue":"Proceedings of the AAAI Conference on Artificial Intelligence","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":120,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Maximum satisfiability problem; Boolean satisfiability problem; Solver; Resolution (logic); Satisfiability; Inference; Algorithm; Computer science; Sequence (biology); Core (optical fiber); Mathematics; Mathematical optimization; Artificial intelligence","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.002119896,0.0002289693,0.000272743,0.0001315885,0.0002811775,0.0002102355,0.00219477,0.0001284212,0.000034017],"category_scores_gemma":[0.001806689,0.0001827822,0.0001163435,0.0007912588,0.0004018946,0.0006386976,0.0004651621,0.0003025349,0.00005514144],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001289524,"about_ca_system_score_gemma":0.00008551262,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00007802583,"about_ca_topic_score_gemma":0.000004794153,"domain_scores_codex":[0.9976969,0.00006792978,0.000647489,0.0005929951,0.0006106527,0.000384074],"domain_scores_gemma":[0.9978423,0.000113886,0.0005798216,0.0006407119,0.0007281376,0.00009516995],"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.00002528375,0.00005591902,0.0004470625,0.00003442153,0.000004543465,4.622149e-8,0.0003776648,0.0002262602,0.06215836,0.8781496,0.00005145032,0.05846933],"study_design_scores_gemma":[0.00001456982,0.00008282631,0.000655039,0.00007613478,0.000006152618,0.00000441166,0.000056325,0.4379148,0.2584613,0.302513,0.00008116032,0.0001343113],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.2870281,0.000007614851,0.6999476,0.0009941091,0.0008353591,0.000475969,0.000002495863,0.0001464716,0.01056232],"genre_scores_gemma":[0.7929964,0.000006068021,0.2067365,0.0001338835,0.00006386071,0.00001298248,2.536748e-7,0.000009912519,0.00004013934],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.5756366,"threshold_uncertainty_score":0.7453644,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.2078896805235524,"score_gpt":0.3593631138283615,"score_spread":0.1514734333048091,"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."}}