How to get the formal model using propositional logic

Question

Input

There are three chairs (1,2,3) in the same row. We need to find a seat for three guests (a,b,c).

Constraints

• The first guest does not want to be seated next to the third one (neither left nor right).

• The first guest does not want to be placed on the leftmost chair.

• The second guest does not want to be seated on the right side of the third.

How would this translate to propositional logic? I have difficulties coming out with a solution because all the models I've seen did not have these constraints that depend on two inputs. The end goal is to solve this problem by using a SAT solver.

Answer 1

For this problem, the simplest approach is to try all $3^3=27$ cases by hand.

If you must use a SAT solver, introduce boolean variables to represent the solution. A natural approach is to let $x_{i,j}$ be true if the $i$th guest sits in the $j$th chair. Now you should be able to take it from here and translate each of those constraints into a boolean formula on those variables. For instance, your first constraint can become the formula $$\neg(x_{1,1} \land x_{3,2}) \land \neg(x_{1,2} \land x_{3,1}) \land \neg(x_{1,2} \land x_{3,1}) \land \neg(x_{1,3} \land x_{3,2}).$$ You should be able to turn that into a formula in CNF form, and to translate the other constraints as well.