(module lprop2cnf mzscheme
(require (prefix srfi1: (lib "1.ss" "srfi"))
(prefix srfi71: (lib "71.ss" "srfi"))
(lib "42.ss" "srfi")
(lib "list.ss")
(lib "file.ss")
(lib "etc.ss")
(lib "contract.ss")
(lib "plt-match.ss")
"cardinality-constraints.scm")
(define (remove-redundant-ops f)
(match f
(`(=> ,op1 ,op2)
`(or (not ,(remove-redundant-ops op1))
,(remove-redundant-ops op2)))
(`(<=> ,op1 ,op2)
(remove-redundant-ops
`(and (=> ,op1 ,op2)
(=> ,op2 ,op1))))
(`(xor ,op1 ,op2) (remove-redundant-ops
`(not (<=> ,op1 ,op2))))
(`(ite ,op1 ,op2 ,op3)
(remove-redundant-ops
`(and (=> ,op1 ,op2)
(=> (not ,op1) ,op3))))
(`(xor ,ops ..3) (remove-redundant-ops
`(and (or ,@ops)
,(apply encode-atmost1/lprop ops))))
(`(am1 ,ops ..2) (remove-redundant-ops (apply encode-atmost1/lprop ops)))
(`(and ,ops ..1)
`(and ,@(map remove-redundant-ops ops)))
(`(or ,ops ..1)
`(or ,@(map remove-redundant-ops ops)))
(`(not ,op)
`(not ,(remove-redundant-ops op)))
((? (λ (a) (or (symbol? a)
(boolean? a))) s)
s)
(_ (error 'remove-redundant-ops "Couldn't find a match for ~a" f))))
(define (lprop->cnf formula)
(let ([var-hash (make-hash-table)] [clause-hash (make-hash-table 'equal)] [code-hash (make-hash-table 'equal)]) (letrec ([new-code
(let ([avail-code 1])
(λ ()
(begin0
avail-code
(set! avail-code (+ avail-code 1)))))]
[insert-var
(λ (v)
(let ([code (new-code)])
(hash-table-put! var-hash code v)
(hash-table-put! code-hash v code)
code))]
[insert-formula
(λ (f)
(let ([code (new-code)])
(hash-table-put! code-hash f code)
code))]
[get-var-code
(λ (v) (hash-table-get code-hash v (λ () (insert-var v))))]
[get-formula-code
(λ (f) (hash-table-get code-hash f (λ () #f)))]
[insert-clauses (λ (f . clauses)
(for-each (λ (c) (hash-table-put! clause-hash (sort c <) f)) clauses)
clauses)])
(apply values
var-hash
clause-hash
(let-values ([(top-level-code top-level-clauses)
(let loop ([f formula])
(match f
(`(and ,ops ..1)
(let ([ids/clauses (map (λ (op) (srfi71:values->list (loop op))) ops)])
(let* ([ids (sort! (map car ids/clauses) <)]
[clauses (apply append (map cadr ids/clauses))]
[reuse-code (get-formula-code `(and ,@ids))])
(if reuse-code
(values reuse-code clauses)
(let ([code (insert-formula `(and ,@ids))])
(values code
(append (apply insert-clauses f
(cons (cons code (map (λ (id) (- id)) ids))
(map (λ (id) (list id (- code))) ids)))
clauses)))))))
(`(or ,ops ..1)
(let ([ids/clauses (map (λ (op) (srfi71:values->list (loop op))) ops)])
(let* ([ids (sort! (map car ids/clauses) <)]
[clauses (apply append (map cadr ids/clauses))]
[reuse-code (get-formula-code `(or ,@ids))])
(if reuse-code
(values reuse-code clauses)
(let ([code (insert-formula `(or ,@ids))])
(values code
(append (apply insert-clauses f
(cons (cons (- code) ids)
(map (λ (id) (list (- id) code)) ids)))
clauses)))))))
(`(not ,op)
(let-values ([(id clauses) (loop op)])
(let ([reuse-code (get-formula-code `(not ,id))])
(if reuse-code
(values reuse-code clauses)
(let ([code (insert-formula `(not ,id))])
(values code
(append (insert-clauses f
(list id code)
(list (- id) (- code)))
clauses)))))))
((? (λ (a) (or (symbol? a)
(boolean? a))) s) (values (get-var-code s) '()))
(`(=> ,op1 ,op2)
(let-values ([(id1 clauses1) (loop op1)]
[(id2 clauses2) (loop op2)])
(let ([reuse-code (get-formula-code `(=> ,id1 ,id2))])
(if reuse-code
(values reuse-code (append clauses1 clauses2))
(let ([code (insert-formula `(=> ,id1 ,id2))])
(values code
(append (insert-clauses f
(list (- id1) id2 (- code))
(list id1 code)
(list (- id2) code))
clauses1
clauses2)))))))
(`(<=> ,op1 ,op2)
(let-values ([(id1 clauses1) (loop op1)]
[(id2 clauses2) (loop op2)])
(let* ([sorted-ids (sort (list id1 id2) <)]
[reuse-code (get-formula-code `(<=> ,@sorted-ids))])
(if reuse-code
(values reuse-code (append clauses1 clauses2))
(let ([code (insert-formula `(<=> ,@sorted-ids))])
(values code
(append (insert-clauses f
(list id1 id2 code)
(list id1 (- id2) (- code))
(list (- id1) (- id2) code)
(list (- id1) id2 (- code)))
clauses1
clauses2)))))))
(`(xor ,op1 ,op2)
(let-values ([(id1 clauses1) (loop op1)]
[(id2 clauses2) (loop op2)])
(let* ([sorted-ids (sort (list id1 id2) <)]
[reuse-code (get-formula-code `(<=> ,@sorted-ids))])
(if reuse-code
(values reuse-code (append clauses1 clauses2))
(let ([code (insert-formula `(<=> ,@sorted-ids))])
(values code
(append (insert-clauses f
(list id1 id2 (- code))
(list id1 (- id2) code)
(list (- id1) (- id2) (- code))
(list (- id1) id2 code))
clauses1
clauses2)))))))
(`(ite ,op1 ,op2 ,op3)
(let-values ([(id1 clauses1) (loop op1)]
[(id2 clauses2) (loop op2)]
[(id3 clauses3) (loop op3)])
(let* ([coded-f `(ite ,id1 ,id2 ,id3)]
[reuse-code (get-formula-code coded-f)])
(if reuse-code
(values reuse-code (append clauses1 clauses2 clauses3))
(let ([code (insert-formula coded-f)])
(values code
(append (insert-clauses f
(list id1 id3 (- code))
(list id1 (- id3) code)
(list (- id1) id2 (- code)))
clauses1
clauses2)))))))
(`(am1 ,ops ..2)
(let ([ids/clauses (map (λ (op) (srfi71:values->list (loop op))) ops)])
(let* ([ids (sort! (map car ids/clauses) <)]
[clauses (apply append (map cadr ids/clauses))]
[coded-f `(am1 ,@ids)]
[reuse-code (get-formula-code coded-f)])
(if reuse-code
(values reuse-code clauses)
(let ([aux-vars (build-list (apply encode-atmost1/needed-vars ids) (λ (n) (new-code)))]
[code (insert-formula coded-f)])
(values code
(append (apply insert-clauses f (apply encode-atmost1 aux-vars ids)) clauses)))))))
(`(xor ,ops ..3)
(loop `(and (or ,@ops) (am1 ,@ops))))
(_ (error 'lprop2cnf "Couldn't find a match for ~a" f))))])
(let* ([false-code (get-var-code #f)]
[true-code (get-var-code #t)]
[false-needed (>= top-level-code false-code)]
[true-needed (>= top-level-code true-code)]
[mid-clause-set (if false-needed (cons (list (- false-code)) top-level-clauses) top-level-clauses)]
[final-clause-set (if true-needed (cons (list true-code) mid-clause-set) mid-clause-set)])
(list top-level-code final-clause-set)))))))
(define (output-cnf num-vars clauses path)
(let ([num-clauses (length clauses)])
(call-with-output-file* path
(lambda (fp)
(fprintf fp "p cnf ~a ~a~n" num-vars (+ 1 num-clauses))
(for-each (λ (clause)
(for-each (λ (literal) (fprintf fp "~a " literal)) clause)
(fprintf fp "0~n"))
clauses)
(fprintf fp "~a 0~n" num-vars))
'truncate)))
(provide lprop->cnf output-cnf)
)