{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.005632631,0.00135935,0.001004113,0.001347162,0.0008372555,0.003129838,0.005425903,0.00174488,0.01014645],"category_scores_gemma":[0.01164776,0.001471262,0.00300905,0.001483701,0.002821123,0.006023393,0.005977907,0.006261874,0.002931387],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001106104,"about_ca_system_score_gemma":0.002583317,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00127471,"about_ca_topic_score_gemma":0.003472182,"domain_scores_codex":[0.9957774,0.001796563,0.0005465588,0.000678623,0.0009418523,0.0002590457],"domain_scores_gemma":[0.9901537,0.005761753,0.000700612,0.002248941,0.0009016831,0.0002332141],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0004668375,0.0004396843,0.001570473,0.001213499,0.0002891656,0.0007293801,0.001348723,0.08762851,0.01693781,0.6371303,0.03208942,0.2201563],"study_design_scores_gemma":[0.0002602897,0.0001235857,0.0002255169,0.0001951705,0.0001515134,0.0004703629,0.0001072468,0.6316813,0.02042977,0.2408271,0.1054308,0.0000972986],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.001155218,0.00005973981,0.9908769,0.00021,0.00006294102,0.00009206482,0.0001785748,0.005390166,0.001974456],"genre_scores_gemma":[0.03691198,0.0001646974,0.9575561,0.0004378063,0.00008387263,0.0003315277,0.0008899776,0.001235098,0.002388874],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.01014645,"threshold_uncertainty_score":0.03394324,"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."}}