Insanity#15
Merged
MusinaPolina merged 124 commits intodevfrom Aug 16, 2022
Merged
Conversation
# Conflicts: # src/commonMain/kotlin/org/kosat/CDCL.kt
# Conflicts: # src/commonMain/kotlin/org/kosat/CDCL.kt # src/jvmTest/kotlin/test.kt
# Conflicts: # src/commonMain/kotlin/org/kosat/CDCL.kt # src/jvmTest/kotlin/test.kt
AlekseyVlasov
added a commit
that referenced
this pull request
Aug 23, 2022
* first draft of interface * small changes * remove useless clauses & delete long-running test * remove useless clauses function * deleted long-running test * external class * reordered functions. Created new functions for incremental Sat * - basic vsids implementation * private variables + comments style * reordered functions. Created new functions for incremental Sat * assumptions * - bve implementation (improves time on big tests) - remove tautologies (fast implementation) * Reader classes and Kosat class separation * Using Kosat class instead of CDCL * Solve with assumptions * Assumptions tests * reducing in- and pre-processing, small fixes * Add to units * Resolving clearing of trail * pass varsNumber by user * added comments * review fixes * fix return model * test distribution between folders added DESCRIPTION.md (for tests) * assumptions fixes * assumptions fixes (uncomment test) * small fixes * more hard tests * Preprocessing and restarts from dev (#13) * fixed addResolvents function (not adding tautology clauses to list) updated score array definition for correct work * Correctly restoring answer in SAT cnf's * fixed bug with deleting duplicated clauses by subsuming (e.g. if clauses contain 2 copies of {1} clause, we were deleting both of them) * tests added * merge Co-authored-by: daver <averkov.daniil@yandex.ru> * code style + comments * added Clause * added class Selector (currently abstract class for VSIDS) for branch heuristics * preprocessor class draft * preprocessor class small fixes * draft Restarter class * draft Trail * warning changes * luby restarts * removed unnecessary interface * Refactoring functions order in CDCL * Preprocessor fix * empty constructor + solverType * Incremental addVariable * MutableList<Int> -> Clause * Java style reoder * Java style reorder * Assumptions tests * Assumptions fixes * phase saving * repaired vsids * reduceDB * Some PR fixes * moved reduceDB from restarts to CDCL + added reduceIncrement * removed reduceIncrement * .locked added to initial clauses * some fixes * assumptions merge fix * removed unused subsumed from restarter.kt * newClause remove redundant lits from added clause * clauses with only 1 literal wouldn't be in clauses anymore. Comments * removed early check of conflict (maybe better with queue) * renamed litIndex * reworked updateWatchers s.t. watchers in clause always at 0,1 places * divided watchers on 2 sides for literals * split clauses in 2 parts: learnts and constraints * delegate clause by lits * new TODO * -some TODO's resolved -analyzeActivity array added -optimized vsids build function * false checks (wrongAssumptions) deleted * uncommented check * watchers changed from set to list learnClause() + addConstraint() functions * for -> foreach * tests * . * priority queue * keep order in priority queue add scoresPQ - doesn't work! * fixed vsids on priority queue * tests * tests * total number + tests * testing files from main * removed unused Clause property locked * restarter comments * CDCL comments * phaseSaving -> polarity * learnClause -> addLearnt * input from file with right configuration * testing files from main * updated analyzeConflicts and removed satisfiable * kosat again * deleted big test * varsNumber -> numberOfVariables (didn't understand topVar name) * variableValues -> getModel + minor fixes * comment for level variable * comments for solve function. nextVariable -> nextDecisionVariable * check for x and -x in clause. ctrl + alt + l * reserveVars * ctrl + alt + l * inheritance (clause.kt by) * comment for restarter + removed useless comments and constant * Incremental interface docs * VarState * Some fixes + test filter benchmarks * + todo docs + renamed setVariableValues to assign, changed signature * + todo docs + use (miniSatSolver) * Int.clauseSize -> clauseSize(Int) * recoverAnswer todo docs * todo: value class Lit, consistent indexation * todo: parametrized tests * void fun assign * void fun assign fix * apply Preprocessor.kt * VarStatus.clause -> VarStatus.reason * measure time by klock * scores -> activity * todo add docs for Preprocessor.kt * incremental structure of restarter * lubySeq -> luby as function * minimizing comments * Parameterized tests (don't work) * Parameterized tests (don't work) * commit for timechecking tests * abs -> variable + litIndex resolved * vsids(...) -> getMaxActivityVariable(...) * countOccurrence unused line removed * status -> value everywhere * Parameterized tests (don't work) * Parameterized tests (don't work) * fixes * big merge * number of conflicts output * fixes * simple variable selector * units removed * path simplification * tests * swap + seen * Simple -> FixedOrder + VsidsWithoutQueue * fixme p cnf 0 0 fix * new vsids used * tests * simple tests update * simple placeholder for vsids (simple realization but works) * backjump fix * Insanity (#15) * added Clause * added class Selector (currently abstract class for VSIDS) for branch heuristics * preprocessor class draft * preprocessor class small fixes * draft Restarter class * draft Trail * warning changes * luby restarts * removed unnecessary interface * Refactoring functions order in CDCL * Preprocessor fix * empty constructor + solverType * Incremental addVariable * MutableList<Int> -> Clause * Java style reoder * Java style reorder * Assumptions tests * Assumptions fixes * phase saving * repaired vsids * reduceDB * Some PR fixes * moved reduceDB from restarts to CDCL + added reduceIncrement * removed reduceIncrement * .locked added to initial clauses * some fixes * assumptions merge fix * removed unused subsumed from restarter.kt * newClause remove redundant lits from added clause * clauses with only 1 literal wouldn't be in clauses anymore. Comments * removed early check of conflict (maybe better with queue) * renamed litIndex * reworked updateWatchers s.t. watchers in clause always at 0,1 places * divided watchers on 2 sides for literals * split clauses in 2 parts: learnts and constraints * delegate clause by lits * new TODO * -some TODO's resolved -analyzeActivity array added -optimized vsids build function * false checks (wrongAssumptions) deleted * uncommented check * watchers changed from set to list learnClause() + addConstraint() functions * for -> foreach * tests * . * priority queue * keep order in priority queue add scoresPQ - doesn't work! * fixed vsids on priority queue * tests * tests * total number + tests * testing files from main * removed unused Clause property locked * restarter comments * CDCL comments * phaseSaving -> polarity * learnClause -> addLearnt * input from file with right configuration * testing files from main * updated analyzeConflicts and removed satisfiable * kosat again * deleted big test * varsNumber -> numberOfVariables (didn't understand topVar name) * variableValues -> getModel + minor fixes * comment for level variable * comments for solve function. nextVariable -> nextDecisionVariable * check for x and -x in clause. ctrl + alt + l * reserveVars * ctrl + alt + l * inheritance (clause.kt by) * comment for restarter + removed useless comments and constant * Incremental interface docs * VarState * Some fixes + test filter benchmarks * + todo docs + renamed setVariableValues to assign, changed signature * + todo docs + use (miniSatSolver) * Int.clauseSize -> clauseSize(Int) * recoverAnswer todo docs * todo: value class Lit, consistent indexation * todo: parametrized tests * void fun assign * void fun assign fix * apply Preprocessor.kt * VarStatus.clause -> VarStatus.reason * measure time by klock * scores -> activity * todo add docs for Preprocessor.kt * incremental structure of restarter * lubySeq -> luby as function * minimizing comments * Parameterized tests (don't work) * Parameterized tests (don't work) * commit for timechecking tests * abs -> variable + litIndex resolved * vsids(...) -> getMaxActivityVariable(...) * countOccurrence unused line removed * status -> value everywhere * Parameterized tests (don't work) * Parameterized tests (don't work) * fixes * big merge * number of conflicts output * fixes * simple variable selector * units removed * path simplification * tests * swap + seen * Simple -> FixedOrder + VsidsWithoutQueue * fixme p cnf 0 0 fix * new vsids used * tests * simple tests update * simple placeholder for vsids (simple realization but works) * backjump fix Co-authored-by: MusinaPolina <pmusina03@gmail.com> Co-authored-by: daver <averkov.daniil@yandex.ru> * renumber * fix non incremental * renumber test passed * global minimize marks * bag fix * parametrized assumptions test * parametrized assumptions test fix * comments update (+ luby 2 -> 1) * benchmarks test * fixes * fixes * Correct version of vsids on PriorityQueue: - bug fix in build PriorityQueue - indices renumbered - improved kosat solution checker if cnf is solvable * fixed check of kosat solution * seen outside analyzeConflict * clausesToRemove * without star points * tests MiniSat time * refactoring priority queue added number of made decisions * ctrl alt L Co-authored-by: AlekseyVlasov <89700696+AlekseyVlasov@users.noreply.github.com> Co-authored-by: AlekseyVlasov <vlasoff.al03@gmail.com> Co-authored-by: daver <averkov.daniil@yandex.ru>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Soon will be added small changes (probably some comments and renamings of functions)