LAC
/
Questionnaire-2024
3
0
Fork 0
Code Issues Pull Requests Projects Releases 9 Wiki Activity
Browse Source

added ass1 examples for satsolver
continuous-integration/drone/push Build is passing
Details
continuous-integration/drone/tag Build is passing
Details

main release_satsolver
sp 2 months ago
parent
c3a0d9000e
commit
4764fb59b4
7 changed files with 444 additions and 1 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      compile
  2. 13
      sat_solvers_dpll/ex1.tex
  3. 120
      sat_solvers_dpll/ex1_sol.tex
  4. 119
      sat_solvers_dpll/ex2_sol.tex
  5. 14
      sat_solvers_dpll/ex3.tex
  6. 168
      sat_solvers_dpll/ex3_sol.tex
  7. 9
      sat_solvers_dpll/sat_solvers_dpll.tex

2
compile
View File

@ -104,7 +104,7 @@ compile_wrapper() {
compile_chapter() {
#for chapter in smtzthree proplogic satsolver ndpred predlogic ndpred smt bdd eqchecking symbenc temporal
for chapter in ndprop
for chapter in satsolver
do
set_chapter "\\chapter${chapter}true"
compile_wrapper "$chapter" "$@"

13
sat_solvers_dpll/ex1.tex
View File

@ -0,0 +1,13 @@
\item \ifassignmentsheet \points{3}
\dpllDescriptionAssignmentSheet
\else \prac
\dpllDescription{negative}
\fi
\begin{dpllCNFInput}
\item $\{a,\neg b, c \}$
\item $\{b,\neg c, d \}$
\item $\{a, \neg b \}$
\item $\{a ,c \}$
\item $\{\neg c, \neg d \}$
\item $\{\neg a, c \}$
\end{dpllCNFInput}

120
sat_solvers_dpll/ex1_sol.tex
View File

@ -0,0 +1,120 @@
\hspace{-0.09cm}\scalebox{0.85}{
\begin{dplltabular}{5}
\dpllStep{1|2|3|4|5}
\dpllDecL{0|1|1|1|1}
\dpllAssi{ - |$\lnot a$|$\lnot a, \lnot b$|$\lnot a, \lnot b, c$|\makecell{$\lnot a, \lnot b, c, $ \\ $\lnot d$}}
\dpllClause{1}{$a, \lnot b, c$}{$a, \lnot b, c$|$\lnot b, c$|\done|\done|\done}
\dpllClause{2}{$b, \lnot c, d$}{$b, \lnot c, d$|$b, \lnot c, d$|$\lnot c, d$|$d$|\conflict}
\dpllClause{3}{$a, \lnot b$}{$a, \lnot b$|$\lnot b$|\done|\done|\done}
\dpllClause{4}{$a, c$}{$a, c$|$c$|$c$|\done|\done}
\dpllClause{5}{$\lnot c, \lnot d$}{$\lnot c, \lnot d$|$\lnot c, \lnot d$|$\lnot c, \lnot d$|$\lnot d$|\done}
\dpllClause{6}{$\lnot a, c$}{$\lnot a, c$|\done|\done|\done|\done}
\dpllBCP{ - |$\lnot b$|$c$|$\lnot d$| - }
\dpllPL{ - | - | - | - | - }
\dpllDeci{$\lnot a$| - | - | - | - }
\end{dplltabular}
}
Conflict in step 5\\
\scalebox{0.75}{
\begin{tikzpicture}[>=latex,line join=bevel,]
\pgfsetlinewidth{1bp}
%%
\pgfsetcolor{black}
% Edge: 1 -> 4
\draw [->] (21.966bp,69.373bp) .. controls (35.227bp,72.53bp) and (58.98bp,78.186bp) .. (86.047bp,84.63bp);
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (54.0bp,87.5bp) node {$$3$$};
% Edge: 1 -> 5
\draw [->] (21.417bp,62.714bp) .. controls (26.77bp,60.427bp) and (33.652bp,57.735bp) .. (40.0bp,56.0bp) .. controls (51.702bp,52.801bp) and (65.111bp,50.597bp) .. (85.949bp,47.957bp);
\draw (54.0bp,63.5bp) node {$$4$$};
% Edge: 3 -> 2
\draw [->] (193.67bp,47.438bp) .. controls (201.41bp,44.585bp) and (212.51bp,40.495bp) .. (231.47bp,33.51bp);
% Edge: 4 -> 3
\draw [->] (107.62bp,83.519bp) .. controls (118.86bp,79.383bp) and (137.97bp,72.139bp) .. (154.0bp,65.0bp) .. controls (157.18bp,63.585bp) and (160.52bp,62.002bp) .. (172.77bp,55.877bp);
\draw (140.0bp,84.5bp) node {$$2$$};
% Edge: 5 -> 3
\draw [->] (108.3bp,47.49bp) .. controls (121.47bp,48.118bp) and (144.58bp,49.218bp) .. (171.88bp,50.518bp);
\draw (140.0bp,57.5bp) node {$$2$$};
% Edge: 5 -> 6
\draw [->] (106.56bp,41.131bp) .. controls (111.96bp,37.593bp) and (119.2bp,33.173bp) .. (126.0bp,30.0bp) .. controls (137.72bp,24.533bp) and (151.47bp,19.844bp) .. (172.24bp,13.608bp);
\draw (140.0bp,37.5bp) node {$$5$$};
% Edge: 6 -> 2
\draw [->] (193.67bp,14.223bp) .. controls (201.24bp,16.746bp) and (212.02bp,20.339bp) .. (231.09bp,26.697bp);
% Node: 1
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (11.0bp,67.0bp) ellipse (11.0bp and 11.0bp);
\draw (11.0bp,67.0bp) node {$\lnot a$};
\end{scope}
% Node: 4
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (97.0bp,87.0bp) ellipse (11.0bp and 11.0bp);
\draw (97.0bp,87.0bp) node {$\lnot b$};
\end{scope}
% Node: 5
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (97.0bp,47.0bp) ellipse (11.0bp and 11.0bp);
\draw (97.0bp,47.0bp) node {$c$};
\end{scope}
% Node: 2
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (242.0bp,30.0bp) ellipse (11.0bp and 11.0bp);
\draw (242.0bp,30.0bp) node {$\bot$};
\end{scope}
% Node: 3
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (183.0bp,51.0bp) ellipse (11.0bp and 11.0bp);
\draw (183.0bp,51.0bp) node {$d$};
\end{scope}
% Node: 6
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (183.0bp,11.0bp) ellipse (11.0bp and 11.0bp);
\draw (183.0bp,11.0bp) node {$\lnot d$};
\end{scope}
%
\end{tikzpicture}
}
\begin{prooftree}
\AxiomC{$2. \; b \lor \lnot c \lor d$}
\AxiomC{$5. \; \lnot c \lor \lnot d$}
\BinaryInfC{$b \lor \lnot c$}
\AxiomC{$3. \; a \lor \lnot b$}
\BinaryInfC{$\lnot c \lor a$}
\AxiomC{$4. \; a \lor c$}
\BinaryInfC{$a$}
\end{prooftree}
\hspace{-0.09cm}\scalebox{0.85}{
\begin{dplltabular}{5}
\dpllStep{6|7|8|9|10}
\dpllDecL{0|0|0|0|0}
\dpllAssi{ - |$a$|$a, c$|$a, c, \lnot d$|\makecell{$a, c, \lnot d, $ \\ $b$}}
\dpllClause{1}{$a, \lnot b, c$}{$a, \lnot b, c$|\done|\done|\done|\done}
\dpllClause{2}{$b, \lnot c, d$}{$b, \lnot c, d$|$b, \lnot c, d$|$b, d$|$b$|\done}
\dpllClause{3}{$a, \lnot b$}{$a, \lnot b$|\done|\done|\done|\done}
\dpllClause{4}{$a, c$}{$a, c$|\done|\done|\done|\done}
\dpllClause{5}{$\lnot c, \lnot d$}{$\lnot c, \lnot d$|$\lnot c, \lnot d$|$\lnot d$|\done|\done}
\dpllClause{6}{$\lnot a, c$}{$\lnot a, c$|$c$|\done|\done|\done}
\dpllClause{7}{$a$}{$a$|\done|\done|\done|\done}
\dpllBCP{$a$|$c$|$\lnot d$|$b$| - }
\dpllPL{ - | - | - | - | - }
\dpllDeci{ - | - | - | - |SAT}
\end{dplltabular}
}

119
sat_solvers_dpll/ex2_sol.tex
View File

@ -0,0 +1,119 @@
\hspace{-0.09cm}\scalebox{0.85}{
\begin{dplltabular}{5}
\dpllStep{1|2|3|4|5}
\dpllDecL{0|1|2|2|2}
\dpllAssi{ - |$\lnot a$|$\lnot a, \lnot b$|$\lnot a, \lnot b, c$|\makecell{$\lnot a, \lnot b, c, $ \\ $\lnot d$}}
\dpllClause{1}{$a, b, c$}{$a, b, c$|$b, c$|$c$|\done|\done}
\dpllClause{2}{$\lnot a, \lnot b, \lnot c$}{$\lnot a, \lnot b, \lnot c$|\done|\done|\done|\done}
\dpllClause{3}{$a, c, \lnot e$}{$a, c, \lnot e$|$c, \lnot e$|$c, \lnot e$|\done|\done}
\dpllClause{4}{$\lnot b, \lnot c, e$}{$\lnot b, \lnot c, e$|$\lnot b, \lnot c, e$|\done|\done|\done}
\dpllClause{5}{$b, e$}{$b, e$|$b, e$|$e$|$e$|$e$}
\dpllClause{6}{$b, \lnot d$}{$b, \lnot d$|$b, \lnot d$|$\lnot d$|$\lnot d$|\done}
\dpllClause{7}{$\lnot c, d$}{$\lnot c, d$|$\lnot c, d$|$\lnot c, d$|$d$|\conflict}
\dpllClause{8}{$\lnot c, e$}{$\lnot c, e$|$\lnot c, e$|$\lnot c, e$|$e$|$e$}
\dpllBCP{ - | - |$c$|$\lnot d$| - }
\dpllPL{ - | - | - | - | - }
\dpllDeci{$\lnot a$|$\lnot b$| - | - | - }
\end{dplltabular}
}
Conflict in step 5\\
\scalebox{0.75}{
\begin{tikzpicture}[>=latex,line join=bevel,]
\pgfsetlinewidth{1bp}
%%
\pgfsetcolor{black}
% Edge: 1 -> 4
\draw [->] (19.683bp,81.526bp) .. controls (24.978bp,77.19bp) and (32.406bp,71.982bp) .. (40.0bp,69.5bp) .. controls (51.392bp,65.776bp) and (64.79bp,65.173bp) .. (85.794bp,66.207bp);
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (54.0bp,77.0bp) node {$$1$$};
% Edge: 1 -> 5
\draw [->] (21.965bp,89.912bp) .. controls (42.831bp,92.87bp) and (91.46bp,99.762bp) .. (129.08bp,105.09bp);
\draw (54.0bp,103.0bp) node {$$6$$};
% Edge: 2 -> 4
\draw [->] (21.909bp,32.194bp) .. controls (33.423bp,34.415bp) and (52.786bp,38.945bp) .. (68.0bp,46.5bp) .. controls (72.163bp,48.567bp) and (76.339bp,51.274bp) .. (88.19bp,60.406bp);
\draw (54.0bp,54.0bp) node {$$1$$};
% Edge: 4 -> 6
\draw [->] (108.3bp,67.5bp) .. controls (121.47bp,67.5bp) and (144.58bp,67.5bp) .. (171.88bp,67.5bp);
\draw (140.0bp,75.0bp) node {$$7$$};
% Edge: 5 -> 3
\draw [->] (150.95bp,104.51bp) .. controls (167.28bp,101.24bp) and (200.03bp,94.694bp) .. (231.09bp,88.483bp);
% Edge: 6 -> 3
\draw [->] (193.67bp,70.723bp) .. controls (201.24bp,73.246bp) and (212.02bp,76.839bp) .. (231.09bp,83.197bp);
% Node: 1
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (11.0bp,88.5bp) ellipse (11.0bp and 11.0bp);
\draw (11.0bp,88.5bp) node {$\lnot b$};
\end{scope}
% Node: 4
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (97.0bp,67.5bp) ellipse (11.0bp and 11.0bp);
\draw (97.0bp,67.5bp) node {$c$};
\end{scope}
% Node: 5
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (140.0bp,106.5bp) ellipse (11.0bp and 11.0bp);
\draw (140.0bp,106.5bp) node {$\lnot d$};
\end{scope}
% Node: 2
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (11.0bp,30.5bp) ellipse (11.0bp and 11.0bp);
\draw (11.0bp,30.5bp) node {$\lnot a$};
\end{scope}
% Node: 3
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (242.0bp,86.5bp) ellipse (11.0bp and 11.0bp);
\draw (242.0bp,86.5bp) node {$\bot$};
\end{scope}
% Node: 6
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (183.0bp,67.5bp) ellipse (11.0bp and 11.0bp);
\draw (183.0bp,67.5bp) node {$d$};
\end{scope}
%
\end{tikzpicture}
}
\begin{prooftree}
\AxiomC{$7. \; \lnot c \lor d$}
\AxiomC{$1. \; a \lor b \lor c$}
\BinaryInfC{$d \lor a \lor b$}
\AxiomC{$6. \; b \lor \lnot d$}
\BinaryInfC{$a \lor b$}
\end{prooftree}
\hspace{-0.09cm}\scalebox{0.85}{
\begin{dplltabular}{5}
\dpllStep{6|7|8|9|10}
\dpllDecL{1|1|1|2|2}
\dpllAssi{$\lnot a$|$\lnot a, b$|$\lnot a, b, d$|\makecell{$\lnot a, b, d, $ \\ $\lnot c$}|\makecell{$\lnot a, b, d, $ \\ $\lnot c, \lnot e$}}
\dpllClause{1}{$a, b, c$}{$b, c$|\done|\done|\done|\done}
\dpllClause{2}{$\lnot a, \lnot b, \lnot c$}{\done|\done|\done|\done|\done}
\dpllClause{3}{$a, c, \lnot e$}{$c, \lnot e$|$c, \lnot e$|$c, \lnot e$|$\lnot e$|\done}
\dpllClause{4}{$\lnot b, \lnot c, e$}{$\lnot b, \lnot c, e$|$\lnot c, e$|$\lnot c, e$|\done|\done}
\dpllClause{5}{$b, e$}{$b, e$|\done|\done|\done|\done}
\dpllClause{6}{$b, \lnot d$}{$b, \lnot d$|\done|\done|\done|\done}
\dpllClause{7}{$\lnot c, d$}{$\lnot c, d$|$\lnot c, d$|\done|\done|\done}
\dpllClause{8}{$\lnot c, e$}{$\lnot c, e$|$\lnot c, e$|$\lnot c, e$|\done|\done}
\dpllClause{9}{$a, b$}{$b$|\done|\done|\done|\done}
\dpllBCP{$b$| - | - |$\lnot e$| - }
\dpllPL{ - |$d$| - | - | - }
\dpllDeci{ - | - |$\lnot c$| - |SAT}
\end{dplltabular}
}

14
sat_solvers_dpll/ex3.tex
View File

@ -0,0 +1,14 @@
\item \ifassignmentsheet \points{3}
\dpllDescriptionAssignmentSheet
\else \prac
\dpllDescription{negative}
\fi
\begin{dpllCNFInput}
\item $\{a, b\}$
\item $\{\neg b, c\}$
\item $\{\neg a, \neg c\}$
\item $\{b, c\}$
\item $\{a, \neg b\}$
\item $\{\neg b, \neg c\}$
\end{dpllCNFInput}

168
sat_solvers_dpll/ex3_sol.tex
View File

@ -0,0 +1,168 @@
\hspace{-0.09cm}\scalebox{0.85}{
\begin{dplltabular}{3}
\dpllStep{1|2|3}
\dpllDecL{0|1|1}
\dpllAssi{ - |$\lnot a$|$\lnot a, \lnot b$}
\dpllClause{1}{$a, b$}{$a, b$|$b$|\conflict}
\dpllClause{2}{$\lnot b, c$}{$\lnot b, c$|$\lnot b, c$|\done}
\dpllClause{3}{$\lnot a, \lnot c$}{$\lnot a, \lnot c$|\done|\done}
\dpllClause{4}{$b, c$}{$b, c$|$b, c$|$c$}
\dpllClause{5}{$a, \lnot b$}{$a, \lnot b$|$\lnot b$|\done}
\dpllClause{6}{$\lnot b, \lnot c$}{$\lnot b, \lnot c$|$\lnot b, \lnot c$|\done}
\dpllBCP{ - |$\lnot b$| - }
\dpllPL{ - | - | - }
\dpllDeci{$\lnot a$| - | - }
\end{dplltabular}
}
Conflict in step 3\\
\scalebox{0.75}{
\begin{tikzpicture}[>=latex,line join=bevel,]
\pgfsetlinewidth{1bp}
%%
\pgfsetcolor{black}
% Edge: 1 -> 3
\draw [->] (21.966bp,33.373bp) .. controls (35.227bp,36.53bp) and (58.98bp,42.186bp) .. (86.047bp,48.63bp);
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (54.0bp,50.5bp) node {$$1$$};
% Edge: 1 -> 4
\draw [->] (21.111bp,26.371bp) .. controls (26.482bp,23.828bp) and (33.482bp,20.828bp) .. (40.0bp,19.0bp) .. controls (51.65bp,15.733bp) and (65.057bp,13.758bp) .. (85.923bp,11.639bp);
\draw (54.0bp,26.5bp) node {$$5$$};
% Edge: 3 -> 2
\draw [->] (107.67bp,47.438bp) .. controls (115.41bp,44.585bp) and (126.51bp,40.495bp) .. (145.47bp,33.51bp);
% Edge: 4 -> 2
\draw [->] (107.67bp,14.223bp) .. controls (115.24bp,16.746bp) and (126.02bp,20.339bp) .. (145.09bp,26.697bp);
% Node: 1
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (11.0bp,31.0bp) ellipse (11.0bp and 11.0bp);
\draw (11.0bp,31.0bp) node {$\lnot a$};
\end{scope}
% Node: 3
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (97.0bp,51.0bp) ellipse (11.0bp and 11.0bp);
\draw (97.0bp,51.0bp) node {$b$};
\end{scope}
% Node: 4
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (97.0bp,11.0bp) ellipse (11.0bp and 11.0bp);
\draw (97.0bp,11.0bp) node {$\lnot b$};
\end{scope}
% Node: 2
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (156.0bp,30.0bp) ellipse (11.0bp and 11.0bp);
\draw (156.0bp,30.0bp) node {$\bot$};
\end{scope}
%
\end{tikzpicture}
}
\begin{prooftree}
\AxiomC{$1. \; a \lor b$}
\AxiomC{$5. \; a \lor \lnot b$}
\BinaryInfC{$a$}
\end{prooftree}
\hspace{-0.09cm}\scalebox{0.85}{
\begin{dplltabular}{4}
\dpllStep{4|5|6|7}
\dpllDecL{0|0|0|0}
\dpllAssi{ - |$a$|$a, \lnot c$|$a, \lnot c, \lnot b$}
\dpllClause{1}{$a, b$}{$a, b$|\done|\done|\done}
\dpllClause{2}{$\lnot b, c$}{$\lnot b, c$|$\lnot b, c$|$\lnot b$|\done}
\dpllClause{3}{$\lnot a, \lnot c$}{$\lnot a, \lnot c$|$\lnot c$|\done|\done}
\dpllClause{4}{$b, c$}{$b, c$|$b, c$|$b$|\conflict}
\dpllClause{5}{$a, \lnot b$}{$a, \lnot b$|\done|\done|\done}
\dpllClause{6}{$\lnot b, \lnot c$}{$\lnot b, \lnot c$|$\lnot b, \lnot c$|\done|\done}
\dpllClause{7}{$a$}{$a$|\done|\done|\done}
\dpllBCP{$a$|$\lnot c$|$\lnot b$| - }
\dpllPL{ - | - | - | - }
\dpllDeci{ - | - | - |UNSAT}
\end{dplltabular}
}
Conflict in step 7\\
\scalebox{0.75}{
\begin{tikzpicture}[>=latex,line join=bevel,]
\pgfsetlinewidth{1bp}
%%
\pgfsetcolor{black}
% Edge: 0 -> 5
\draw [->] (1.0536bp,31.0bp) .. controls (2.5071bp,31.0bp) and (33.188bp,31.0bp) .. (64.696bp,31.0bp);
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (33.0bp,38.5bp) node {$$7$$};
% Edge: 2 -> 1
\draw [->] (258.67bp,47.438bp) .. controls (266.41bp,44.585bp) and (277.51bp,40.495bp) .. (296.47bp,33.51bp);
% Edge: 3 -> 2
\draw [->] (172.97bp,33.373bp) .. controls (186.23bp,36.53bp) and (209.98bp,42.186bp) .. (237.05bp,48.63bp);
\draw (205.0bp,50.5bp) node {$$2$$};
% Edge: 3 -> 4
\draw [->] (172.11bp,26.371bp) .. controls (177.48bp,23.828bp) and (184.48bp,20.828bp) .. (191.0bp,19.0bp) .. controls (202.65bp,15.733bp) and (216.06bp,13.758bp) .. (236.92bp,11.639bp);
\draw (205.0bp,26.5bp) node {$$4$$};
% Edge: 4 -> 1
\draw [->] (258.67bp,14.223bp) .. controls (266.24bp,16.746bp) and (277.02bp,20.339bp) .. (296.09bp,26.697bp);
% Edge: 5 -> 3
\draw [->] (87.3bp,31.0bp) .. controls (100.47bp,31.0bp) and (123.58bp,31.0bp) .. (150.88bp,31.0bp);
\draw (119.0bp,38.5bp) node {$$3$$};
% Node: 5
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (76.0bp,31.0bp) ellipse (11.0bp and 11.0bp);
\draw (76.0bp,31.0bp) node {$a$};
\end{scope}
% Node: 1
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (307.0bp,30.0bp) ellipse (11.0bp and 11.0bp);
\draw (307.0bp,30.0bp) node {$\bot$};
\end{scope}
% Node: 2
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (248.0bp,51.0bp) ellipse (11.0bp and 11.0bp);
\draw (248.0bp,51.0bp) node {$\lnot b$};
\end{scope}
% Node: 3
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (162.0bp,31.0bp) ellipse (11.0bp and 11.0bp);
\draw (162.0bp,31.0bp) node {$\lnot c$};
\end{scope}
% Node: 4
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (248.0bp,11.0bp) ellipse (11.0bp and 11.0bp);
\draw (248.0bp,11.0bp) node {$b$};
\end{scope}
%
\end{tikzpicture}
}
\begin{prooftree}
\AxiomC{$2. \; \lnot b \lor c$}
\AxiomC{$4. \; b \lor c$}
\BinaryInfC{$c$}
\AxiomC{$3. \; \lnot a \lor \lnot c$}
\BinaryInfC{$\lnot a$}
\AxiomC{$7. \; a$}
\BinaryInfC{$\bot$}
\end{prooftree}

9
sat_solvers_dpll/sat_solvers_dpll.tex
View File

@ -329,5 +329,14 @@
\question{sat_solvers_dpll/0056.tex}
{sat_solvers_dpll/0056_sol.tex}
{3cm}
\question{sat_solvers_dpll/ex1.tex}
{sat_solvers_dpll/ex1_sol.tex}
{3cm}
\question{sat_solvers_dpll/4002.tex}
{sat_solvers_dpll/ex2_sol.tex}
{3cm}
\question{sat_solvers_dpll/ex3.tex}
{sat_solvers_dpll/ex3_sol.tex}
{3cm}
\end{questionSection}
Write Preview
Loading…
Cancel
Save