corpus.blog
41554 blogs · [ { "id": "01a0bbef-146a-71d1-80ee-6730e4c3a1ac", "title": "Distributed SAT solving is fun", "url": "https://www.msoos.org/2010/12/distributed-sat-solving-is-fun/", "published_at": "2010-12-20T17:45:33+00:00" }, { "id": "01a0bbef-146a-71d1-80ee-6730e58009be", "title": "Hyper-binary resolution: I was wrong, again", "url": "https://www.msoos.org/2010/12/hyper-binary-resolution-i-was-wrong-again/", "published_at": "2010-12-16T19:42:26+00:00" }, { "id": "01a0bbef-146a-71d1-80ee-6730e5c8373e", "title": "Dependent Literals", "url": "https://www.msoos.org/2010/12/dependent-literals/", "published_at": "2010-12-07T22:15:41+00:00" }, { "id": "01a0bbef-146a-71d1-80ee-6730e6a65d9e", "title": "Caching", "url": "https://www.msoos.org/2010/11/caching/", "published_at": "2010-11-23T13:43:50+00:00" }, { "id": "01a0bbef-146a-71d1-80ee-6730e6a77efa", "title": "The Cathedral", "url": "https://www.msoos.org/2010/11/the-cathedral/", "published_at": "2010-11-07T20:09:59+00:00" }, { "id": "01a0bbf2-24c3-7044-abc9-1bb177f6607b", "title": "Implicit binary clauses", "url": "https://www.msoos.org/2010/10/implicit-binary-clauses/", "published_at": "2010-10-27T22:14:57+00:00" }, { "id": "01a0bbf2-24c3-7044-abc9-1bb178ee0d7a", "title": "Wasting cluster time", "url": "https://www.msoos.org/2010/10/wasting-cluster-time/", "published_at": "2010-10-15T21:54:20+00:00" }, { "id": "01a0bbf2-24c3-7044-abc9-1bb17979e37e", "title": "CryptoMiniSat 2.7.1 released", "url": "https://www.msoos.org/2010/10/cryptominisat-2-7-1-released/", "published_at": "2010-10-13T16:46:18+00:00" }, { "id": "01a0bbf2-24c3-7044-abc9-1bb17a419f15", "title": "Configuration management at IRILL days", "url": "https://www.msoos.org/2010/10/configuration-management-at-irill-days/", "published_at": "2010-10-04T16:17:42+00:00" }, { "id": "01a0bbf2-24c3-7044-abc9-1bb17a7a4af6", "title": "Open source software? Free software?", "url": "https://www.msoos.org/2010/09/open-source-software-free-software/", "published_at": "2010-09-30T18:40:27+00:00" }, { "id": "01a0bbf4-facc-7388-90e8-f46d64944e46", "title": "Documenting CryptoMiniSat", "url": "https://www.msoos.org/2010/09/documenting-cryptominisat/", "published_at": "2010-09-29T16:59:36+00:00" }, { "id": "01a0bbf4-facc-7388-90e8-f46d64e29668", "title": "Transitive OTF self-subsuming resolution", "url": "https://www.msoos.org/2010/09/transitive-otf-self-subsuming-resolution/", "published_at": "2010-09-28T16:26:51+00:00" }, { "id": "01a0bbf4-facc-7388-90e8-f46d65dd6bca", "title": "anf2cnf script released", "url": "https://www.msoos.org/2010/09/anf2cnf-script-released/", "published_at": "2010-09-24T15:38:29+00:00" }, { "id": "01a0bbf4-facc-7388-90e8-f46d66807e98", "title": "anf2cnf hell in Sage", "url": "https://www.msoos.org/2010/09/anf2cnf-hell-in-sage/", "published_at": "2010-09-22T23:38:20+00:00" }, { "id": "01a0bbf4-facc-7388-90e8-f46d6721c823", "title": "Reinventing the wheel", "url": "https://www.msoos.org/2010/09/reinventing-the-wheel/", "published_at": "2010-09-18T16:29:45+00:00" }, { "id": "01a0bbf7-e568-73a3-b5fa-5a98664e7746", "title": "FPGA programming and SAT", "url": "https://www.msoos.org/2010/09/fpga-programming-and-sat/", "published_at": "2010-09-13T21:06:08+00:00" }, { "id": "01a0bbf7-e568-73a3-b5fa-5a98666b0c8b", "title": "Creating a SAT solver from scratch", "url": "https://www.msoos.org/2010/09/creating-a-sat-solver-from-scratch/", "published_at": "2010-09-05T16:53:28+00:00" }, { "id": "01a0bbf7-e568-73a3-b5fa-5a9866804e50", "title": "Truth table to ANF conversion", "url": "https://www.msoos.org/2010/09/truth-table-to-anf-conversion/", "published_at": "2010-09-03T14:00:28+00:00" }, { "id": "01a0bbf7-e568-73a3-b5fa-5a9867341a2f", "title": "CryptoMiniSat 2.6.0 released", "url": "https://www.msoos.org/2010/08/cryptominisat-2-6-0-released/", "published_at": "2010-08-30T12:30:10+00:00" }, { "id": "01a0bbf7-e568-73a3-b5fa-5a9867f8580f", "title": "On-the-fly self-subsuming resolution", "url": "https://www.msoos.org/2010/08/on-the-fly-self-subsuming-resolution/", "published_at": "2010-08-15T22:44:16+00:00" }, { "id": "01a0bbfa-ace5-71dc-8bd4-76d94c5f7d2b", "title": "Self-subsuming resolution", "url": "https://www.msoos.org/2010/08/self-subsuming-resolution/", "published_at": "2010-08-04T20:26:00+00:00" }, { "id": "01a0bbfa-ace5-71dc-8bd4-76d94d1c6aef", "title": "Asymmetric branching", "url": "https://www.msoos.org/2010/07/asymmetric-branching/", "published_at": "2010-07-28T11:38:00+00:00" }, { "id": "01a0bbfa-ace5-71dc-8bd4-76d94d46d756", "title": "Propagating faster", "url": "https://www.msoos.org/2010/07/propagating-faster/", "published_at": "2010-07-26T16:13:00+00:00" }, { "id": "01a0bbfa-ace5-71dc-8bd4-76d94d87f1a5", "title": "Stats on CryptoMiniSat’s development", "url": "https://www.msoos.org/2010/07/stats-on-cryptominisats-development/", "published_at": "2010-07-22T15:10:00+00:00" }, { "id": "01a0bbfa-ace5-71dc-8bd4-76d94ddfcf47", "title": "Winning the SAT Race", "url": "https://www.msoos.org/2010/07/winning-the-sat-race/", "published_at": "2010-07-17T18:12:00+00:00" }, { "id": "01a0bbfe-b050-73de-900d-a1df5ef76254", "title": "The 2010 SAT Conference", "url": "https://www.msoos.org/2010/07/the-2010-sat-conference/", "published_at": "2010-07-12T19:04:00+00:00" }, { "id": "01a0bbfe-b050-73de-900d-a1df5fa95336", "title": "ANF to CNF conversion", "url": "https://www.msoos.org/2010/07/anf-to-cnf-conversion/", "published_at": "2010-07-06T10:25:00+00:00" }, { "id": "01a0bbfe-b050-73de-900d-a1df606501ee", "title": "How to bit-stuff pointers", "url": "https://www.msoos.org/2010/06/how-to-bit-stuff-pointers/", "published_at": "2010-06-30T07:22:00+00:00" }, { "id": "01a0bbfe-b050-73de-900d-a1df6140904c", "title": "Propagating binary clauses", "url": "https://www.msoos.org/2010/06/propagating-binary-clauses/", "published_at": "2010-06-27T17:48:00+00:00" }, { "id": "01a0bbfe-b050-73de-900d-a1df61824d68", "title": "Optimisations, take two", "url": "https://www.msoos.org/2010/06/optimisations-take-two/", "published_at": "2010-06-12T19:50:00+00:00" }, { "id": "01a0bc01-4a11-72aa-b93a-3a67f4912caf", "title": "The Obvious Child", "url": "https://www.msoos.org/2010/06/the-obvious-child/", "published_at": "2010-06-08T14:39:00+00:00" }, { "id": "01a0bc01-4a11-72aa-b93a-3a67f4c08826", "title": "Why programs fail", "url": "https://www.msoos.org/2010/05/why-programs-fail/", "published_at": "2010-05-29T18:18:00+00:00" }, { "id": "01a0bc01-4a11-72aa-b93a-3a67f590cdb2", "title": "Being dumb is part of the deal", "url": "https://www.msoos.org/2010/05/being-dumb-is-part-of-the-deal/", "published_at": "2010-05-26T18:36:00+00:00" }, { "id": "01a0bc01-4a11-72aa-b93a-3a67f63b9c9c", "title": "I must be dumb", "url": "https://www.msoos.org/2010/05/i-must-be-dumb/", "published_at": "2010-05-23T17:44:00+00:00" }, { "id": "01a0bc01-4a11-72aa-b93a-3a67f6f97634", "title": "On failed literal probing", "url": "https://www.msoos.org/2010/05/on-failed-literal-probing/", "published_at": "2010-05-17T23:11:00+00:00" }, { "id": "01a0bc03-d8db-70c7-86e9-65b78e558415", "title": "Gaussian elimination is released", "url": "https://www.msoos.org/2010/05/gaussian-elimination-is-released/", "published_at": "2010-05-09T20:33:00+00:00" }, { "id": "01a0bc03-d8db-70c7-86e9-65b78f26df6c", "title": "Parallelisation", "url": "https://www.msoos.org/2010/05/parallelisation/", "published_at": "2010-05-05T09:01:00+00:00" }, { "id": "01a0bc03-d8db-70c7-86e9-65b78f8c1709", "title": "Social coding", "url": "https://www.msoos.org/2010/04/social-coding/", "published_at": "2010-04-29T20:04:00+00:00" }, { "id": "01a0bc03-d8db-70c7-86e9-65b79086b7af", "title": "Blocked clause elimination implies dependent variable removal", "url": "https://www.msoos.org/2010/04/blocked-clause-elimination-implies-dependent-variable-removal/", "published_at": "2010-04-28T20:50:00+00:00" }, { "id": "01a0bc03-d8db-70c7-86e9-65b79128fe73", "title": "CryptoMiniSat v2 finally released", "url": "https://www.msoos.org/2010/04/cryptominisat-v2-finally-released/", "published_at": "2010-04-27T12:49:00+00:00" }, { "id": "01a0bc06-7575-71b0-8eca-3fa0b9b3dd36", "title": "On PrecoSat", "url": "https://www.msoos.org/2010/04/on-precosat/", "published_at": "2010-04-25T19:47:00+00:00" }, { "id": "01a0bc06-7575-71b0-8eca-3fa0b9e9b904", "title": "Optimisations", "url": "https://www.msoos.org/2010/04/optimisations/", "published_at": "2010-04-22T12:10:00+00:00" }, { "id": "01a0bc06-7575-71b0-8eca-3fa0ba950b67", "title": "Tools that I often use", "url": "https://www.msoos.org/2010/04/tools-that-i-use-often/", "published_at": "2010-04-19T20:23:00+00:00" }, { "id": "01a0bc06-7575-71b0-8eca-3fa0bb09999c", "title": "216", "url": "https://www.msoos.org/2010/04/216/", "published_at": "2010-04-17T20:14:00+00:00" }, { "id": "01a0bc06-7575-71b0-8eca-3fa0bb4056ad", "title": "A great essay on security in the cyberworld", "url": "https://www.msoos.org/2010/04/a-great-essay-on-security-in-the-cyberworld/", "published_at": "2010-04-13T19:34:00+00:00" }, { "id": "01a0bc08-d81e-7230-ab67-f4c39315cbd2", "title": "The dates of the SAT Race 2010 have been announced!", "url": "https://www.msoos.org/2010/04/the-dates-of-the-sat-race-2010-have-been-announced/", "published_at": "2010-04-12T10:15:00+00:00" }, { "id": "01a0bc08-d81e-7230-ab67-f4c393eec42a", "title": "On research in general", "url": "https://www.msoos.org/2010/04/on-research-in-general/", "published_at": "2010-04-01T19:29:00+00:00" }, { "id": "01a0bc08-d81e-7230-ab67-f4c394338ab2", "title": "Why CryptoMiniSat can’t use MATLAB to do Gaussian elimination", "url": "https://www.msoos.org/2010/03/why-cryptominisat-cant-use-matlab-to-do-gaussian-elimination/", "published_at": "2010-03-19T14:16:00+00:00" }, { "id": "01a0bc08-d81e-7230-ab67-f4c394704db7", "title": "Could monomials be handled natively from SAT solvers?", "url": "https://www.msoos.org/2010/03/could-monomials-be-handled-natively-from-sat-solvers/", "published_at": "2010-03-17T12:05:00+00:00" }, { "id": "01a0bc08-d81e-7230-ab67-f4c3947fd1b2", "title": "CryptoMiniSat v2", "url": "https://www.msoos.org/2010/03/cryptominisat-v2/", "published_at": "2010-03-04T20:58:00+00:00" }, { "id": "01a0bc0b-2e68-720d-aa08-5a41bdeea26d", "title": "Why do I use Linux?", "url": "https://www.msoos.org/2008/11/why-do-i-use-linux/", "published_at": "2008-11-01T13:11:00+00:00" }, { "id": "01a0bc0b-2e68-720d-aa08-5a41be5c2101", "title": "How to unload the sound module", "url": "https://www.msoos.org/2008/10/how-to-unload-the-sound-module/", "published_at": "2008-10-26T18:02:00+00:00" }, { "id": "01a0bc0b-2e68-720d-aa08-5a41bea9715b", "title": "KDE4 composite with intel drivers", "url": "https://www.msoos.org/2008/09/kde4-composite-with-intel-drivers/", "published_at": "2008-09-20T09:06:00+00:00" }, { "id": "01a0bc0b-2e68-720d-aa08-5a41bf9698a1", "title": "Suspend on Dell D430", "url": "https://www.msoos.org/2008/09/suspend-on-dell-d430/", "published_at": "2008-09-19T18:13:00+00:00" }, { "id": "01a0bc0b-2e68-720d-aa08-5a41bfd94d2c", "title": "Synaptics", "url": "https://www.msoos.org/2008/09/synaptics/", "published_at": "2008-09-12T19:33:00+00:00" } ] posts Claim your blog
Back to msoos.org
Blog · corpus.blog/blogs/msoos.org/posts

