{"id":"W1556588790","doi":"10.1007/978-3-642-15396-9_17","title":"Using Learnt Clauses in maxsat","year":2010,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":9,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Toronto","funders":"","keywords":"Maximum satisfiability problem; Soundness; Computer science; Set (abstract data type); Solver; Boolean satisfiability problem; Exploit; Connection (principal bundle); Theoretical computer science; Algorithm; Mathematics; Programming language; Boolean function","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.001455574,0.0009388251,0.0007451739,0.0007327181,0.0005908771,0.002032265,0.002478472,0.0008669622,0.02681718],"category_scores_gemma":[0.007005656,0.0009504429,0.001260797,0.001239837,0.001671525,0.009440498,0.0031339,0.004072953,0.003376993],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001141314,"about_ca_system_score_gemma":0.000751117,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0007244566,"about_ca_topic_score_gemma":0.001818689,"domain_scores_codex":[0.9987687,0.0004610617,0.00007234851,0.0002345695,0.0003730216,0.00009016688],"domain_scores_gemma":[0.9967656,0.002524503,0.00009498194,0.0004157221,0.0001522888,0.00004683067],"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.0002638502,0.0001099438,0.0003606207,0.0006951434,0.00007287678,0.0001211726,0.0002595859,0.04313125,0.002698638,0.6372706,0.01942367,0.2955928],"study_design_scores_gemma":[0.00005234849,0.00002942129,0.00008578273,0.0001024422,0.00003031826,0.000081661,0.00005238115,0.09758695,0.00417803,0.8809904,0.01679164,0.00001859135],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.01662793,0.001156005,0.9334109,0.002160771,0.00038629,0.0001339386,0.0008531695,0.003181088,0.04208996],"genre_scores_gemma":[0.3447601,0.001562258,0.6088853,0.001111842,0.0003891078,0.0003971324,0.002799418,0.00216905,0.03792572],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.02681718,"threshold_uncertainty_score":0.08971238,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05979020646472324,"score_gpt":0.3185460344412531,"score_spread":0.2587558279765299,"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."}}