{"id":"W2403478642","doi":"","title":"Single-Solver Algorithms for 2QBF (Poster Presentation)","year":2012,"lang":"en","type":"article","venue":"Theory and Applications of Satisfiability Testing","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"","keywords":"Solver; Computer science; Boolean satisfiability problem; DPLL algorithm; Algorithm; Heuristic; Set (abstract data type); Satisfiability; Theoretical computer science; Programming language; 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":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.002645841,0.00009112584,0.0001208223,0.00005093918,0.0001714184,0.00003540564,0.0002508448,0.00004452021,0.000007674213],"category_scores_gemma":[0.001253021,0.00008853099,0.00003009638,0.0002642416,0.0001662567,0.0006968494,0.0001191105,0.00005903984,0.000003462498],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00002022204,"about_ca_system_score_gemma":0.00001681747,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000005792852,"about_ca_topic_score_gemma":2.017557e-7,"domain_scores_codex":[0.9989957,0.0001703573,0.0003069691,0.0002282568,0.0001075366,0.0001912392],"domain_scores_gemma":[0.9964233,0.002622175,0.0001787181,0.0005284967,0.0001778868,0.00006941336],"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.000004570951,0.00008322503,0.003829116,0.00006054782,0.000004492226,5.790359e-9,0.0004325039,0.00000798896,0.003734847,0.6203495,0.000004608587,0.3714886],"study_design_scores_gemma":[0.000357064,0.0001312389,0.05117076,0.00003012312,0.00003534873,0.00001684468,0.0002167466,0.006915724,0.04462213,0.8937448,0.002463171,0.0002960217],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.0312944,0.0001231802,0.9662181,0.00006285727,0.00005122062,0.0007240658,0.00001217674,0.00009380792,0.001420217],"genre_scores_gemma":[0.4155883,6.575785e-7,0.5840515,0.00003515738,0.00005886174,0.0002431392,0.000002601813,0.000004518072,0.0000151735],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.3842939,"threshold_uncertainty_score":0.3610189,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.07232481774454069,"score_gpt":0.3347471103248786,"score_spread":0.2624222925803379,"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."}}