Skip to content

Instantly share code, notes, and snippets.

@emina
Last active Jun 28, 2021
Embed
What would you like to do?
Source code for the Primer on Boolean Satisfiability
c FILE: aim-50-1_6-yes1-4.cnf
c
c SOURCE: Kazuo Iwama, Eiji Miyano (miyano@cscu.kyushu-u.ac.jp),
c and Yuichi Asahiro
c
c DESCRIPTION: Artifical instances from generator by source.
c Generators and more information in
c sat/contributed/iwama.
c
c NOTE: Satisfiable
c
p cnf 50 80
16 17 30 0
-17 22 30 0
-17 -22 30 0
16 -30 47 0
16 -30 -47 0
-16 -21 31 0
-16 -21 -31 0
-16 21 -28 0
-13 21 28 0
13 -16 18 0
13 -18 -38 0
13 -18 -31 0
31 38 44 0
-8 31 -44 0
8 -12 -44 0
8 12 -27 0
12 27 40 0
-4 27 -40 0
12 23 -40 0
-3 4 -23 0
3 -23 -49 0
3 -13 -49 0
-23 -26 49 0
12 -34 49 0
-12 26 -34 0
19 34 36 0
-19 26 36 0
-30 34 -36 0
24 34 -36 0
-24 -36 43 0
6 42 -43 0
-24 42 -43 0
-5 -24 -42 0
5 20 -42 0
5 -7 -20 0
4 7 10 0
-4 10 -20 0
7 -10 -41 0
-10 41 46 0
-33 41 -46 0
33 -37 -46 0
32 33 37 0
6 -32 37 0
-6 25 -32 0
-6 -25 -48 0
-9 28 48 0
-9 -25 -28 0
19 -25 48 0
2 9 -19 0
-2 -19 35 0
-2 22 -35 0
-22 -35 50 0
-17 -35 -50 0
-29 -35 -50 0
-1 29 -50 0
1 11 29 0
-11 17 -45 0
-11 39 45 0
-26 39 45 0
-3 -26 45 0
-11 15 -39 0
14 -15 -39 0
14 -15 -45 0
14 -15 -27 0
-14 -15 47 0
17 17 40 0
1 -29 -31 0
-7 32 38 0
-14 -33 -47 0
-1 2 -8 0
35 43 44 0
21 21 24 0
20 29 -48 0
23 35 -37 0
2 18 -33 0
15 25 -45 0
9 14 -38 0
-5 11 50 0
-3 -13 46 0
-13 -41 43 0
#lang racket
(provide nnf dnf cnf)
; Converts f to NNF by first limiting operators
; to ∧,∨¬ and then pushing ¬ down to the leaves
; (literals) of the formula.
(define (nnf f)
(nnf-neg (nnf-ops f)))
; Converts f to DNF by first converting it to NNF,
; then distributing ∧ over ∨, and finally flattening
; out nested conjunctions and disjunctions.
(define (dnf f)
(unnest (distribute '∧ '∨ (nnf f))))
; Converts f to CNF as done for the DNF conversion but
; swapping ∧ for ∨ and vice versa.
(define (cnf f)
(unnest (distribute '∨ '∧ (nnf f))))
; Returns a formula that is equivalent to f but
; uses only the connectives allowed by NNF: ∧∨¬.
(define (nnf-ops f)
(match f
[`(→ ,(app nnf-ops f1) ,(app nnf-ops f2))
`(∨ (¬ ,f1) ,f2)]
[`(↔ ,(app nnf-ops f1) ,(app nnf-ops f2))
`(∧ (∨ (¬ ,f1) ,f2) (∨ (¬ ,f2) ,f1))]
[`(,op ,fs ...)
`(,op ,@(map nnf-ops fs))]
[_ f]))
; Assuming that f contains only the NNF connectives,
; returns a formula that is equivalent to f but with
; negations (¬) occuring only in literals.
(define (nnf-neg f)
(match f
[`(¬ ⊥) `⊤]
[`(¬ ⊤) `⊥]
[`(¬ ,(? symbol?)) f]
[`(¬ (¬ ,f1)) (nnf-neg f1)]
[`(¬ (∧ ,fs ...))
`(∨ ,@(for/list ([fi fs]) (nnf-neg `(¬ ,fi))))]
[`(¬ (∨ ,fs ...))
`(∧ ,@(for/list ([fi fs]) (nnf-neg `(¬ ,fi))))]
[`(,op ,fs ...)
`(,op ,@(map nnf-neg fs))]
[_ f]))
; Assuming that f is in NNF, distributes ⊗ over ⊕,
; where ⊗, ⊕ ∈ { ∧, ∨ }.
(define (distribute ⊗ ⊕ f)
(match f
[`(,(== ⊗) ,gs ... (,(== ⊕) ,fs ...) ,hs ...)
(distribute ⊗ ⊕
`(,⊕ ,@(for/list ([fi fs]) `(,⊗ ,fi ,@gs ,@hs))))]
[`(,(== ⊕) ,fs ...)
`(,⊕ ,@(for/list ([fi fs]) (distribute ⊗ ⊕ fi)))]
[_ f]))
; Assuming that f is in NNF, transforms it to flatten
; all nested subformulas of the form (∧ ... (∧ ...) ...)
; and (∨ ... (∨ ...) ...).
(define (unnest f)
(match f
[`(∨ ,gs ... (∨ ,fs ...) ,hs ...)
(unnest `(∨ ,@gs ,@fs ,@hs))]
[`(∧ ,gs ... (∧ ,fs ...) ,hs ...)
(unnest `(∧ ,@gs ,@fs ,@hs))]
[`(,op ,fs ...)
`(,op ,@(map unnest fs))]
[_ f]))
#lang racket
(provide (all-defined-out))
; We represent interpretations using immutable hashes
; and define the following operations on them:
; * (assign x0 v0 x1 v1 ...) creates an interpretation
; that assigns the value vi to the variable xi.
; * (lookup I xi) returns the value of the variable xi.
; * (extends I xi vi) returns a new interpretation that
; is like I, except that it binds xi to vi.
(define assign hash)
(define lookup hash-ref)
(define extend hash-set)
; Returns true (#t) if I ⊨ f and false (#f) if I ⊭ f.
(define (evaluate f I)
(match f
['⊤ true]
['⊥ false]
[(? symbol? xi) (lookup I xi)]
[`(¬ ,f1) (not (evaluate f1 I))]
[`(∧ ,fs ...) (for/and ([fi fs]) (evaluate fi I))]
[`(∨ ,fs ...) (for/or ([fi fs]) (evaluate fi I))]
[`(→ ,f1 ,f2) (or (not (evaluate f1 I)) (evaluate f2 I))]
[`(↔ ,f1 ,f2) (equal? (evaluate f1 I) (evaluate f2 I))]))
#lang racket
(provide search-sat dpll read-cnf)
; The procedures search-sat and dpll assume that a CNF formula is
; given as a list of clauses, where each clause is a list of non-zero
; integers representing positive or negative literals.
; If f is satisfiable, returns a model of f given as a list of
; integers (positive or negative literals). Otherwise returns false.
(define (search-sat f)
(let search ([vars (variables f)] [I (list)])
(if (evaluate f I)
I
(match vars
[(list) #f]
[(list v vs ...)
(or (search vs (cons v I))
(search vs (cons (- v) I)))]))))
; If f is satisfiable, returns a model of f given as a list of
; integers (positive or negative literals). Otherwise returns false.
(define (dpll f)
(define g (bcp f))
(match g
[`((,lit) ...) lit] ; model
[`(,_ ... () ,_ ...) #f] ; unsat
[`((,assigned) ... (,lit ,_ ,_ ...) ,_ ...) ; search
(let* ([undecided (drop g (length assigned))]
[result (or (dpll `((,lit) ,@undecided))
(dpll `((,(- lit)) ,@undecided)))])
(and result `(,@assigned ,@result)))]))
; Applies BCP to f.
(define (bcp f)
(match f
[`(,ci ... (,lit) ,cj ...)
`((,lit) ,@(bcp (unit-rule lit `(,@ci ,@cj))))]
[_ f]))
; Applies the unit rule to f with respect to the given literal.
(define (unit-rule lit f)
(define -lit (- lit))
(for/list ([clause f] #:unless (member lit clause))
(match clause
[`(,li ... ,(== -lit) ,lj ...) `(,@li ,@lj)]
[_ clause])))
; Returns the variables in a CNF formula f represented as a
; list of lists of integers.
(define (variables f)
(remove-duplicates (map abs (flatten f))))
; Returns true iff I is a model of the CNF formula f
; represented as a list of lists of integers.
(define (evaluate f I)
(for/and ([c f])
(for/or ([l c] #:when (member l I)) #t)))
; Returns a list of lists representation of a CNF formula
; in the standard DIMACS format.
(define (read-cnf file)
(call-with-input-file file
(lambda (port)
(filter-map
(lambda (ln)
(and (not (string-prefix? ln "c"))
(not (string-prefix? ln "p"))
(map string->number (drop-right (string-split ln) 1))))
(port->lines port)))))
#lang racket
(require "normal-forms.rkt")
(provide tseitin)
; Converts f to an equisatisfiable formula in CNF
; using Tseitin's encoding.
(define (tseitin f)
(cnf (auxiliaries f)))
; Returns a conjunction of formulas of the form
; (∧ a ... (↔ ai fi) ...), where a's are fresh
; auxiliary variables, and fi's are f's subformulas,
; with nested subexpressions replaced by their
; corresponding auxiliary variables.
(define (auxiliaries f)
(define aux (make-hash))
(let intro ([f f])
(and (list? f)
(not (hash-has-key? aux f))
(hash-set! aux f (gensym 'a))
(for-each intro (cdr f))))
`(∧ ,(hash-ref aux f f)
,@(for/list ([fi↦a (sort (hash->list aux) symbol<? #:key cdr)])
(match-define (cons `(,op ,fs ...) a) fi↦a)
`(↔ ,a (,op ,@(for/list ([fj fs]) (hash-ref aux fj fj)))))))
#lang racket
(require "semantics.rkt")
(provide search-valid? deduce-valid?)
; Returns a duplicate-free list of variables that occur in f.
(define (variables f)
(remove-duplicates (remove* '(⊤ ⊥ ¬ ∧ ∨ → ↔) (flatten f))))
; Returns true (#t) if f is valid and false (#f) otherwise,
; by checking that every interpretation satisfies f.
(define (search-valid? f)
(let all-sat? ([vars (variables f)] [I (assign)])
(match vars
[(list)
(evaluate f I)]
[(list v vs ...)
(and (all-sat? vs (extend I v false))
(all-sat? vs (extend I v true)))])))
; Returns true (#t) if f is valid and false (#f) otherwise,
; by checking that all branches of f's proof tree are
; closed (i.e., contain a contradiction).
(define (deduce-valid? f)
(let all-closed? ([facts `((I ⊭ ,f))]) ; assumption
(match facts
[`(,gs ... (I ⊨ (¬ ,f1)) ,hs ...) ; (1)
(all-closed? `((I ⊭ ,f1) ,@gs ,@hs))]
[`(,gs ... (I ⊭ (¬ ,f1)) ,hs ...) ; (2)
(all-closed? `((I ⊨ ,f1) ,@gs ,@hs))]
[`(,gs ... (I ⊨ (∧ ,fs ...)) ,hs ...) ; (3)
(all-closed? `(,@(for/list ([fi fs]) `(I ⊨ ,fi)) ,@gs ,@hs))]
[`(,gs ... (I ⊭ (∧ ,fs ...)) ,hs ...) ; (4)
(for/and ([fi fs])
(all-closed? `((I ⊭ ,fi) ,@gs ,@hs)))]
[`(,gs ... (I ⊨ (∨ ,fs ...)) ,hs ...) ; (5)
(for/and ([fi fs])
(all-closed? `((I ⊨ ,fi) ,@gs ,@hs)))]
[`(,gs ... (I ⊭ (∨ ,fs ...)) ,hs ...) ; (6)
(all-closed? `(,@(for/list ([fi fs]) `(I ⊭ ,fi)) ,@gs ,@hs))]
[`(,gs ... (I ⊨ (→ ,f1 ,f2)) ,hs ...) ; (7)
(and (all-closed? `((I ⊭ ,f1) ,@gs ,@hs))
(all-closed? `((I ⊨ ,f2) ,@gs ,@hs)))]
[`(,gs ... (I ⊭ (→ ,f1 ,f2)) ,hs ...) ; (8)
(all-closed? `((I ⊨ ,f1) (I ⊭ ,f2) ,@gs ,@hs))]
[`(,gs ... (I ⊨ (↔ ,f1 ,f2)) ,hs ...) ; (9)
(and (all-closed? `((I ⊨ (∧ ,f1 ,f2)) ,@gs ,@hs))
(all-closed? `((I ⊭ (∨ ,f1 ,f2)) ,@gs ,@hs)))]
[`(,gs ... (I ⊭ (↔ ,f1 ,f2)) ,hs ...) ; (10)
(and (all-closed? `((I ⊨ (∧ ,f1 (¬ ,f2))) ,@gs ,@hs))
(all-closed? `((I ⊨ (∧ (¬ ,f1) ,f2)) ,@gs ,@hs)))]
[(or `(,_ ... (I ⊨ ,fi) ,_ ... (I ⊭ ,fi) ,_ ...)
`(,_ ... (I ⊭ ,fi) ,_ ... (I ⊨ ,fi) ,_ ...))
(printf "Contradiction on ~a: ~a\n" fi facts)
#t]
[_
(printf "Open branch: ~a\n" facts)
#f])))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment