+++
title = "Proper SAT solution"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["2e1c4", "2e1c3a"]
forwardlinks = ["2e1c6"]
zettelid = "2e1c5"
+++

One could also encode the following SAT query, which should be
*unsatisfiable*, in the case where the SAT solver supports simple
arithmetic.

$$(P \rightarrow x = 1) \land (\neg P \land Q \rightarrow x = 2) \land (\neg P\land \neg Q \land R \rightarrow x = 3) \land (\neg P \land \neg Q \land \neg R\rightarrow x = 4) \land (Q \rightarrow x' = 2) \land (\neg Q \land P\rightarrow x' = 1) \land (\neg Q \land \neg P \land R \rightarrow x' = 3) \land(\neg Q \land \neg P \land \neg R \rightarrow x' = 4) \land \neg (x = x') $$

This solution was proposed by George during the group meeting.