Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Updates to delay optimization project. | Alan Mishchenko | 2016-12-29 | 1 | -1/+6 |
| | |||||
* | Bug fix in 'dsat <file.cnf>' when the number of classes in listed incorrectly. | Alan Mishchenko | 2016-12-13 | 2 | -4/+3 |
| | |||||
* | Bug fix in 'dsat <file.cnf>' when the number of classes in listed incorrectly. | Alan Mishchenko | 2016-12-13 | 8 | -110/+138 |
| | |||||
* | xSAT is an experimental SAT Solver based on Glucose v3(see Glucose ↵ | Bruno Schmitt | 2016-12-12 | 13 | -0/+3151 |
| | | | | | | | | | | | | | | copyrights below) and ABC C version of MiniSat (bsat) developed by Niklas Sorensson and modified by Alan Mishchenko. It’s development has reached sufficient maturity to be committed in ABC, but still in a beta state. TODO: * Read compressed CNF files. * Study the use of floating point for variables and clauses activity. * Better documentation. * Improve verbose messages. * Expose parameters for tuning. | ||||
* | Fixes and adjustments for the edge computation flow. | Alan Mishchenko | 2016-07-15 | 1 | -1/+1 |
| | |||||
* | Experiments with edge-based mapping. | Alan Mishchenko | 2016-06-15 | 1 | -2/+3 |
| | |||||
* | Enabling AIGs without structural hashing. | Alan Mishchenko | 2016-05-20 | 1 | -2/+2 |
| | |||||
* | Added switch 'bmc3 -r' to disable periodic restarts in the SAT solver. | Alan Mishchenko | 2016-05-19 | 4 | -1/+4 |
| | |||||
* | Experiments with generating sat assignments. | Alan Mishchenko | 2016-05-15 | 1 | -1/+1 |
| | |||||
* | Experiments with generating sat assignments. | Alan Mishchenko | 2016-05-14 | 2 | -0/+196 |
| | |||||
* | New command 'expand' to expand SOPs against the offset. | Alan Mishchenko | 2016-05-12 | 2 | -0/+175 |
| | |||||
* | This code was accidentally deleted from the SAT solver (effectively ↵ | Alan Mishchenko | 2016-04-30 | 1 | -0/+7 |
| | | | | disabling restarts!) | ||||
* | Improved algo for edge computation. | Alan Mishchenko | 2016-04-23 | 2 | -1/+14 |
| | |||||
* | Adding new implementation of LEXSAT. | Alan Mishchenko | 2016-04-12 | 3 | -1/+75 |
| | |||||
* | Restructing sat_solver_solve() method for pushing/popping assumptions. | Alan Mishchenko | 2016-04-12 | 3 | -151/+153 |
| | |||||
* | Removing unused feature of the SAT solver (user-guided variable ordering). | Alan Mishchenko | 2016-04-12 | 2 | -53/+1 |
| | |||||
* | Removing unused feature of the SAT solver (native support for cardinality ↵ | Alan Mishchenko | 2016-04-12 | 3 | -33/+2 |
| | | | | constraint). | ||||
* | Improvements to delay-optimization in &satlut. | Alan Mishchenko | 2016-04-04 | 1 | -1/+8 |
| | |||||
* | Corner-case bug fix in 'satclp' with conflict limit. | Alan Mishchenko | 2016-03-25 | 1 | -5/+10 |
| | |||||
* | Bug fix in &fftest: not outputting test patterns when user test patterns are ↵ | Alan Mishchenko | 2016-03-09 | 1 | -8/+15 |
| | | | | given. | ||||
* | Experiments with SAT-based mapping. | Alan Mishchenko | 2016-02-07 | 1 | -0/+23 |
| | |||||
* | Adding a way to derive cardinality constraint as a sorting network. | Alan Mishchenko | 2016-01-13 | 1 | -4/+89 |
| | |||||
* | Integrating new CNF generation into &bmc. | Alan Mishchenko | 2016-01-12 | 2 | -8/+10 |
| | |||||
* | Experiments with SAT-based mapping. | Alan Mishchenko | 2016-01-10 | 1 | -0/+9 |
| | |||||
* | Adding support of candinality clause to the SAT solver. | Alan Mishchenko | 2016-01-10 | 4 | -4/+45 |
| | |||||
* | Improvements to 'satclp'. | Alan Mishchenko | 2015-11-09 | 1 | -4/+180 |
| | |||||
* | Improvements to 'satclp'. | Alan Mishchenko | 2015-11-09 | 1 | -3/+3 |
| | |||||
* | Improvements to 'satclp' (unfinished). | Alan Mishchenko | 2015-11-06 | 1 | -54/+163 |
| | |||||
* | Improvements to 'satclp' (unfinished). | Alan Mishchenko | 2015-11-06 | 1 | -8/+344 |
| | |||||
* | Improvements to 'satclp'. | Alan Mishchenko | 2015-10-28 | 1 | -10/+161 |
| | |||||
* | Set the default cube limit in 'satclp' to be 0. | Alan Mishchenko | 2015-10-23 | 1 | -2/+2 |
| | |||||
* | Quality improvement in 'satclp'. | Alan Mishchenko | 2015-10-22 | 1 | -2/+85 |
| | |||||
* | Minor tuning in 'satclp'. | Alan Mishchenko | 2015-10-22 | 1 | -10/+18 |
| | |||||
* | Corner case bug in 'satclp'. | Alan Mishchenko | 2015-10-21 | 1 | -3/+6 |
| | |||||
* | Code inserts to profile runtime of 'satclp'. | Alan Mishchenko | 2015-10-21 | 1 | -0/+24 |
| | |||||
* | Additional improvements in 'satclp'. | Alan Mishchenko | 2015-10-18 | 1 | -1/+1 |
| | |||||
* | Additional improvements in 'satclp'. | Alan Mishchenko | 2015-10-18 | 1 | -1/+162 |
| | |||||
* | Added approximate SAT-based irredundant procedure to 'satclp'. | Alan Mishchenko | 2015-10-17 | 1 | -0/+80 |
| | |||||
* | Added comment how to print binary clauses in procedure Sat_SolverWriteDimacs(). | Alan Mishchenko | 2015-10-16 | 1 | -1/+4 |
| | |||||
* | Bug fix in 'satclp -r'. | Alan Mishchenko | 2015-10-16 | 1 | -1/+4 |
| | |||||
* | New switch 'satclp -r' to reverse variable order. | Alan Mishchenko | 2015-10-07 | 1 | -6/+10 |
| | |||||
* | Tuning SAT solver for QBF instances. | Alan Mishchenko | 2015-09-18 | 1 | -1/+1 |
| | |||||
* | Tuning SAT solver for QBF instances. | Alan Mishchenko | 2015-09-18 | 2 | -8/+18 |
| | |||||
* | Tuning SAT solver for QBF instances. | Alan Mishchenko | 2015-09-18 | 1 | -3/+9 |
| | |||||
* | Experiments with SAT-based collapsing. | Alan Mishchenko | 2015-09-04 | 3 | -51/+130 |
| | |||||
* | Experiments with SAT-based collapsing. | Alan Mishchenko | 2015-09-04 | 1 | -71/+148 |
| | |||||
* | Experiments with SAT-based collapsing. | Alan Mishchenko | 2015-09-03 | 1 | -0/+227 |
| | |||||
* | Experiments with SAT-based collapsing. | Alan Mishchenko | 2015-09-03 | 3 | -8/+52 |
| | |||||
* | Removing unhelpful assertion in CEX minimization. | Alan Mishchenko | 2015-09-01 | 1 | -1/+1 |
| | |||||
* | Merging two threads. | Alan Mishchenko | 2015-05-25 | 1 | -0/+4 |
|\ |