{"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":"codex-gemma-dda1882f352a","candidate_categories":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.001857211,0.0004829637,0.0004970751,0.001291802,0.0002046921,0.0005019989,0.003950442,0.0005596248,0.00002380593],"category_scores_gemma":[0.0002545578,0.000465948,0.00009856421,0.0008843023,0.0008298642,0.001001878,0.001419799,0.0017982,0.00004694887],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0004359362,"about_ca_system_score_gemma":0.0005980009,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00006484451,"about_ca_topic_score_gemma":0.000161661,"domain_scores_codex":[0.9961452,0.00007206538,0.0006276926,0.001508799,0.0009366092,0.0007095714],"domain_scores_gemma":[0.9972342,0.0003085647,0.0003353864,0.001798979,0.000180915,0.00014195],"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.000008377938,0.00004507357,0.0002956893,0.00005828331,0.000005730659,0.0001125631,0.001249264,0.03696245,0.005591227,0.1004167,0.000002615733,0.8552521],"study_design_scores_gemma":[0.0002130621,0.00009179922,0.0004819189,0.0003537943,0.000004339191,0.0001295505,1.63008e-7,0.7981243,0.01041536,0.187324,0.002102011,0.0007597708],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.00064487,0.0001990957,0.9928535,0.0002119656,0.003117126,0.0003555742,0.000001588309,0.0001346314,0.002481663],"genre_scores_gemma":[0.02591343,0.00002616783,0.9729525,0.0006402298,0.0003129195,0.000005428623,0.000001306815,0.00003252299,0.0001154982],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.8544923,"threshold_uncertainty_score":0.9997792,"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."}}