{"id":"W2018678448","doi":"10.1109/fmcad.2013.6679404","title":"Efficient modular SAT solving for IC3","year":2013,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":22,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"Natural Sciences and Engineering Research Council of Canada; Western Canada Research Grid","keywords":"Computer science; Solver; Modular design; Modulo; Satisfiability modulo theories; Boolean satisfiability problem; Sequence (biology); Parallel computing; Algorithm; Theoretical computer science; Programming language; Mathematics; Discrete mathematics","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.001872954,0.001564545,0.0006689726,0.001035935,0.0007713719,0.001463695,0.002710236,0.0009461066,0.021573],"category_scores_gemma":[0.005480584,0.0008556931,0.002022952,0.001407811,0.001297543,0.002331697,0.0027065,0.002452861,0.004007167],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001753569,"about_ca_system_score_gemma":0.003264554,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.004840512,"about_ca_topic_score_gemma":0.01106208,"domain_scores_codex":[0.9976766,0.0004405839,0.0001572031,0.0004724261,0.0008214363,0.0004318118],"domain_scores_gemma":[0.9962112,0.001633693,0.000260155,0.001126968,0.0006424863,0.000125455],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.001064202,0.0008055617,0.005224002,0.001314506,0.0002771325,0.0007731129,0.000739101,0.2519487,0.09214128,0.1721593,0.03331602,0.4402371],"study_design_scores_gemma":[0.0002622305,0.0002161118,0.000507814,0.00008120987,0.0001050807,0.0002682065,0.0001016315,0.8410777,0.07601549,0.05459383,0.02672128,0.00004939359],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.02890401,0.0001410026,0.9271641,0.0002514931,0.00008070534,0.0003183451,0.0006523028,0.02228608,0.02020193],"genre_scores_gemma":[0.2221227,0.0001002685,0.7688174,0.0003167522,0.00004071818,0.0002410211,0.001795522,0.001896735,0.004668946],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.021573,"threshold_uncertainty_score":0.07216889,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02590236693379281,"score_gpt":0.27647829920258,"score_spread":0.2505759322687872,"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."}}