blob: dcfaffd312823d0aba48bf7d60c476e15f545159 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
+++
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.
|
