{"id":"W986923873","doi":"10.1007/978-3-319-21668-3_5","title":"Using Minimal Correction Sets to More Efficiently Compute Minimal Unsatisfiable Sets","year":2015,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":36,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Toronto","funders":"","keywords":"Satisfiability; Set (abstract data type); Combinatorics; Intersection (aeronautics); Duality (order theory); Discrete mathematics; Computer science; Computation; Algorithm; Mathematics","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.001642884,0.001503588,0.001182641,0.002212165,0.001329524,0.002343498,0.002778759,0.001086178,0.0169415],"category_scores_gemma":[0.01179827,0.001006484,0.002582632,0.001774084,0.001369841,0.00472528,0.003468867,0.003832219,0.002201761],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00239715,"about_ca_system_score_gemma":0.002830961,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003924786,"about_ca_topic_score_gemma":0.01034216,"domain_scores_codex":[0.9976413,0.000389719,0.0001650456,0.0003963758,0.001127912,0.0002796086],"domain_scores_gemma":[0.9927192,0.003933344,0.0002532068,0.001754308,0.001214879,0.00012499],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0006958877,0.000390631,0.002089825,0.0009292445,0.0001675261,0.0003012741,0.0005569757,0.1265184,0.02904522,0.2284362,0.02050373,0.5903651],"study_design_scores_gemma":[0.0001256942,0.0001511071,0.0004993913,0.0001691003,0.000160751,0.0001980017,0.0002394882,0.4845383,0.05594007,0.439269,0.01862554,0.00008357263],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.03680821,0.0002004656,0.94272,0.0005235047,0.000303343,0.000320428,0.0004142385,0.007259367,0.0114505],"genre_scores_gemma":[0.2374727,0.0001514717,0.7489616,0.0003740081,0.0000957076,0.0002204724,0.001775226,0.002309966,0.008638928],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.0169415,"threshold_uncertainty_score":0.0566749,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.06497413392949586,"score_gpt":0.333500299153706,"score_spread":0.2685261652242101,"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."}}