Skip to content

Commit

Permalink
picosat-913
Browse files Browse the repository at this point in the history
  • Loading branch information
Nico Buchholz committed Nov 20, 2022
1 parent 95ad85c commit b910f24
Show file tree
Hide file tree
Showing 13 changed files with 8,776 additions and 1 deletion.
20 changes: 20 additions & 0 deletions LICENSE
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
Copyright (c) 2006 - 2009, Armin Biere, Johannes Kepler University.

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to
deal in the Software without restriction, including without limitation the
rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
IN THE SOFTWARE.

47 changes: 47 additions & 0 deletions NEWS
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
news for release 91x since 846
------------------------------

* propagation of binary clauses until completion

* fixed API usage 'assume;sat;sat'

* literals move to front (LMTF) during traversal of visited clauses

* switched from inner/outer to Luby style restart scheduling

* less agressive reduce schedule

* replaced watched literals with head and tail pointers

* add 'picosat_failed_assumption', which allows to avoid tracing and core
generation, if one is only interested in assumptions in the core

* fixed a BUG in the generic iterator code of clauses
(should rarely happen unless you use a very sophisticated malloc lib)

news for release 846 since 632
------------------------------

* cleaned up assumption handling (actually removed buggy optimization)

* incremental core generation

* experimental 'all different constraint' handling as in our FMCAD'08 paper

* new API calls:

- picosat_add_ado_lit (add all different object literal)
- picosat_deref_top_level (deref top level assignment)
- picosat_changed (check whether extension was possible)
- picosat_measure_all_calls (per default do not measure adding time)
- picosat_set_prefix (set prefix for messages)

* 64 bit port (and compilation options)

* optional NVSIDS visualization code

* resource controlled failed literal implementation

* disconnect long clauses satisfied at lower decision level

* controlling restarts
5 changes: 5 additions & 0 deletions README
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
These are the sources of the PicoSAT solver.
The preprocessor is not included.
To compile run './configure && make'.
The API is document in 'picosat.h'.
See also 'NEWS' and 'LICENSE'.
1 change: 0 additions & 1 deletion README.md

This file was deleted.

1 change: 1 addition & 0 deletions VERSION
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
913
Loading

0 comments on commit b910f24

Please sign in to comment.