Newest at the top
| 2026-04-27 20:00:17 +0000 | michalz | (~michalz@185.246.207.203) (Remote host closed the connection) |
| 2026-04-27 20:00:03 +0000 | thenightmail` | (~whoareyou@user/thenightmail) (ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.2)) |
| 2026-04-27 19:59:58 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 244 seconds) |
| 2026-04-27 19:59:35 +0000 | gabriel_sevecek | (~gabriel@92-180-224-71.dynamic.orange.sk) gabriel_sevecek |
| 2026-04-27 19:59:04 +0000 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-04-27 19:58:30 +0000 | gabriel_sevecek | (~gabriel@92-180-224-71.dynamic.orange.sk) (Quit: WeeChat 4.9.0) |
| 2026-04-27 19:57:13 +0000 | wootehfoot | (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
| 2026-04-27 19:55:13 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-04-27 19:54:32 +0000 | tromp | (~textual@2001:1c00:340e:2700:144f:94ac:cf96:df60) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-04-27 19:50:27 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-27 19:48:05 +0000 | r1bilski_ | (~r1bilski@user-31-175-22-58.play-internet.pl) |
| 2026-04-27 19:45:26 +0000 | <davean> | They can be forced into enumeration but they try to avoid it and do only a ... pertial enumeration, not to feed __monty__ |
| 2026-04-27 19:44:57 +0000 | <davean> | Yah and SMT solvers very much try to NOT have to cover all of them |
| 2026-04-27 19:39:44 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-04-27 19:39:03 +0000 | layline-away | (~layline@149.154.26.56) (Quit: ZZZzzz…) |
| 2026-04-27 19:36:55 +0000 | Googulator53 | (~Googulato@78-131-16-66.pool.digikabel.hu) |
| 2026-04-27 19:36:29 +0000 | Googulator53 | (~Googulato@78-131-16-66.pool.digikabel.hu) (Quit: Client closed) |
| 2026-04-27 19:36:23 +0000 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) ezzieyguywuf |
| 2026-04-27 19:35:19 +0000 | layline_ | layline-away |
| 2026-04-27 19:35:04 +0000 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 276 seconds) |
| 2026-04-27 19:34:24 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-27 19:28:51 +0000 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) (Remote host closed the connection) |
| 2026-04-27 19:27:17 +0000 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2026-04-27 19:26:24 +0000 | target_i | (~target_i@user/target-i/x-6023099) (Ping timeout: 255 seconds) |
| 2026-04-27 19:23:14 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-04-27 19:21:56 +0000 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2026-04-27 19:19:01 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-27 19:17:14 +0000 | pavonia | (~user@user/siracusa) siracusa |
| 2026-04-27 19:17:11 +0000 | <int-e> | "enumerate", to me, means covering all possible cases (assignments of variables) |
| 2026-04-27 19:16:29 +0000 | <int-e> | __monty__: that's not a contradiction; your search space (from splitting into cases) can explode long before you exhaust all possibilities (which may even be infinite) |
| 2026-04-27 19:15:15 +0000 | <__monty__> | I may just not be good at using them, causing my observations of their working to skew towards lengthy enumerations : ) |
| 2026-04-27 19:14:14 +0000 | <int-e> | that's my objection |
| 2026-04-27 19:14:06 +0000 | <int-e> | it's just the least important and interesting aspect of these solvers |
| 2026-04-27 19:13:33 +0000 | <__monty__> | I didn't say they were exhaustive. But they do "enumerate" through relevant classes of values, no? |
| 2026-04-27 19:13:29 +0000 | <int-e> | (but keeping learned clauses and information about how fruitful variables are for finding forced inferences (i.e., pruning the search tree early)) |
| 2026-04-27 19:12:36 +0000 | <int-e> | Even modern SAT solvers (which operate with boolean variables, so everything is discrete) are primarily trying to find forced inferences that allow better pruning of the search space, and a good order in which to try variables. They restart a lot (wiping the whole search tree)) |
| 2026-04-27 19:08:33 +0000 | <int-e> | __monty__: Not really. The point of these tools is generally to work symbolically. But there's usually a lot of case splitting, which adds an enumerative flavor, and can degernate into enumerating all possible cases. |
| 2026-04-27 19:08:05 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-04-27 19:05:29 +0000 | r1bilski_ | (~r1bilski@user-31-175-22-58.play-internet.pl) (Ping timeout: 252 seconds) |
| 2026-04-27 19:04:56 +0000 | <__monty__> | Enumerating is pretty much what model checkers do, no? And SMT solvers kinda. |
| 2026-04-27 19:03:48 +0000 | layline-away | layline_ |
| 2026-04-27 19:03:42 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-27 19:02:15 +0000 | layline_ | layline-away |
| 2026-04-27 19:01:56 +0000 | layline-away | layline_ |
| 2026-04-27 19:00:18 +0000 | redshuffle | (~quassel@45.43.70.75) |
| 2026-04-27 19:00:11 +0000 | redshuffle | (~quassel@45.43.70.75) (Remote host closed the connection) |
| 2026-04-27 18:57:07 +0000 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2026-04-27 18:52:12 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-04-27 18:50:03 +0000 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Remote host closed the connection) |
| 2026-04-27 18:49:23 +0000 | jmcantrell_ | jmcantrell |