{"id":"W1564397736","doi":"10.1007/11814948_6","title":"Minimum Witnesses for Unsatisfiable 2CNFs","year":2006,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":11,"is_retracted":false,"has_abstract":false,"ca_institutions":"Simon Fraser University","funders":"","keywords":"Resolution (logic); Characterization (materials science); Time complexity; Computer science; Combinatorics; Tree (set theory); Graph; Dynamic programming; Discrete mathematics; Mathematics; Algorithm; 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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.002351497,0.0008324835,0.001108151,0.001329532,0.001472037,0.002873664,0.002018211,0.002178298,0.01841483],"category_scores_gemma":[0.01845406,0.001076059,0.001435825,0.001276276,0.001631689,0.006592263,0.003399412,0.003859684,0.001388751],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001542741,"about_ca_system_score_gemma":0.00146687,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001689365,"about_ca_topic_score_gemma":0.004600395,"domain_scores_codex":[0.9976438,0.0003985995,0.0002200593,0.0004686898,0.0009384847,0.0003304591],"domain_scores_gemma":[0.9878154,0.008407206,0.0004490964,0.001747408,0.001240853,0.0003401261],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.00103308,0.0002238845,0.003058297,0.001334456,0.0001475283,0.0008643345,0.001313558,0.0214795,0.01607695,0.7336506,0.02095279,0.199865],"study_design_scores_gemma":[0.0001322453,0.00008335659,0.0008751297,0.0002081733,0.00009008037,0.0004750468,0.0003342233,0.05263622,0.01253525,0.9135988,0.0189822,0.00004928495],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.1917707,0.001290835,0.7341655,0.004237082,0.0008087353,0.0005589938,0.003849708,0.003670918,0.05964765],"genre_scores_gemma":[0.6837462,0.0007844786,0.2886218,0.0006827821,0.0003293849,0.0004837164,0.005168567,0.0009695936,0.01921353],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.01841483,"threshold_uncertainty_score":0.06160372,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0248006996301742,"score_gpt":0.2767819911094897,"score_spread":0.2519812914793155,"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."}}