(define \$delete-literals (lambda [\$ls \$cnf] (map (lambda [\$c] (match-all [c ls] [(multiset integer) (multiset integer)] [[ !] l])) cnf))) (define \$delete-clauses-with (lambda [\$ls \$cnf] (match-all [ls cnf] [(multiset integer) (multiset (multiset integer))] [{[# ] ![ ]} c]))) (define \$assign-true (lambda [\$l \$cnf] (delete-literals {(neg l)} (delete-clauses-with {l} cnf)))) (define \$resolve-on (lambda [\$v \$cnf] (match-all cnf (multiset (multiset integer)) [{ _>> ![ ]} (unique {@xs @ys})]))) (define \$dp (lambda [\$vars \$cnf] (match [vars cnf] [(multiset integer) (multiset (multiset integer))] {[[_ ] #t] [[_ _>] #f] [[_ > _>] (dp (delete (abs l) vars) (assign-true l cnf))] [[ ! _>] (dp vs (assign-true v cnf))] [[ ! _>] (dp vs (assign-true (neg v) cnf))] [[ _] (dp vs {@(resolve-on v cnf) @(delete-clauses-with {v (neg v)} cnf)})]}))) (dp {1} {{1}}) ; #t (dp {1} {{1} {-1}}) ; #f (dp {1 2 3} {{1 2} {-1 3} {1 -3}}) ; #t (dp {1 2} {{1 2} {-1 -2} {1 -2}}) ; #t (dp {1 2} {{1 2} {-1 -2} {1 -2} {-1 2}}) ; #f (dp {1 2 3 4 5} {{-1 -2 3} {-1 -2 -3} {1 2 3 4} {-4 -2 3} {5 1 2 -3} {-3 1 -5} {1 -2 3 4} {1 -2 -3 5}}) ; #t (dp {1 2} {{-1 -2} {1}}) ; #t