summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat/satSolver.h
Commit message (Collapse)AuthorAgeFilesLines
* Added switch 'bmc3 -r' to disable periodic restarts in the SAT solver.Alan Mishchenko2016-05-191-0/+1
|
* Improved algo for edge computation.Alan Mishchenko2016-04-231-1/+1
|
* Adding new implementation of LEXSAT.Alan Mishchenko2016-04-121-0/+1
|
* Restructing sat_solver_solve() method for pushing/popping assumptions.Alan Mishchenko2016-04-121-8/+19
|
* Removing unused feature of the SAT solver (user-guided variable ordering).Alan Mishchenko2016-04-121-12/+0
|
* Removing unused feature of the SAT solver (native support for cardinality ↵Alan Mishchenko2016-04-121-10/+0
| | | | constraint).
* Experiments with SAT-based mapping.Alan Mishchenko2016-02-071-0/+23
|
* Experiments with SAT-based mapping.Alan Mishchenko2016-01-101-0/+9
|
* Adding support of candinality clause to the SAT solver.Alan Mishchenko2016-01-101-1/+10
|
* Experiments with SAT-based collapsing.Alan Mishchenko2015-09-041-0/+7
|
* Experiments with SAT-based collapsing.Alan Mishchenko2015-09-031-0/+11
|
* Bug fix in QBF solver.Alan Mishchenko2015-05-041-0/+4
|
* Experiments with SAT-based cube enumeration.Alan Mishchenko2015-03-051-19/+19
|
* Compiler warnings.Alan Mishchenko2014-10-281-2/+2
|
* Adding command to dump UNSAT core of BMC instance.Alan Mishchenko2014-04-071-1/+7
|
* Adding switch to handle only single faults.Alan Mishchenko2014-04-011-4/+4
|
* Changes to LUT mappers.Alan Mishchenko2014-03-041-0/+64
|
* Changes to LUT mappers.Alan Mishchenko2014-02-271-0/+46
|
* Specialized induction check.Alan Mishchenko2013-10-311-0/+39
|
* Specialized induction check.Alan Mishchenko2013-10-311-0/+19
|
* SAT solver with dynamic CNF loading.Alan Mishchenko2013-08-011-0/+6
|
* Adding a wrapper around clock() for more accurate time counting in ABC.Alan Mishchenko2013-05-271-3/+3
|
* SAT variable profiling.Alan Mishchenko2013-05-181-0/+14
|
* SAT variable profiling (undo).Alan Mishchenko2013-05-181-2/+0
|
* SAT variable profiling.Alan Mishchenko2013-05-181-0/+2
|
* SAT variable profiling (undo).Alan Mishchenko2013-05-181-2/+0
|
* SAT variable profiling.Alan Mishchenko2013-05-181-0/+2
|
* Adding rollback for the other solver.Alan Mishchenko2013-04-251-0/+21
|
* Compiler warnings.Alan Mishchenko2013-02-231-0/+1
|
* Recording and reusing learned util clauses in bmc3.Alan Mishchenko2012-07-221-1/+3
|
* Several small changes and fixes.Alan Mishchenko2012-07-131-1/+0
|
* Improvements in the proof-logging SAT solver.Alan Mishchenko2012-07-111-5/+4
|
* Adding several command-line arguments to 'dsat'.Alan Mishchenko2012-07-091-0/+3
|
* Added learned clause recycling to the SAT solver (may impact bmc2, bmc3, ↵Alan Mishchenko2012-07-091-3/+14
| | | | dsat, etc).
* Updating project settings to have simpler include paths.Alan Mishchenko2012-07-071-1/+1
|
* Fixing time primtouts throughout the code.Alan Mishchenko2012-07-071-3/+3
|
* Added memory reporting to &vta.Alan Mishchenko2012-06-221-1/+1
|
* Reporing memory usage by the SAT solver in 'bmc3'.Alan Mishchenko2012-06-151-0/+1
|
* Moving Vec_Set_t to the vector directory.Alan Mishchenko2012-03-281-1/+1
|
* Improved memory management of proof-logging and propagated changes.Alan Mishchenko2012-02-161-2/+2
|
* Major restructuring of the code.Alan Mishchenko2012-01-211-2/+2
|
* Variable timeframe abstraction.Alan Mishchenko2012-01-201-3/+3
|
* Bug fix related to not properly resizing SAT solver's model array.Alan Mishchenko2012-01-061-7/+8
|
* APIs to represent simple gates in CNF.Alan Mishchenko2012-01-051-0/+100
|
* Transforming the solver to use different clause representation.Alan Mishchenko2011-12-231-65/+70
|
* Undoing temporary change to the solver.Alan Mishchenko2011-12-151-1/+1
|
* Temporary change to the solver.Alan Mishchenko2011-12-151-1/+1
|
* Implemented rollback in the main SAT solver and updated PDR to use it (saves ↵Alan Mishchenko2011-12-101-0/+1
| | | | about 5% of runtime).
* Changes to the main SAT solver: fixing performance bug (resetting decay ↵Alan Mishchenko2011-12-091-41/+9
| | | | params after each restart), making the SAT solver platform- and runtime-independent (by using interger-based activity).
* Proof-logging in the updated solver.Alan Mishchenko2011-12-041-2/+2
|
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-04 23:34:20 +0000