summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat
Commit message (Expand)AuthorAgeFilesLines
* Changing how often timeout is checked in the SAT solver and several applicati...Alan Mishchenko2013-05-272-2/+2
* SAT variable profiling.Alan Mishchenko2013-05-182-4/+4
* SAT variable profiling.Alan Mishchenko2013-05-183-3/+27
* SAT variable profiling (undo).Alan Mishchenko2013-05-182-16/+0
* SAT variable profiling.Alan Mishchenko2013-05-182-0/+16
* SAT variable profiling (undo).Alan Mishchenko2013-05-182-16/+0
* SAT variable profiling.Alan Mishchenko2013-05-182-0/+16
* Adding rollback for the other solver.Alan Mishchenko2013-04-253-3/+141
* Fixing the dump of SAT solver into a CNF file.Alan Mishchenko2013-03-263-17/+18
* Compiler warnings.Alan Mishchenko2013-02-232-0/+5
* Fixing compilation problems on Linux-32 related to constants of type unsigned...Alan Mishchenko2013-01-301-6/+6
* Increasing memory page limit in the main SAT solver.Alan Mishchenko2012-10-311-1/+1
* C++ portability changes.Alan Mishchenko2012-10-032-2/+3
* Reversed to a buggy version of reduceDB in complete proof-logging, because it...Alan Mishchenko2012-09-121-2/+2
* Changes to allow &gla to run with fSimple = 1 (useful for debugging).Alan Mishchenko2012-08-311-0/+1
* Bug fix in &gla.Alan Mishchenko2012-08-273-5/+16
* Scalable gate-level abstraction.Alan Mishchenko2012-08-021-0/+12
* Scalable gate-level abstraction.Alan Mishchenko2012-07-311-1/+1
* Saving variable activity during rollback.Alan Mishchenko2012-07-302-0/+7
* Saving variable activity during rollback.Alan Mishchenko2012-07-302-1/+10
* Disabling learned clause removal when incremental proof-logging is running (t...Alan Mishchenko2012-07-301-1/+1
* Fixing performance bug with old proof-logging (adding clauses multiple times).Alan Mishchenko2012-07-301-0/+1
* Fixed compiler warnings.Alan Mishchenko2012-07-291-2/+2
* Reducing memory usage in proof-based abstraction.Alan Mishchenko2012-07-293-30/+393
* Fixed the problem with 'write_cnf' after recent changes to the SAT solver.Alan Mishchenko2012-07-281-37/+49
* Fixed the problem with 'write_cnf' after recent changes to the SAT solver.Alan Mishchenko2012-07-282-65/+89
* Recording and reusing learned util clauses in bmc2.Alan Mishchenko2012-07-221-0/+1
* Recording and reusing learned util clauses in bmc3.Alan Mishchenko2012-07-222-1/+19
* Debugging a proof error.Alan Mishchenko2012-07-132-12/+7
* Debugging a proof error.Alan Mishchenko2012-07-131-2/+2
* Debugging a proof error.Alan Mishchenko2012-07-131-0/+2
* Debugging a proof error.Alan Mishchenko2012-07-131-25/+9
* Debugging a proof error.Alan Mishchenko2012-07-131-0/+2
* Debugging a proof error.Alan Mishchenko2012-07-131-3/+3
* Debugging a proof error.Alan Mishchenko2012-07-131-0/+1
* Debugging a proof error.Alan Mishchenko2012-07-131-1/+1
* Debugging a proof error.Alan Mishchenko2012-07-131-1/+2
* Debugging a proof error.Alan Mishchenko2012-07-131-2/+5
* Debugging a proof error.Alan Mishchenko2012-07-131-1/+3
* Debugging a proof error.Alan Mishchenko2012-07-131-3/+21
* Debugging a proof error.Alan Mishchenko2012-07-131-2/+6
* Debugging a proof error.Alan Mishchenko2012-07-131-0/+3
* Several small changes and fixes.Alan Mishchenko2012-07-133-5/+11
* Removed useless file.Alan Mishchenko2012-07-121-5/+6
* Added procedure for checking satisfied clauses.Alan Mishchenko2012-07-121-0/+37
* Silencing warnings.Alan Mishchenko2012-07-111-1/+1
* Silencing warnings.Alan Mishchenko2012-07-112-7/+6
* Changes to clause mapping.Alan Mishchenko2012-07-113-24/+30
* Changes to clause mapping.Alan Mishchenko2012-07-111-1/+1
* Improvements in the proof-logging SAT solver.Alan Mishchenko2012-07-118-455/+498