Skip to content

Commit

Permalink
picosat-959
Browse files Browse the repository at this point in the history
  • Loading branch information
Nico Buchholz committed Nov 20, 2022
1 parent 95ad85c commit 1d261e2
Show file tree
Hide file tree
Showing 16 changed files with 11,670 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 - 2013, 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.

148 changes: 148 additions & 0 deletions NEWS
Original file line number Diff line number Diff line change
@@ -0,0 +1,148 @@
news for release 959 since 953
------------------------------

* fixed header comments

* fixed minor compilation issues

* fixed unitialized memory access problem for 'picosat_deref_partial'
and another issue with partial models

* added 'picosat_add_arg' and 'picosat_add_lits'

* '--plain' and 'picosat_set_plain' to disable failed literal probing

* new '#define PICOSAT_REENTRANT_API' in 'picosat.h'

* added manager so no more global variables
(allows multiple instances, requires manager object)

news for release 951 since 941
------------------------------

* cleaned up code (based on comments by Donald Knuth)

* lreduce=O(conflicts^.5)

* added 'picosat_visits' and 'picosat_decisions'

* added '--partial' command line option

* added 'picosat_deref_partial' and 'picosat_save_original_clauses'

* added 'picomcs' as example for MSS computation

news for release 941 since 936
------------------------------

* added 'picogcnf'

* added All-SAT mode ('--all' command line option)

* statistics include time spent in failed literal preprocessing (probing)

* 'picosat_failed_context' for 'push & pop'
(and tested failed assumptions for 'push & pop')

* 'picosat_simplify' for forced garbage collection

* undefined NFL, defined NADC (= failed literals on, ADC's off)

* 'picosat_push' and 'picosat_pop' (beta version)

* fixed some issues related to binary clause handling and
generating list of failed assumptions

news for release 936 since 935
------------------------------

* simple minimal unsatisfiable core (MUS) extractor 'picomus'
(example for using 'picosat_mus_assumptions' and 'picosat_coreclause')

* added 'picosat_mus_assumptions'

* added 'picosat_{set_}propagations'

* new 'int' return value for 'picosat_enable_trace_generation' to
check for trace code being compiled

news for release 935 since 926
------------------------------

* added 'picosat_failed_assumptions' (plural)

* new '-A <failedlits>' command line option

* fixed failed assumption issues

* added 'picosat_remove_learned'

* added 'picosat_reset_{phases,scores}'

* added 'picosat_set_less_important_lit'

* added 'picosat_res'

news for release 926 since 846
------------------------------

* random initial phase (API of 'picosat_set_default_phase' changed)

* fixed accumulative failed assumption (multiple times)

* fixed missing original clause in core generation with assumptions

* fixed debugging code for memory allocation

* shared library in addition to static library

* removed potential UNKNOWN result without decision limit

* added picosat_set_more_important_lit

* added picosat_coreclause

* 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 @@
959
Loading

0 comments on commit 1d261e2

Please sign in to comment.