{"id":"W2126983591","doi":"10.1145/1057661.1057725","title":"Utilizing don't care states in SAT-based bounded sequential problems","year":2005,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":9,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Bounded function; Boolean satisfiability problem; Model checking; Computer science; Solver; Equivalence (formal languages); Theoretical computer science; Mathematics; Mathematical optimization; Algorithm; Discrete mathematics; Programming language","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.0004139418,0.0001046234,0.0001023414,0.0001326296,0.0000689495,0.0001605969,0.000536242,0.00005435572,0.00003836772],"category_scores_gemma":[0.00003054242,0.00009735755,0.00003411283,0.000359242,0.00003651937,0.000635375,0.00008970048,0.0001175602,0.00005468171],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001859935,"about_ca_system_score_gemma":0.0001084276,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0001814932,"about_ca_topic_score_gemma":0.0006564779,"domain_scores_codex":[0.9988465,0.0001078982,0.0002527183,0.0003018178,0.0002204658,0.0002705793],"domain_scores_gemma":[0.9993547,0.00003678225,0.00006150141,0.0004277894,0.00006818163,0.00005109232],"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.00004055328,0.000295283,0.01048548,0.0002908163,0.00001889298,0.00001465627,0.01964545,0.04544315,0.01418211,0.323718,0.0005231862,0.5853423],"study_design_scores_gemma":[0.0006044421,0.0000690542,0.001963449,0.00003752225,0.000002308197,0.000003272604,0.0004484455,0.9157342,0.06433135,0.002048208,0.01450151,0.0002562056],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.0775931,0.000141191,0.9149219,0.0004745479,0.0002337911,0.0002714486,0.000001487283,0.0002810764,0.006081425],"genre_scores_gemma":[0.4770887,0.000002582785,0.5226025,0.0002097269,0.0000214142,0.00001668759,0.000005449426,0.000004526963,0.00004836541],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.8702911,"threshold_uncertainty_score":0.3970126,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03977499646281055,"score_gpt":0.3085277922968641,"score_spread":0.2687527958340535,"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."}}