*.toc
*.pdf
*.png
+a[1234].tex
\subsection{SMT format solution}
The formula is easily convertable to SMT format by literal conversion and is
-listed in Listing~\ref{listing:a1.smt}. The maximization is done by
+listed in Listing~\ref{listing:a1.bash}. The maximization is done by
incrementing a special variable called \texttt{<REP>} which is an instantiation
of $n(p)$. When the iteration yields unsat we know that the current number
minus one is the maximum amount of prittles the trucks can carry. The
maximization is done with a bash script shown in Listing~\ref{listing:1.bash}.
-\lstinputlisting[language=bash,
+\lstinputlisting[language=bash,firstline=66,
caption={Iteratively find the largest solution for problem 1},
label={listing:1.bash}]{src/a1.bash}
\begin{table}[H]
\centering
- \begin{tabular}{l|lllll|ll}
- \toprule
- Truck & Nuzzles & Prittles & Skipples & Crottles & Dupples &
- Weight & Pallets\\
- \midrule
- 1 & 0 & 0 & 4 & 2 & 1 & 7100 & 7\\
- 2 & 0 & 3 & 4 & 0 & 1 & 6500 & 8\\
- 3 & 0 & 8 & 0 & 0 & 0 & 6400 & 7\\
- 4 & 0 & 7 & 0 & 0 & 1 & 5700 & 8\\
- 5 & 0 & 0 & 0 & 5 & 1 & 7600 & 6\\
- 6 & 4 & 0 & 0 & 3 & 1 & 7400 & 8\\
- \midrule
- total & 4 & 18 & 8 & 10 & 5 & &\\
- \bottomrule
- \end{tabular}
+\input{a1.tex}
\caption{Solution visualization for problem 1}
\label{tab:s1}
\end{table}
LATEX:=pdflatex
DOCUMENT:=ar
-SOURCES:=$(filter-out preamble.tex,$(shell ls *.tex))
-LISTINGS:=$(shell ls src/*)
-IMAGES:=$(shell ls *.png)
+PROBLEMS:=1 2 3 4
-.SECONDARY: $(addsuffix .fmt,$(DOCUMENT))
+SOURCES:=$(DOCUMENT).tex $(addsuffix .tex,$(PROBLEMS))
+LISTINGS:=$(addprefix src/a,$(addsuffix .bash,$(PROBLEMS)))
+SOLUTIONS:=$(addprefix a,$(addsuffix .tex,$(PROBLEMS)))
+
+.SECONDARY: $(DOCUMENT).fmt $(SOLUTIONS)
+.PHONY: solutions
all: $(DOCUMENT).pdf
-%.pdf: %.tex %.fmt $(SOURCES) $(LISTINGS) $(IMAGES)
- $(LATEX) $(basename $@)
- $(LATEX) $(basename $@)
+%.pdf: %.tex %.fmt $(SOURCES) $(LISTINGS) $(SOLUTIONS)
+ $(LATEX) $(basename $<)
+ $(LATEX) $(basename $<)
-%.fmt: preamble.tex
+%.fmt: pre.tex
$(LATEX) -ini -jobname="$(basename $@)" "&$(LATEX) $<\dump"
+a%.tex: src/a%.bash
+ bash $< $@ >/dev/null
+
clean:
- $(RM) -v $(addprefix $(DOCUMENT).,fmt aux log out toc pdf)
+ $(RM) -v $(addprefix $(DOCUMENT).,fmt aux log out toc pdf) $(SOLUTIONS)
\end{lstlisting}
\newpage
-\lstinputlisting[language=lisp,caption={a1.smt},
- label={listing:a1.smt}]{src/a1.smt}
+\lstinputlisting[language=lisp,caption={a1.bash},
+ label={listing:a1.bash}]{src/a1.bash}
\newpage
\lstinputlisting[language=python,caption={a2.py},
\maketitle
\tableofcontents
+\section{Introduction}
+Implementing all the problems by hand in SMT-Lib format would be too much work
+and therefore all problems have an accompanying bash script that does the
+generation and/or the mini or maximization. The bash scripts all have a
+function defined called \lstinline{generate} with a parameter that will be used
+for mini or maximization. All solving is done on the benchmark system listed in
+Listing~\ref{listing:benchmark}.
+
+\begin{lstlisting}[caption={Benchmark system},label={listing:benchmark}]
+CPU: 3600MHz AMD FX(tm)-4100 Quad-Core Processor
+RAM: 8GB
+
+Yices: 2.4.1
+SMT-Lib: 1.2
+Bash: 4.3.30(1)
+\end{lstlisting}
+
\newpage
\input{1.tex}
+function generate {
+ cat<<GENERATE
+(benchmark a1.smt
+:logic QF_UFLIA
+:extrafuns (
+ (t1p Int) (t1n Int) (t1s Int) (t1c Int) (t1d Int)
+ (t2p Int) (t2n Int) (t2s Int) (t2c Int) (t2d Int)
+ (t3p Int) (t3n Int) (t3s Int) (t3c Int) (t3d Int)
+ (t4p Int) (t4n Int) (t4s Int) (t4c Int) (t4d Int)
+ (t5p Int) (t5n Int) (t5s Int) (t5c Int) (t5d Int)
+ (t6p Int) (t6n Int) (t6s Int) (t6c Int) (t6d Int)
+)
+:formula
+(and
+ (>= t1p 0) (>= t1n 0) (>= t1s 0) (>= t1c 0) (>= t1d 0)
+ (>= t2p 0) (>= t2n 0) (>= t2s 0) (>= t2c 0) (>= t2d 0)
+ (>= t3p 0) (>= t3n 0) (>= t3s 0) (>= t3c 0) (>= t3d 0)
+ (>= t4p 0) (>= t4n 0) (>= t4s 0) (>= t4c 0) (>= t4d 0)
+ (>= t5p 0) (>= t5n 0) (>= t5s 0) (>= t5c 0) (>= t5d 0)
+ (>= t6p 0) (>= t6n 0) (>= t6s 0) (>= t6c 0) (>= t6d 0)
+
+ (<= (+ t1p t1n t1s t1c t1d) 8)
+ (<= (+ t2p t2n t2s t2c t2d) 8)
+ (<= (+ t3p t3n t3s t3c t3d) 8)
+ (<= (+ t4p t4n t4s t4c t4d) 8)
+ (<= (+ t5p t5n t5s t5c t5d) 8)
+ (<= (+ t6p t6n t6s t6c t6d) 8)
+
+ (<= (+ (* t1n 700) (* t1p 800) (* t1s 1000) (* t1c 1500) (* t1d 100)) 7800)
+ (<= (+ (* t2n 700) (* t2p 800) (* t2s 1000) (* t2c 1500) (* t2d 100)) 7800)
+ (<= (+ (* t3n 700) (* t3p 800) (* t3s 1000) (* t3c 1500) (* t3d 100)) 7800)
+ (<= (+ (* t4n 700) (* t4p 800) (* t4s 1000) (* t4c 1500) (* t4d 100)) 7800)
+ (<= (+ (* t5n 700) (* t5p 800) (* t5s 1000) (* t5c 1500) (* t5d 100)) 7800)
+ (<= (+ (* t6n 700) (* t6p 800) (* t6s 1000) (* t6c 1600) (* t6d 100)) 7800)
+
+ (or (= 0 t1p) (= 0 t1c))
+ (or (= 0 t2p) (= 0 t2c))
+ (or (= 0 t3p) (= 0 t3c))
+ (or (= 0 t4p) (= 0 t4c))
+ (or (= 0 t5p) (= 0 t5c))
+ (or (= 0 t6p) (= 0 t6c))
+
+ (<= t1d 1) (<= t2d 1) (<= t3d 1) (<= t4d 1) (<= t5d 1) (<= t6d 1)
+
+ (= t3s 0) (= t4s 0) (= t5s 0) (= t6s 0)
+
+ (= (+ t1n t2n t3n t4n t5n t6n) 4)
+ (= (+ t1s t2s t3s t4s t5s t6s) 8)
+ (= (+ t1c t2c t3c t4c t5c t6c) 10)
+ (= (+ t1d t2d t3d t4d t5d t6d) 5)
+
+ (>= (+ t1p t2p t3p t4p t5p t6p) $1)
+)
+)
+GENERATE
+}
+
i=1
-while [ $(sed "s/<REP>/$i/g" a1.smt | yices-smt) = "sat" ]; do
+while [ $(generate $i | yices-smt) = "sat" ]; do
echo "n(p)=$i is still sat"
i=$((i+1))
done
echo "n(p)=$i is unsat thus maximum n(p)=$((i-1))"
+generate $((i-1)) | yices-smt -m | python3 src/a1.py > $1
--- /dev/null
+#!/usr/bin/env python3
+import sys
+
+trucks = {}
+pallets = {'p': 'Prittles', 'n': 'Nuzzles', 'c': 'Crottles',
+ 's': 'Skipples', 'd': 'Dupples'}
+
+for line in sys.stdin:
+ if line.startswith('(='):
+ truck = line[4]
+ pallet = line[5]
+
+ number = int(line[7:-2])
+ trucks[truck] = trucks.get(truck, {})
+ trucks[truck][pallets[pallet]] = number
+
+print('$\\begin{array}{|l|lllll|}')
+print('\t\\toprule')
+print('\tTruck & {}\\\\'.format(' & '.join(sorted(pallets.values()))))
+print('\t\\midrule')
+for truck in sorted(trucks):
+ print('\t{} & {}\\\\'.format(truck, ' & '.join(
+ str(p[1]) for p in sorted(trucks[truck].items()))))
+print('\t\\midrule')
+print('\tTotal & {}\\\\'.format(' & '.join(
+ str(sum(t[p] for t in trucks.values())) for p in
+ sorted(pallets.values()))))
+print('\t\\bottomrule')
+print('\\end{array}$')
+++ /dev/null
-(benchmark a1.smt
-:logic QF_UFLIA
-:extrafuns (
- (t1p Int) (t1n Int) (t1s Int) (t1c Int) (t1d Int)
- (t2p Int) (t2n Int) (t2s Int) (t2c Int) (t2d Int)
- (t3p Int) (t3n Int) (t3s Int) (t3c Int) (t3d Int)
- (t4p Int) (t4n Int) (t4s Int) (t4c Int) (t4d Int)
- (t5p Int) (t5n Int) (t5s Int) (t5c Int) (t5d Int)
- (t6p Int) (t6n Int) (t6s Int) (t6c Int) (t6d Int)
-)
-:formula
-(and
- (>= t1p 0) (>= t1n 0) (>= t1s 0) (>= t1c 0) (>= t1d 0)
- (>= t2p 0) (>= t2n 0) (>= t2s 0) (>= t2c 0) (>= t2d 0)
- (>= t3p 0) (>= t3n 0) (>= t3s 0) (>= t3c 0) (>= t3d 0)
- (>= t4p 0) (>= t4n 0) (>= t4s 0) (>= t4c 0) (>= t4d 0)
- (>= t5p 0) (>= t5n 0) (>= t5s 0) (>= t5c 0) (>= t5d 0)
- (>= t6p 0) (>= t6n 0) (>= t6s 0) (>= t6c 0) (>= t6d 0)
-
- (<= (+ t1p t1n t1s t1c t1d) 8)
- (<= (+ t2p t2n t2s t2c t2d) 8)
- (<= (+ t3p t3n t3s t3c t3d) 8)
- (<= (+ t4p t4n t4s t4c t4d) 8)
- (<= (+ t5p t5n t5s t5c t5d) 8)
- (<= (+ t6p t6n t6s t6c t6d) 8)
-
- (<= (+ (* t1n 700) (* t1p 800) (* t1s 1000) (* t1c 1500) (* t1d 100)) 7800)
- (<= (+ (* t2n 700) (* t2p 800) (* t2s 1000) (* t2c 1500) (* t2d 100)) 7800)
- (<= (+ (* t3n 700) (* t3p 800) (* t3s 1000) (* t3c 1500) (* t3d 100)) 7800)
- (<= (+ (* t4n 700) (* t4p 800) (* t4s 1000) (* t4c 1500) (* t4d 100)) 7800)
- (<= (+ (* t5n 700) (* t5p 800) (* t5s 1000) (* t5c 1500) (* t5d 100)) 7800)
- (<= (+ (* t6n 700) (* t6p 800) (* t6s 1000) (* t6c 1600) (* t6d 100)) 7800)
-
- (or (= 0 t1p) (= 0 t1c))
- (or (= 0 t2p) (= 0 t2c))
- (or (= 0 t3p) (= 0 t3c))
- (or (= 0 t4p) (= 0 t4c))
- (or (= 0 t5p) (= 0 t5c))
- (or (= 0 t6p) (= 0 t6c))
-
- (<= t1d 1)
- (<= t2d 1)
- (<= t3d 1)
- (<= t4d 1)
- (<= t5d 1)
- (<= t6d 1)
-
- (= t3s 0)
- (= t4s 0)
- (= t5s 0)
- (= t6s 0)
-
- (= (+ t1n t2n t3n t4n t5n t6n) 4)
- (= (+ t1s t2s t3s t4s t5s t6s) 8)
- (= (+ t1c t2c t3c t4c t5c t6c) 10)
- (= (+ t1d t2d t3d t4d t5d t6d) 5)
-
- (>= (+ t1p t2p t3p t4p t5p t6p) <REP>)
-)
-)
repositories / ar1516.git / commitdiff