Boolean SatisfiabilityICS 275Spring 2010Fall 2010Learning Issues• Learning styles– Graph-based or context-based– i-bounded, scope-bounded– Relevance-based• Non-systematic randomized learning• Implies time and space overhead• Applicable to SATFall 2010Comparing with CSP:• Sat can be decided before all variables are assignedComplexity: when is unit propagation complete?....Think Horn clausesBenchmarks• Random• Crafted• IndustrialSAT race 2006SAT race
View Full Document