Triad encoding (refer to tdoku) Need lit compression? Can implement like candidates? Implement own SAT solver?