{"id":"W1496739046","doi":"10.1007/978-3-540-24677-0_56","title":"Systematic versus Non-systematic Methods for Solving Incremental Satisfiability","year":2004,"lang":"en","type":"book","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Regina","funders":"","keywords":"Satisfiability; Computer science; Propositional calculus; Boolean satisfiability problem; Conjunctive normal form; Propositional formula; Completeness (order theory); Set (abstract data type); Approximation algorithm; Mathematical optimization; Theoretical computer science; Algorithm; Mathematics; Propositional variable","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.001918868,0.0005723935,0.0005222069,0.0008025366,0.0003641146,0.0006453971,0.00128419,0.000631927,0.004313864],"category_scores_gemma":[0.007751933,0.000712131,0.001126649,0.0009690607,0.001245745,0.002144247,0.001699948,0.001163277,0.0006407388],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0003745477,"about_ca_system_score_gemma":0.001615106,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0006484409,"about_ca_topic_score_gemma":0.003226283,"domain_scores_codex":[0.9986814,0.0004208107,0.0001211957,0.0001399389,0.000527364,0.0001092731],"domain_scores_gemma":[0.9940284,0.004133447,0.0002291319,0.001207852,0.0003350034,0.00006610273],"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.0002972912,0.000162561,0.001267539,0.001252015,0.0001152182,0.0001268035,0.000580291,0.03192202,0.0167291,0.186842,0.005033851,0.7556714],"study_design_scores_gemma":[0.0003531215,0.0004366023,0.001278478,0.0004076072,0.0004345994,0.0006291068,0.0003949647,0.4001953,0.04129506,0.5206442,0.03384559,0.00008524906],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.009350109,0.0004314891,0.9854188,0.0001277236,0.00003757172,0.0001013036,0.00003767096,0.0009087973,0.003586544],"genre_scores_gemma":[0.1253964,0.0005467503,0.8695605,0.00008621542,0.00003178625,0.0002159874,0.0001506763,0.0002913525,0.003720378],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.004313864,"threshold_uncertainty_score":0.0144313,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03358788017929245,"score_gpt":0.3477794127939009,"score_spread":0.3141915326146085,"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."}}