{"id":"W4415903173","doi":"10.24963/kr.2025/53","title":"Efficient Volume Computation for SMT Formulas","year":2025,"lang":"","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"Natural Sciences and Engineering Research Council of Canada; Alliance de recherche numérique du Canada; University of Toronto; Innovation, Science and Economic Development Canada","keywords":"Satisfiability modulo theories; Computation; Volume (thermodynamics); Satisfiability; Context (archaeology); Automated reasoning; Set (abstract data type); Modulo; Software; Semiring","routes":{"ca_aff":true,"ca_fund":true,"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.0008917128,0.00128353,0.001514759,0.001933875,0.001072069,0.002790395,0.002197824,0.0009553991,0.008622291],"category_scores_gemma":[0.008457159,0.0006609008,0.002124135,0.002117155,0.001529522,0.004157823,0.003654681,0.001952983,0.001411447],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001742606,"about_ca_system_score_gemma":0.001852124,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003665049,"about_ca_topic_score_gemma":0.006282232,"domain_scores_codex":[0.998253,0.000265855,0.00009352424,0.0002634753,0.0009208127,0.0002032551],"domain_scores_gemma":[0.9969361,0.001873369,0.0002347058,0.0003676622,0.0004843935,0.0001037868],"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.0004819992,0.0001200388,0.002557408,0.0006793967,0.0001096624,0.0003705212,0.0004879438,0.338396,0.0111298,0.2009159,0.01557545,0.4291759],"study_design_scores_gemma":[0.00003202049,0.00003690612,0.0001230967,0.00003088474,0.00001484803,0.00008132183,0.00009348639,0.8834603,0.006438709,0.1064515,0.003223078,0.00001375512],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.02338618,0.0002786112,0.9665143,0.0003030249,0.00006502305,0.00008585393,0.0003546451,0.00382878,0.005183526],"genre_scores_gemma":[0.30496,0.0003047124,0.6871138,0.0002155047,0.00009758498,0.0002669809,0.002025431,0.001568993,0.00344706],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.008622291,"threshold_uncertainty_score":0.02884442,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03070991135187328,"score_gpt":0.3430744459743921,"score_spread":0.3123645346225188,"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."}}