4

I don't know precisely how Bob works, but let's talk about clause learning. Suppose you have a set of variable assignments, $A$, say $x_1 = 0$, $x_2 = 1$, $x_3 = 0$. This is a single clause in disjunctive normal form: $$A = \neg x_1 \wedge x_2 \wedge \neg x_3$$ The negation of this set of assignments is a single clause in conjunctive normal form: $$\neg A = ...


3

You can naively compute ALL-SAT in $2^npoly(n,m)$ time, where $n$ is the number of variables and $m$ is the number of clauses. You clearly need $\Omega(2^n)$ time in the worst case just to write down the assignments (in the case of a tautology). If the strong exponential time hypothesis (SETH) holds, then this is not much harder than SAT itself, so under ...


2

First, you need to figure out the semantics of your language: does divide-by-zero cause the program to abort/halt/throw an exception, or does execution proceed and the divide-by-zero returns a NaN? If it causes the program to halt, then you should not try to represent $\bot$ values. Instead, treat division as a conditional statement, that first tests ...


Only top voted, non community-wiki answers of a minimum length are eligible