{"id":"W1568918982","doi":"10.1007/11527695","title":"Theory and Applications of Satisfiability Testing: 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10-13, 2004, Revised Selected Papers","year":2005,"lang":"en","type":"book","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":false,"ca_institutions":"","funders":"","keywords":"Boolean satisfiability problem; True quantified Boolean formula; Satisfiability; Conjunctive normal form; Maximum satisfiability problem; Mathematics; DPLL algorithm; Boolean data type; Solver; Discrete mathematics; Algorithm; Computer science; Theoretical computer science; Boolean function; Mathematical optimization","routes":{"ca_aff":false,"ca_fund":false,"ca_venue":false,"about_ca":true,"invisible_to_affiliation_only":true},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.003012505,0.001571607,0.001686738,0.003385417,0.001088444,0.005895625,0.002381019,0.001426111,0.02257602],"category_scores_gemma":[0.00638298,0.001689797,0.001050103,0.005110011,0.003865801,0.004444804,0.001708874,0.00340018,0.00490535],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00527732,"about_ca_system_score_gemma":0.005597843,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.01864315,"about_ca_topic_score_gemma":0.02504857,"domain_scores_codex":[0.9979376,0.0004599324,0.0001370481,0.0003381314,0.0009851018,0.0001422751],"domain_scores_gemma":[0.9962218,0.001987912,0.00009493429,0.0004817351,0.001037873,0.0001758678],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"not_applicable","study_design_scores_codex":[0.0001022398,0.00009935629,0.0009758829,0.0008133019,0.00007214757,0.0001109781,0.0002448239,0.0146751,0.001978106,0.2166135,0.2200587,0.5442558],"study_design_scores_gemma":[0.0000523359,0.00008009672,0.001831165,0.0008424391,0.00009722345,0.0005730254,0.0002043535,0.07121189,0.003022399,0.4181809,0.5038416,0.00006247571],"study_design_candidate":"not_applicable","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"other","genre_scores_codex":[0.005782373,0.186058,0.632822,0.01493257,0.007068969,0.0002148856,0.001429175,0.003249063,0.1484431],"genre_scores_gemma":[0.1333581,0.1807737,0.4622201,0.002597841,0.006204701,0.0005184215,0.005838942,0.001910108,0.206578],"genre_candidate":"other","genre_consensus":null,"teacher_disagreement_score":0.02257602,"threshold_uncertainty_score":0.07552433,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01873044341151169,"score_gpt":0.2598583838044706,"score_spread":0.2411279403929589,"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."}}