msoos.org

msoos.org

2010

Distributed SAT solving is funoriginal ↗
20 Dec 2010
Hyper-binary resolution: I was wrong, againoriginal ↗
16 Dec 2010
Dependent Literalsoriginal ↗
7 Dec 2010
Cachingoriginal ↗
23 Nov 2010
The Cathedraloriginal ↗
7 Nov 2010
Implicit binary clausesoriginal ↗
27 Oct 2010
Wasting cluster timeoriginal ↗
15 Oct 2010
CryptoMiniSat 2.7.1 releasedoriginal ↗
13 Oct 2010
Configuration management at IRILL daysoriginal ↗
4 Oct 2010
Open source software? Free software?original ↗
30 Sept 2010
Documenting CryptoMiniSatoriginal ↗
29 Sept 2010
Transitive OTF self-subsuming resolutionoriginal ↗
28 Sept 2010
anf2cnf script releasedoriginal ↗
24 Sept 2010
anf2cnf hell in Sageoriginal ↗
22 Sept 2010
Reinventing the wheeloriginal ↗
18 Sept 2010
FPGA programming and SAToriginal ↗
13 Sept 2010
Creating a SAT solver from scratchoriginal ↗
5 Sept 2010
Truth table to ANF conversionoriginal ↗
3 Sept 2010
CryptoMiniSat 2.6.0 releasedoriginal ↗
30 Aug 2010
On-the-fly self-subsuming resolutionoriginal ↗
15 Aug 2010
Self-subsuming resolutionoriginal ↗
4 Aug 2010
Asymmetric branchingoriginal ↗
28 Jul 2010
Propagating fasteroriginal ↗
26 Jul 2010
Stats on CryptoMiniSat’s developmentoriginal ↗
22 Jul 2010
Winning the SAT Raceoriginal ↗
17 Jul 2010
The 2010 SAT Conferenceoriginal ↗
12 Jul 2010
ANF to CNF conversionoriginal ↗
6 Jul 2010
How to bit-stuff pointersoriginal ↗
30 Jun 2010
Propagating binary clausesoriginal ↗
27 Jun 2010
Optimisations, take twooriginal ↗
12 Jun 2010
The Obvious Childoriginal ↗
8 Jun 2010
Why programs failoriginal ↗
29 May 2010
Being dumb is part of the dealoriginal ↗
26 May 2010
I must be dumboriginal ↗
23 May 2010
On failed literal probingoriginal ↗
17 May 2010
Gaussian elimination is releasedoriginal ↗
9 May 2010
Parallelisationoriginal ↗
5 May 2010
Social codingoriginal ↗
29 Apr 2010
Blocked clause elimination implies dependent variable removaloriginal ↗
28 Apr 2010
CryptoMiniSat v2 finally releasedoriginal ↗
27 Apr 2010
On PrecoSatoriginal ↗
25 Apr 2010
Optimisationsoriginal ↗
22 Apr 2010
Tools that I often useoriginal ↗
19 Apr 2010
216original ↗
17 Apr 2010
A great essay on security in the cyberworldoriginal ↗
13 Apr 2010
The dates of the SAT Race 2010 have been announced!original ↗
12 Apr 2010
On research in generaloriginal ↗
1 Apr 2010
Why CryptoMiniSat can’t use MATLAB to do Gaussian eliminationoriginal ↗
19 Mar 2010
Could monomials be handled natively from SAT solvers?original ↗
17 Mar 2010
CryptoMiniSat v2original ↗
4 Mar 2010

2008

Why do I use Linux?original ↗
1 Nov 2008
How to unload the sound moduleoriginal ↗
26 Oct 2008
KDE4 composite with intel driversoriginal ↗
20 Sept 2008
Suspend on Dell D430original ↗
19 Sept 2008
Synapticsoriginal ↗
12 Sept 2008
Previous