{"id":"W2109577721","doi":"10.5555/968878.969032","title":"Managing don't cares in Boolean satisfiability","year":2004,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":24,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Satisfiability; Boolean satisfiability problem; Computer science; And-inverter graph; Boolean circuit; Boolean function; Very-large-scale integration; Theoretical computer science; Circuit minimization for Boolean functions; Maximum satisfiability problem; Representation (politics); Boolean expression; Process (computing); 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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.004649073,0.00100114,0.001428105,0.001365168,0.002678879,0.003418291,0.002427229,0.002048553,0.007062113],"category_scores_gemma":[0.02644641,0.001122322,0.001434677,0.001352044,0.003271578,0.008484634,0.003021883,0.003222682,0.0007971931],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002141496,"about_ca_system_score_gemma":0.002823448,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003453629,"about_ca_topic_score_gemma":0.007154106,"domain_scores_codex":[0.9946395,0.002100167,0.0003314386,0.0007789636,0.001458536,0.0006914876],"domain_scores_gemma":[0.9782087,0.01711261,0.001117306,0.002013139,0.001226418,0.0003219067],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"not_applicable","study_design_scores_codex":[0.002083129,0.0006430353,0.007678029,0.0008315949,0.0002070894,0.002102972,0.001676633,0.187885,0.01601138,0.3668756,0.01579013,0.3982155],"study_design_scores_gemma":[0.0002596106,0.0003074459,0.0006620875,0.0001698689,0.0001889393,0.0008777393,0.0006833784,0.5384724,0.02889824,0.4158155,0.01355314,0.0001116979],"study_design_candidate":"not_applicable","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.2077285,0.001327407,0.7576084,0.004070788,0.0003281844,0.0004846498,0.0003937435,0.002948252,0.02511012],"genre_scores_gemma":[0.7244889,0.0006119865,0.2651129,0.0009745436,0.00009768755,0.0002721185,0.0005279076,0.0006195829,0.007294266],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.007062113,"threshold_uncertainty_score":0.02458692,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02012541432448371,"score_gpt":0.2869123942921041,"score_spread":0.2667869799676204,"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."}}