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


  • 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.


1 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.