10:02:10	 From  Max Heller : Too cool for school
10:09:22	 From  christopher : Its underdetermined
10:09:54	 From  christopher : Maybe I should check more carefully, but I think multiple truth values are consistent
10:10:07	 From  Daniel Kostovetsky : Depends on the values of the variables?
10:10:51	 From  Gene Siriviboon : No
10:10:55	 From  Mary Loukidi-Papanikoli : No
10:10:57	 From  christopher : No because we can set X_1=false
10:11:13	 From  Monica Roy : yes
10:11:13	 From  Gene Siriviboon : yes
10:11:15	 From  Koyena Pal : yes
10:11:15	 From  kawam : yes
10:11:24	 From  christopher : x1=true, x2=true, x3=anything
10:11:59	 From  Nicholas Keirstead : Reduces to x1 and x2
10:13:12	 From  Daniel Kostovetsky : Just testing
10:13:31	 From  Phunn Boonchouchouy : Truth table
10:15:03	 From  Neil Ramaswamy : 2^k
10:15:04	 From  Phunn Boonchouchouy : 2^k
10:15:05	 From  mia 🤠 : 2 to the k
10:15:08	 From  christopher : 2^k
10:15:28	 From  christopher : You can prune a lot though
10:18:38	 From  christopher : but you can prune off the 0 path off of x_1 because you know that’s already false
10:20:28	 From  christopher : You could do some optimizations like putting variables that are in singleton clauses at the top
10:21:28	 From  Justin Ly : You can immediately prune any branches where x1 isn’t true
10:21:32	 From  christopher : x_2 because it’s the most frequent?
10:21:38	 From  mlunghi : Remove x3
10:23:27	 From  Danielle Rozenblit : If there are no not x3
10:24:17	 From  Monica Roy : there’s also no not x2
10:28:00	 From  christopher : does that evaluate to true?
10:28:27	 From  christopher : probably true because demorgan’s laws and the empty and
10:28:30	 From  Daniel Kostovetsky : false, I think, because it doesn’t contain any true literals?
10:28:57	 From  Jordan Hartzell : is there an idea of “vacuously” true or false
10:29:05	 From  Gene Siriviboon : False because if we define binary “or” recursively that would be the base case?
10:29:22	 From  christopher : Actually, maybe false is nicer because AND() is maybe more naturally false and OR() could be true
10:29:37	 From  christopher : wait, I meant the other way around
10:30:17	 From  Nicholas Keirstead : False because it’s like adding 0, whereas and would be true because like multiplying by 1 - doesn’t affect the expression
10:30:26	 From  christopher : It is also nicer for it to be false because in every other case, we just need to check if a clause contains a true symbol, and the empty clause doesn’t
10:31:13	 From  Monica Roy : true
10:31:14	 From  Ethan Greenberg : The empty clause would be true
10:31:14	 From  Danielle Rozenblit : True
10:34:05	 From  Monica Roy : if a literal always occurs in the not form, is it also considered a pure literal?
10:37:17	 From  christopher : we can set x_3 any way we want
10:37:28	 From  Daniel Kostovetsky : delete it
10:37:35	 From  christopher : ^
10:38:21	 From  christopher : Just delete the clauses that are already satisfied at each step (like Daniel said), or delete the instances of variables that don’t contribute to satisfaction (like the ~x_1 in clause 2)
10:38:55	 From  kawam : Because we are dealing with CNF right?
10:39:25	 From  Ryan Greenblatt : So we know everything can be represented with CNF?
10:41:35	 From  justin : It feels like any arbitrary assignment has a 50/50 chance of being true on a random Boolean formula, so isn't just guessing a valid strategy?
10:41:51	 From  Thomas Del Vecchio : @Ryan we can convert a truth table to a CNF: each row that produces false into a clause by negating the truth value of each of the inputs.
10:43:30	 From  christopher : Not necessarily @Justin because you could write a formula that is always false
10:43:49	 From  christopher : and in that case you have a 0% chance of getting SAT by guessing randomly
10:46:20	 From  christopher : Don’t you just need the first and the last?
10:46:33	 From  christopher : o nvm
10:47:46	 From  Gene Siriviboon : Should we try to prove satisfiability along with unsatisfiability in case something like this happen?
10:49:48	 From  Daniel Kostovetsky : What language are we using?
10:49:59	 From  Ryan Greenblatt : In forge, the sat solver enumerates all or at least many possibilites if it is SAT. Will our SAT solver do this or just a single valid instance
10:50:00	 From  Charlie Cutting   to   Mark Lavrentyev(Privately) : Yes
10:50:01	 From  Mark Lavrentyev : yep
10:50:04	 From  Ariana Barzinpour : yes that’s correct
10:52:52	 From  Jordan Hartzell : what does it mean for a queen to threaten?
10:54:17	 From  Joanne Han : I think it means that the queen can move to take the other queen. Queens can move
10:54:41	 From  Joanne Han : diagonally, horizontally, or vertically, so if another queen is in its path, it
10:54:43	 From  Joanne Han : can block it
10:56:04	 From  Spencer Dellenbaugh : is there only this one solution?
10:56:19	 From  christopher : There are probably at least 4 because you can rotate the whole board
10:56:25	 From  christopher : so there might be many