| 4d7483e | malvi | 24 March 2018, 14:05:25 UTC | enumeration | 24 March 2018, 14:05:25 UTC |
| 32c4fb8 | malvi | 24 March 2018, 13:07:23 UTC | add option to choose enumeration algorithm for circumscription | 24 March 2018, 13:07:23 UTC |
| b283369 | malvi | 24 March 2018, 13:06:59 UTC | minor fix in format | 24 March 2018, 13:06:59 UTC |
| 23ee5b9 | malvi | 24 March 2018, 13:06:26 UTC | minor fix in format | 24 March 2018, 13:06:26 UTC |
| f939a64 | malvi | 24 March 2018, 12:29:21 UTC | enum by BC | 24 March 2018, 12:29:21 UTC |
| 41c5603 | Mario Alviano | 22 June 2017, 08:39:21 UTC | Bug fix: eliminated selector variables in case of at-least-one. | 22 June 2017, 08:39:21 UTC |
| 1834d4e | Mario Alviano | 22 June 2017, 08:27:04 UTC | Implement pmres and kdyn. | 22 June 2017, 08:27:04 UTC |
| 0bdcaa5 | Mario Alviano | 24 May 2017, 17:34:03 UTC | Add budget. Remove satId. | 24 May 2017, 17:34:03 UTC |
| 4dfd444 | Mario Alviano | 24 May 2017, 15:52:33 UTC | Copy clauses of size 1 to other solvers. Add debug version: messages are processed as in the single thread version. | 24 May 2017, 15:52:33 UTC |
| 3208a19 | Mario Alviano | 24 May 2017, 12:53:10 UTC | Restore parse of argv[1]. | 24 May 2017, 12:53:10 UTC |
| c3d12bc | Mario Alviano | 17 May 2017, 17:24:30 UTC | Add Parallel MaxSat. | 17 May 2017, 17:24:30 UTC |
| e31c3b4 | Mario Alviano | 09 March 2017, 10:53:14 UTC | Add source file to create the binary circumscriptino. | 09 March 2017, 10:53:14 UTC |
| aa1285c | Mario Alviano | 08 March 2017, 11:34:30 UTC | minor in enum | 08 March 2017, 11:34:30 UTC |
| a895f97 | Mario Alviano | 08 March 2017, 08:03:00 UTC | Add 2qbf and circumscription. | 08 March 2017, 08:03:00 UTC |
| 768d4fd | Mario Alviano | 08 March 2017, 08:00:10 UTC | Expose some methods of glucose. | 08 March 2017, 08:00:10 UTC |
| 8f9363a | Mario Alviano | 08 March 2017, 07:57:24 UTC | Do not sort soft literals if there is only one of them! | 08 March 2017, 07:57:24 UTC |
| 1782ca5 | Mario Alviano | 08 March 2017, 07:48:15 UTC | Add undirected dep-graph. | 08 March 2017, 07:48:15 UTC |
| 791dc40 | Mario Alviano | 08 September 2016, 12:52:13 UTC | LTL and TGD solvers. | 08 September 2016, 12:52:13 UTC |
| 6a51243 | Mario Alviano | 08 September 2016, 12:50:15 UTC | Add PB-constraints to FairSat. | 08 September 2016, 12:50:15 UTC |
| b4feed7 | Mario Alviano | 21 April 2016, 11:00:01 UTC | Add cache of cores. Add a few other tries: weighted core analysis, reversed stratification, ... | 21 April 2016, 11:00:01 UTC |
| d28579b | Mario Alviano | 31 January 2016, 16:31:14 UTC | Add binaries for fairsat. | 31 January 2016, 16:31:14 UTC |
| 39db5dd | Mario Alviano | 31 January 2016, 16:14:19 UTC | In MaxSAT solver the upperbound indicates that a model was found. | 31 January 2016, 16:14:19 UTC |
| b5a209d | Mario Alviano | 31 January 2016, 16:13:27 UTC | Print model even if interrupted. | 31 January 2016, 16:13:27 UTC |
| 359ee81 | Mario Alviano | 31 January 2016, 15:44:13 UTC | Rise error if reading negative weigths in FairSAT. | 31 January 2016, 15:44:13 UTC |
| b8b9271 | Mario Alviano | 29 January 2016, 17:11:44 UTC | Fix bug with weight functions whose weights sum up to a power of 2. | 29 January 2016, 17:11:44 UTC |
| 8f397df | Mario Alviano | 26 January 2016, 16:29:51 UTC | More fixes on replacing int with int64. | 26 January 2016, 16:29:51 UTC |
| d018659 | Mario Alviano | 26 January 2016, 10:31:31 UTC | Fixing a bug in weight constraints: bound was int, now it is int64_t. | 26 January 2016, 10:31:31 UTC |
| cb3bfe5 | Mario Alviano | 21 October 2015, 20:28:15 UTC | Binary search and progression. | 21 October 2015, 20:28:15 UTC |
| 23ca5fe | Mario Alviano | 19 October 2015, 13:14:11 UTC | Start fair sat solver. | 19 October 2015, 13:14:11 UTC |
| 37263d6 | Mario Alviano | 28 July 2015, 18:09:50 UTC | Fix bug with complementary soft literals of the same weight. | 28 July 2015, 18:09:50 UTC |
| 125b399 | Mario Alviano | 28 July 2015, 17:31:19 UTC | Fix bug with empty set of soft literals. | 28 July 2015, 17:31:19 UTC |
| d6058c0 | Mario Alviano | 27 June 2015, 14:45:28 UTC | Align sizes of cardinality constraints in one-pmres. | 27 June 2015, 14:45:28 UTC |
| 84d22c2 | Mario Alviano | 26 June 2015, 09:54:20 UTC | First check unbounded. | 26 June 2015, 09:54:20 UTC |
| 322bb14 | Mario Alviano | 25 June 2015, 11:03:39 UTC | First check with budget on conflicts. | 25 June 2015, 11:03:39 UTC |
| 049c7a5 | Mario Alviano | 25 June 2015, 10:10:40 UTC | Disable initial check. | 25 June 2015, 10:10:40 UTC |
| e6f5395 | Mario Alviano | 24 June 2015, 10:25:47 UTC | Support multiple binaries. Add maxsat evaluation candidates. | 24 June 2015, 10:25:47 UTC |
| cb65365 | Mario Alviano | 24 June 2015, 07:56:19 UTC | Less budget for subsequents progressions. | 24 June 2015, 07:56:19 UTC |
| f2500f8 | Mario Alviano | 23 June 2015, 17:13:08 UTC | LBD reset in minimize. | 23 June 2015, 17:13:08 UTC |
| 865b8d3 | Mario Alviano | 23 June 2015, 16:25:45 UTC | Disable progression+binary find. Actiave progression minimize. | 23 June 2015, 16:25:45 UTC |
| 45bfd01 | Mario Alviano | 23 June 2015, 15:55:29 UTC | Fix bug with hardening. | 23 June 2015, 15:55:29 UTC |
| c8ff844 | Mario Alviano | 23 June 2015, 10:21:22 UTC | Fix bug with top. Fix bug with hardening. | 23 June 2015, 10:21:22 UTC |
| fcf4a10 | Mario Alviano | 20 June 2015, 16:49:50 UTC | Progression+binary to find cores, caching satisfiable soft literals. Budget in seconds. | 20 June 2015, 16:49:50 UTC |
| 566baeb | Mario Alviano | 20 June 2015, 13:19:16 UTC | Fix but with preprocessing. | 20 June 2015, 13:19:16 UTC |
| 8276bec | Mario Alviano | 20 June 2015, 12:43:31 UTC | At most 60 seconds for each check in progressionBinaryMinimize. Reset sum of lbd and conflictsrestarts during minimization. | 20 June 2015, 12:43:31 UTC |
| 4c17f5e | Mario Alviano | 19 June 2015, 09:57:03 UTC | progression+binary minimization. | 19 June 2015, 09:57:03 UTC |
| b65d7c5 | Mario Alviano | 17 June 2015, 10:23:38 UTC | Fix bug with preprocessing. | 17 June 2015, 10:23:38 UTC |
| 36095ee | Mario Alviano | 15 June 2015, 18:28:42 UTC | Start progression from 1. | 15 June 2015, 18:28:42 UTC |
| 8b488cb | Mario Alviano | 14 June 2015, 09:38:39 UTC | Improve kdyn. | 14 June 2015, 09:38:39 UTC |
| 59f6f9b | Mario Alviano | 14 June 2015, 07:27:41 UTC | Add preprocessing. | 14 June 2015, 07:27:41 UTC |
| 5da5372 | Mario Alviano | 13 June 2015, 09:54:24 UTC | Progression from 4, and only if budget > 0. | 13 June 2015, 09:54:24 UTC |
| 3d79552 | Mario Alviano | 10 June 2015, 09:44:31 UTC | Add budget for minimize. | 10 June 2015, 09:44:31 UTC |
| 0c6b4d0 | Mario Alviano | 08 June 2015, 10:33:23 UTC | Activate minimization. | 08 June 2015, 10:33:23 UTC |
| 3f20697 | Mario Alviano | 06 June 2015, 10:14:30 UTC | Fix bug with disjoint core. | 06 June 2015, 10:14:30 UTC |
| e0b7f54 | Mario Alviano | 06 June 2015, 07:49:47 UTC | Trim inside minimization. | 06 June 2015, 07:49:47 UTC |
| f9ee558 | Mario Alviano | 04 June 2015, 15:52:25 UTC | Add progression based minimization. | 04 June 2015, 15:52:25 UTC |
| e5ec54b | Mario Alviano | 03 June 2015, 07:19:37 UTC | Fix bug with disjoint core in the last stratum. | 03 June 2015, 07:19:37 UTC |
| 5e48e33 | Mario Alviano | 31 May 2015, 16:38:19 UTC | Remove BMO. Apply disjoint cores on a per stratum way. | 31 May 2015, 16:38:19 UTC |
| d811e33 | Mario Alviano | 26 May 2015, 12:08:07 UTC | Disable bmo by default because it is bugged. | 26 May 2015, 12:08:07 UTC |
| 940115d | Mario Alviano | 26 May 2015, 11:08:45 UTC | Still working on aggregates for ASP. Add --maxsat-bmo flag. | 26 May 2015, 11:08:45 UTC |
| 6812c76 | Mario Alviano | 23 May 2015, 19:54:00 UTC | Well-founded propagation. | 23 May 2015, 19:54:00 UTC |
| 3fa079f | Mario Alviano | 14 May 2015, 16:00:46 UTC | Try with a different strategy for kdyn. | 14 May 2015, 16:00:46 UTC |
| 802424f | Mario Alviano | 04 May 2015, 10:08:46 UTC | Use --maxsat-tag to set the minimum split for cores. | 04 May 2015, 10:08:46 UTC |
| 1517c14 | Mario Alviano | 04 May 2015, 08:49:53 UTC | Replace cout with trace in kdyn. | 04 May 2015, 08:49:53 UTC |
| a6b1fee | Mario Alviano | 04 May 2015, 08:43:56 UTC | Fix bug with the previous fix for hardening: a last sat-check is possibly required. Add kdyn strategy for maxsat. | 04 May 2015, 08:43:56 UTC |
| 7736b0f | Mario Alviano | 23 April 2015, 07:59:46 UTC | Still incomplete for ASP. | 23 April 2015, 07:59:46 UTC |
| df39524 | Mario Alviano | 23 April 2015, 07:59:21 UTC | Improve hardening. | 23 April 2015, 07:59:21 UTC |
| 0959e0c | Mario Alviano | 25 March 2015, 18:59:56 UTC | Unfounded set detection. | 25 March 2015, 18:59:56 UTC |
| a0eb948 | Mario Alviano | 24 March 2015, 14:18:41 UTC | Completion. Choice rules. SCCs. | 24 March 2015, 14:18:41 UTC |
| ec6bd58 | Mario Alviano | 23 March 2015, 17:09:12 UTC | Start with ASP. | 23 March 2015, 17:09:12 UTC |
| f2b81ce | Mario Alviano | 18 March 2015, 10:26:19 UTC | Handle clauses of zero weight. | 18 March 2015, 10:26:19 UTC |
| 34d17d7 | Mario Alviano | 24 February 2015, 15:37:57 UTC | Fix bug with instances with no assumption. | 24 February 2015, 15:37:57 UTC |
| e043d27 | Mario Alviano | 23 February 2015, 18:14:20 UTC | Remove soft literals at level zero. | 23 February 2015, 18:14:20 UTC |
| ec726a0 | Mario Alviano | 05 January 2015, 16:57:12 UTC | Change default tag to 16. | 05 January 2015, 16:57:12 UTC |
| f2029f2 | Mario Alviano | 05 January 2015, 16:22:37 UTC | Freeze aux atom in one-pmres. | 05 January 2015, 16:22:37 UTC |
| 91eb2f1 | Mario Alviano | 30 December 2014, 15:17:35 UTC | Replace long with int64_t. | 30 December 2014, 15:17:35 UTC |
| 62bffdb | Mario Alviano | 30 December 2014, 14:51:56 UTC | Fix addEquality(CardinalityConstraint). Add variants of the algorithms for maxsat (not really improving the performance of apino). | 30 December 2014, 14:51:56 UTC |
| ff14920 | Mario Alviano | 22 December 2014, 22:46:56 UTC | Change default value of --maxsat-tag. | 22 December 2014, 22:46:56 UTC |
| 4ed394b | Mario Alviano | 22 December 2014, 20:45:22 UTC | Add one-pmres. Fix bug on pmres (useless conjunction was added for the last 2 variables in the conflict). | 22 December 2014, 20:45:22 UTC |
| bf04f7d | Mario Alviano | 22 December 2014, 15:41:13 UTC | Add pmres-reverse. Enable trim() instead of minimize(). | 22 December 2014, 15:41:13 UTC |
| 1f5e43b | Mario Alviano | 21 December 2014, 21:15:15 UTC | Remove useless flag. | 21 December 2014, 21:15:15 UTC |
| 8aa5753 | Mario Alviano | 21 December 2014, 20:02:36 UTC | Implement native cardinality constraints. | 21 December 2014, 20:02:36 UTC |
| 2e50c6e | Mario Alviano | 21 December 2014, 18:33:35 UTC | Forgot to add the patch to bootstrap. | 21 December 2014, 18:33:35 UTC |
| 6a37b55 | Mario Alviano | 21 December 2014, 18:19:14 UTC | Allow to use both - and -- for flags. | 21 December 2014, 18:19:14 UTC |
| a92c6ed | Mario Alviano | 21 December 2014, 17:39:25 UTC | Add EnumOption to glucose (also fix a bug with BoolOption). | 21 December 2014, 17:39:25 UTC |
| 3c74e6e | Mario Alviano | 21 December 2014, 17:36:55 UTC | Remove gflags. | 21 December 2014, 17:36:55 UTC |
| e8e9536 | Mario Alviano | 21 December 2014, 15:37:52 UTC | Rename aspino::Solver as aspino::AbstractSolver. | 21 December 2014, 15:37:52 UTC |
| 4a0c7be | Mario Alviano | 21 December 2014, 15:34:13 UTC | Rename Minisat namespace into Glucose. | 21 December 2014, 15:34:13 UTC |
| 55ff40c | Mario Alviano | 21 December 2014, 15:31:11 UTC | Copy model whenever a new upperbound is found (to fix a problem due to premature exit in case lb == ub; maybe this should be changed in the future). Add a new minimization strategy working on the other side: start from model and try to extend it as much as possible (disabled). | 21 December 2014, 15:31:11 UTC |
| 2eea419 | Mario Alviano | 21 December 2014, 14:20:27 UTC | Add one with flipped polarities. Add minimization of cores based on conflict restriction. Add preprocessing (disabled). | 21 December 2014, 14:20:27 UTC |
| 30df04b | Mario Alviano | 21 December 2014, 11:44:33 UTC | Print model also if status is different than l_True (it can be a previously stored model). | 21 December 2014, 11:44:33 UTC |
| 7c2f9ee | Mario Alviano | 19 December 2014, 17:11:21 UTC | Add smaller conflicts detected by trim(). | 19 December 2014, 17:11:21 UTC |
| d4aa5a0 | Mario Alviano | 17 December 2014, 15:42:04 UTC | Save one variable. Add fake weightOfPreviousLevel element in case of empty instances. | 17 December 2014, 15:42:04 UTC |
| 6fec542 | Mario Alviano | 17 December 2014, 12:55:43 UTC | Safe exit for gprof. | 17 December 2014, 12:55:43 UTC |
| 31cb002 | Mario Alviano | 16 December 2014, 18:35:24 UTC | Fix bug with analyzeFinal. | 16 December 2014, 18:35:24 UTC |
| 50bdca4 | Mario Alviano | 16 December 2014, 15:22:28 UTC | Add patch. | 16 December 2014, 15:22:28 UTC |
| 4c7b91f | Mario Alviano | 16 December 2014, 15:20:39 UTC | Handle conflicts by WCs directly. | 16 December 2014, 15:20:39 UTC |
| de6cdd6 | Mario Alviano | 16 December 2014, 14:04:45 UTC | Fix bug in analyzeFinal. | 16 December 2014, 14:04:45 UTC |
| 6a4b9c9 | Mario Alviano | 16 December 2014, 13:39:31 UTC | Add patch. | 16 December 2014, 13:39:31 UTC |
| e00a44d | Mario Alviano | 16 December 2014, 13:34:24 UTC | Do not create clauses modeling inferences by WC. | 16 December 2014, 13:34:24 UTC |
| bc171bd | Mario Alviano | 16 December 2014, 10:02:43 UTC | Just use 1 more-reason-clause. | 16 December 2014, 10:02:43 UTC |
