summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat/satSolver.c
Commit message (Expand)AuthorAgeFilesLines
* Adding efficient procedure to minimize the set of assumptions (improved liter...Alan Mishchenko2017-03-021-1/+8
* Adding alternative generalization procedure.Alan Mishchenko2017-03-011-1/+1
* Adding efficient procedure to minimize the set of assumptions.Alan Mishchenko2017-03-011-0/+52
* Fixing missing sat_solver APIs in 'iprove'.Alan Mishchenko2017-02-161-6/+24
* Fixing missing sat_solver APIs in 'iprove'.Alan Mishchenko2017-02-151-3/+40
* Commenting out uncommented message.Alan Mishchenko2017-02-111-1/+1
* Updates to variable activity in the SAT solver.Alan Mishchenko2017-02-111-286/+193
* Re-introducing floating-point activity in the SAT solver.Alan Mishchenko2017-02-071-2/+18
* Re-introducing floating-point activity in the SAT solver.Alan Mishchenko2017-02-061-39/+135
* Improvements to inductive generalization in IC3/PDR by Zyad Hassan.Alan Mishchenko2017-02-021-0/+120
* Fixes and adjustments for the edge computation flow.Alan Mishchenko2016-07-151-1/+1
* Experiments with edge-based mapping.Alan Mishchenko2016-06-151-2/+3
* Added switch 'bmc3 -r' to disable periodic restarts in the SAT solver.Alan Mishchenko2016-05-191-1/+1
* This code was accidentally deleted from the SAT solver (effectively disabling...Alan Mishchenko2016-04-301-0/+7
* Improved algo for edge computation.Alan Mishchenko2016-04-231-0/+13
* Adding new implementation of LEXSAT.Alan Mishchenko2016-04-121-0/+68
* Restructing sat_solver_solve() method for pushing/popping assumptions.Alan Mishchenko2016-04-121-142/+134
* Removing unused feature of the SAT solver (user-guided variable ordering).Alan Mishchenko2016-04-121-41/+1
* Removing unused feature of the SAT solver (native support for cardinality con...Alan Mishchenko2016-04-121-21/+2
* Improvements to delay-optimization in &satlut.Alan Mishchenko2016-04-041-1/+8
* Adding support of candinality clause to the SAT solver.Alan Mishchenko2016-01-101-2/+23
* Experiments with SAT-based collapsing.Alan Mishchenko2015-09-041-1/+1
* Experiments with SAT-based collapsing.Alan Mishchenko2015-09-031-8/+40
* Adding command to dump UNSAT core of BMC instance.Alan Mishchenko2014-04-071-0/+8
* Compiler warning about unused variable.Alan Mishchenko2013-09-171-2/+2
* Changing dynamic CNF loading code to perform loading before propagate() as op...Alan Mishchenko2013-09-161-0/+31
* SAT solver with dynamic CNF loading.Alan Mishchenko2013-08-011-4/+28
* Limiting runtime limit checks in 'pdr'.Alan Mishchenko2013-06-211-1/+1
* Adding a wrapper around clock() for more accurate time counting in ABC.Alan Mishchenko2013-05-271-12/+12
* Changing how often timeout is checked in the SAT solver and several applicati...Alan Mishchenko2013-05-271-1/+1
* SAT variable profiling.Alan Mishchenko2013-05-181-2/+2
* SAT variable profiling.Alan Mishchenko2013-05-181-1/+11
* SAT variable profiling (undo).Alan Mishchenko2013-05-181-14/+0
* SAT variable profiling.Alan Mishchenko2013-05-181-0/+14
* SAT variable profiling (undo).Alan Mishchenko2013-05-181-14/+0
* SAT variable profiling.Alan Mishchenko2013-05-181-0/+14
* Adding rollback for the other solver.Alan Mishchenko2013-04-251-1/+118
* Fixing the dump of SAT solver into a CNF file.Alan Mishchenko2013-03-261-1/+2
* Compiler warnings.Alan Mishchenko2013-02-231-0/+4
* Increasing memory page limit in the main SAT solver.Alan Mishchenko2012-10-311-1/+1
* 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-221-0/+16
* Improvements in the proof-logging SAT solver.Alan Mishchenko2012-07-111-10/+4
* Improving print-outs of &vta and &gla.Alan Mishchenko2012-07-101-1/+3
* Bug fix in the recent changes to the SAT solver.Alan Mishchenko2012-07-091-0/+3
* Removing print-out message.Alan Mishchenko2012-07-091-1/+1
* Adding several command-line arguments to 'dsat'.Alan Mishchenko2012-07-091-6/+12
* Added learned clause recycling to the SAT solver (may impact bmc2, bmc3, dsat...Alan Mishchenko2012-07-091-190/+217
* Fixing time primtouts throughout the code.Alan Mishchenko2012-07-071-1/+2
* Fixing time primtouts throughout the code.Alan Mishchenko2012-07-071-2/+2