{"id":"W4230233658","doi":"10.1109/date.2004.1268858","title":"Managing don't cares in Boolean satisfiability","year":2004,"lang":"en","type":"article","venue":"Proceedings Design, Automation and Test in Europe Conference and Exhibition","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":18,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Satisfiability; Boolean satisfiability problem; Computer science; And-inverter graph; Boolean circuit; Very-large-scale integration; Boolean function; Circuit minimization for Boolean functions; Maximum satisfiability problem; Theoretical computer science; Representation (politics); Process (computing); Boolean expression; Computability; Algorithm; Programming language; Embedded system","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.0008313037,0.0001263459,0.0001299718,0.000228098,0.00008409718,0.0003110927,0.0001474798,0.00005524535,0.000002721751],"category_scores_gemma":[0.0005246273,0.0001280589,0.000008335132,0.0005764927,0.00006871183,0.001471658,0.00007232524,0.0001353888,0.000005205974],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00006206385,"about_ca_system_score_gemma":0.00004667984,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00005611156,"about_ca_topic_score_gemma":0.00001570028,"domain_scores_codex":[0.998975,0.00004286287,0.0002892665,0.00037003,0.0001434448,0.0001794039],"domain_scores_gemma":[0.99954,0.00007281203,0.0001054735,0.00009508109,0.0001333628,0.00005328235],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"observational","study_design_scores_codex":[0.00002525033,0.0001858757,0.05059145,0.0003317359,0.000003184089,0.00001177217,0.01163272,0.0002021859,0.03095718,0.6941797,0.00003455573,0.2118444],"study_design_scores_gemma":[0.001402322,0.0003550357,0.4595636,0.000554258,0.000006621521,0.00006180496,0.000629344,0.3600952,0.02428083,0.1524014,0.0001395032,0.0005101089],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.5071267,0.00007816046,0.4891784,0.0009471032,0.00006934666,0.0004112184,6.144176e-7,0.0002169331,0.001971526],"genre_scores_gemma":[0.8982024,0.0001988189,0.1014272,0.0001155202,0.00001127958,0.00002884029,0.000002097188,0.000005828354,0.000008004326],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.5417783,"threshold_uncertainty_score":0.5222089,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03486099874340715,"score_gpt":0.2634861605072138,"score_spread":0.2286251617638067,"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."}}