# Satisfier-Falsifier games

In a Maker-Breaker game, there is a finite set of elements $$X$$, and a family $$F$$ of subsets of $$X$$ called the "winning sets". Two players, Maker and Breaker, take turns picking untaken elements from $$X$$. Maker wins by holding a full winning-set while Breaker wins by holding at least one element in each winning-set.

Consider the following generalization. Instead of the family $$F$$ of winning-sets, we have a family $$F$$ of winning-formulas. Each element of $$F$$ is a logic formula. The game is played by two players, Satisfier and Falsifier. Each player in turn picks an unset variable and sets it to either True or False. The goal of Satisfier is to set variables such that at least one formula is satisfied; the goal of Falsifier is to set variables such that all formulas are unsatisfied.

The Maker-Breaker game is a special case in which each formula in $$F$$ is a conjunction of positive variables. For example, the winning-set $$\{x,y,z\}$$ corresponds to the formula "$$x$$ and $$y$$ and $$z$$". Note that in this special case, Satisfier always prefers to set his picked variables to True and Falsifier always prefers to set his picked variables to False.

Is anything known about the general case?

• There is no point in considering a family of formulas, as you can as well take their disjunction. – Emil Jeřábek Nov 23 '18 at 15:30

This question was bumped to the homepage by Community, it sounded interesting to me so I did a little searching. The only thing I found was the paper

L. Zhao and M. Müller. Game-SAT: A preliminary report. In Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), pages 357-362, Vancouver, Canada, 2004.

which you can find a pdf of in a few places. For example on one of the author's webpage. I could only find this preliminary report and not anything further. According to google a few paper have cited this one, but it seems only as related work and nothing more in this direction that I could find.

They consider what they call the Game-SAT problem of determining who wins assuming perfect play from each player. Reports on some experiments indicating a "phase transition" between being a win for the satisfier and a win for the falsifier are given. The paper also claims the problem has the same complexity as the quantified Boolean formula problem (QBF). However, no reductions are given and it is stated

"We have not found any methods to convert between QBF and Game-SAT without introducing an enormous blow-up of the number of variables and clauses."

It's not going to be as nicely behaved as Maker-Breaker. One of the properties used very often in Maker-Breaker game analysis is that giving either player an extra move can't hurt them. This means strategy stealing applies, and so on.

That monotonicity isn't obviously true in your game; and in fact I think it is likely false for some families $$F$$.

So it is certainly an interesting class of games to study, but it may be that (as for other non-monotone combinatorial games) there isn't going to be much general theory.

• There's no strategy stealing in Maker-Breaker games. – domotorp Dec 2 '18 at 20:37
• True, I'm being stupid.. what I should have written is that one can analyse random play (and variants) in a sensible way, because if Maker randomly selects an already-chosen element we can simply pretend she loses her turn. I'm not sure how that came out as 'strategy-stealing'..! In any case, I stick to the main message that I think this class of games won't have a nice general theory in the way Maker-Breaker does. – user36212 Dec 3 '18 at 20:56
• I'm not so sure. I could even imagine that for every such game there's a simple algorithm that converts it into an equivalent Maker-Breaker game. (Note that the conversion would need to take of your 'extra moves cannot hurt' observation too.) – domotorp Dec 3 '18 at 21:03
• I think I'd have to see such an algorithm to believe it. Just to give a simple example, take (a or b) and (not a or not b) as the two winning formulae on a two-element board. If Falsifier starts, Satisfier wins. But the other way round, Falsifier wins (this is of course effectively the pairing strategy). How are you going to convert that into Maker-Breaker, where Maker always wins as first player if she wins as second player? – user36212 Dec 4 '18 at 8:54