{"id":"W2466797724","doi":"10.1609/aaai.v30i1.10111","title":"SAT-to-SAT: Declarative Extension of SAT Solvers with New Propagators","year":2016,"lang":"en","type":"article","venue":"Proceedings of the AAAI Conference on Artificial Intelligence","topic":"Logic, Reasoning, and Knowledge","field":"Computer Science","cited_by":8,"is_retracted":false,"has_abstract":true,"ca_institutions":"Simon Fraser University","funders":"Natural Sciences and Engineering Research Council of Canada; Mitacs; Academy of Finland","keywords":"Propagator; Computer science; Solver; Extension (predicate logic); Theoretical computer science; Declarative programming; Programming language; Mathematics; Programming paradigm; Inductive programming","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":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0004422538,0.000298869,0.0003874047,0.0001698791,0.000158956,0.000118176,0.00189162,0.0001031468,0.00005176971],"category_scores_gemma":[0.000652664,0.0001553256,0.0001193016,0.0008141036,0.0003931544,0.0005101144,0.0004619741,0.000180625,0.0002397698],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00007083984,"about_ca_system_score_gemma":0.0003675121,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00005434516,"about_ca_topic_score_gemma":0.00005186508,"domain_scores_codex":[0.9977452,0.00002063065,0.000513066,0.0006800494,0.0006074886,0.0004335295],"domain_scores_gemma":[0.9976023,0.0001402553,0.0004907027,0.0004299827,0.001106129,0.0002306392],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"bench_or_experimental","study_design_scores_codex":[0.0002779316,0.0001726063,0.002728277,0.00003729009,0.00003217396,0.000001181343,0.005210314,0.0000131982,0.2441372,0.6483723,0.000579172,0.09843842],"study_design_scores_gemma":[0.00007978817,0.0008892497,0.001729013,0.0007328895,0.00001852581,0.00000721376,0.0004858882,0.001484821,0.9241857,0.06990049,0.0001814707,0.0003049715],"study_design_candidate":"bench_or_experimental","study_design_consensus":null,"genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.7839294,0.00004639138,0.1968785,0.00541062,0.0005821391,0.001081303,0.000006478891,0.0001654909,0.01189968],"genre_scores_gemma":[0.9934225,0.00002055068,0.005561407,0.0001466827,0.0000672871,0.00001550141,2.125425e-7,0.00001477869,0.0007510732],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.6800485,"threshold_uncertainty_score":0.6333996,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0643844141834685,"score_gpt":0.2730478353290722,"score_spread":0.2086634211456037,"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."}}