Skip to content

CDCL solving #869

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
idan0610 wants to merge 467 commits into
base: master
Choose a base branch
from
Open

CDCL solving #869

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
467 commits
Select commit Hold shift + click to select a range
b9e334e
switching to polarity branching heuristic
idan0610 Sep 4, 2024
be49615
update all directions on every decision
idan0610 Sep 8, 2024
b9723ac
small fix
idan0610 Sep 8, 2024
4ec106a
minor
idan0610 Sep 8, 2024
4792150
Revert "minor"
idan0610 Sep 9, 2024
7f3b778
Revert "small fix"
idan0610 Sep 9, 2024
9244faf
Revert "Revert "small fix""
idan0610 Sep 9, 2024
f840777
Revert "Revert "minor""
idan0610 Sep 9, 2024
b74d009
Revert "minor"
idan0610 Sep 9, 2024
8ca5eef
Revert "small fix"
idan0610 Sep 9, 2024
0591440
Revert "update all directions on every decision"
idan0610 Sep 9, 2024
2e597c3
Compute combined polarity and VSIDS score
idan0610 Sep 9, 2024
f10bcdf
adding calls for tightenBoundsOnConstraintMatrix and
idan0610 Sep 10, 2024
f774ae1
adding calls for tightenBoundsOnConstraintMatrix and
idan0610 Sep 10, 2024
d389530
tightenBoundsOnConstraintMatrix when calling Engine::adjustAssignmen…
omriisack Sep 11, 2024
b0793bd
Merge remote-tracking branch 'origin/cdcl-new' into cdcl-new
omriisack Sep 11, 2024
b74a3ca
restoring constant MINIMAL_COEFFICIENT_FOR_TIGHTENING to 0.01
idan0610 Sep 15, 2024
a0ba252
adding frequency for basis bouse
idan0610 Sep 15, 2024
5ada6c7
Revert "adding frequency for basis bouse"
idan0610 Sep 15, 2024
4d76461
stop propagation when too little bounds are learned during a pass ove…
omriisack Sep 16, 2024
7ca7903
commenting decay in VSIDS score
idan0610 Sep 18, 2024
2d0d1ea
Merge remote-tracking branch 'origin/cdcl-new' into cdcl-new
idan0610 Sep 18, 2024
b485afe
adding VSIDS decay based on choosing literal base on last K clauses
idan0610 Sep 22, 2024
33f6967
minor
idan0610 Sep 22, 2024
f5c0862
Add the VSIDS decay threshold into Options
idan0610 Sep 22, 2024
9a875a3
stop propagation only if there is a literal to split on
omriisack Sep 24, 2024
3255c62
fix duplications of literal in the assigned literals list
idan0610 Sep 24, 2024
c1f0479
minor
idan0610 Sep 24, 2024
5ea73f8
Add time measurements for SmtCore methods
idan0610 Sep 26, 2024
e3e1ac9
Separate time measurements for cadical callbacks, and methods called …
idan0610 Sep 26, 2024
358568b
add percentages for time spent in main loop, SmtCore callbacks, prepr…
idan0610 Sep 26, 2024
07dba4b
Add breakdown for cadical callbacks time measurements in statistics
idan0610 Sep 27, 2024
105da86
replace _satisfiedClauses type to be CDHashSet, and _assignedLiterals…
idan0610 Sep 29, 2024
8a55036
minor
idan0610 Sep 29, 2024
3f48f66
stop measure time for notify_backtrack before the calls for notify_as…
idan0610 Sep 29, 2024
a63df46
Change decay behavior to reset the clauses every time the decay thres…
idan0610 Oct 28, 2024
8f6b9ec
reset clauses according to the luby algorithm
idan0610 Oct 29, 2024
acd5aed
adding restart of cadical, based by the number of clauses
idan0610 Oct 29, 2024
da9d425
Minor
omriisack Oct 29, 2024
384ca41
Merge remote-tracking branch 'origin/cdcl-new' into cdcl-new
omriisack Oct 29, 2024
e7f3cf5
small fixes
idan0610 Oct 29, 2024
a03e370
Merge remote-tracking branch 'origin/cdcl-new' into cdcl-new
idan0610 Oct 29, 2024
1bb0423
Minor
omriisack Oct 29, 2024
1c20dbe
Minor
omriisack Oct 29, 2024
1adc26b
change restart behavior to be based on number of calls to solve
idan0610 Oct 30, 2024
cbdb73f
minor
idan0610 Oct 30, 2024
dc148f0
small fix
idan0610 Oct 30, 2024
03cd3b3
change restart to be based on number of conflict clauses
idan0610 Oct 31, 2024
09527e9
Revert "change restart to be based on number of conflict clauses"
idan0610 Nov 1, 2024
34ed691
return to restart v2, with luby const = 256
idan0610 Nov 1, 2024
da35529
canceling decay
idan0610 Nov 3, 2024
2620aa9
Revert "canceling decay"
idan0610 Nov 4, 2024
8e671da
canceling restart + change luby constant to 256 for decay
idan0610 Nov 4, 2024
17be078
Store tableau basics and use them as part of context
OmriIsacHUJI Nov 6, 2024
4085542
minor
idan0610 Nov 6, 2024
b9ecf7f
restore restart
idan0610 Nov 6, 2024
4bd283e
delete restarts again, store tableau basics only for tree leaves
omriisack Nov 6, 2024
3a8b002
Minor
OmriIsacHUJI Nov 7, 2024
8adbec6
restore restart again, add restore tableu to restart
idan0610 Nov 7, 2024
51e3b86
minor
idan0610 Nov 7, 2024
b7a2ef1
Remove unnecessary computations from Tablea state re\store
omriisack Nov 7, 2024
d2a6b46
Minor
omriisack Nov 7, 2024
d21e6fe
Minor
omriisack Nov 7, 2024
52be00e
Revert "Minor"
omriisack Nov 7, 2024
a46166c
Revert "Minor"
omriisack Nov 7, 2024
fd20c9b
Revert "Remove unnecessary computations from Tablea state re\store"
omriisack Nov 7, 2024
c166c61
fix restart + tableau state is not cd
idan0610 Nov 7, 2024
2176cfd
minor
idan0610 Nov 7, 2024
25e17b7
removing restart again
idan0610 Nov 8, 2024
b92a9dc
minor
idan0610 Nov 8, 2024
3ee6299
Revert "minor"
idan0610 Nov 10, 2024
8202a1a
Revert "removing restart again"
idan0610 Nov 10, 2024
014b33d
restoring restart again, removing decay (buggy)
idan0610 Nov 10, 2024
15bef13
fix for bug (removing skip notification when there is a conflict clause)
idan0610 Nov 10, 2024
85be882
Revert "fix for bug (removing skip notification when there is a confl…
idan0610 Nov 10, 2024
eb0841e
Revert "restoring restart again, removing decay (buggy)"
idan0610 Nov 10, 2024
285e756
limit the number of external clauses to add to 1 + cancel store and r…
idan0610 Nov 10, 2024
99852d3
bugfix
omriisack Nov 10, 2024
fbebdd6
Use initial engine state as restore point
omriisack Nov 10, 2024
a0350ab
minor
idan0610 Nov 10, 2024
e326608
minor
idan0610 Nov 10, 2024
25f4c8a
Minor
omriisack Nov 10, 2024
689edc1
cancel skip notification when there is a conflict clause
idan0610 Nov 10, 2024
0603d00
Update cadical to the newest version + change restart implementation …
idan0610 Nov 13, 2024
e7378c2
minor fix
idan0610 Nov 13, 2024
10e2696
change restart to be based on number of conflict clauses
idan0610 Nov 14, 2024
596e689
change decision heuristic to target phases
idan0610 Nov 18, 2024
99a955e
consider all constraints as candidates for decision when using polarity
idan0610 Nov 18, 2024
8156127
Revert "consider all constraints as candidates for decision when usin…
idan0610 Nov 18, 2024
8ebf72a
prioritize variables for decision that are from the target phases
idan0610 Nov 18, 2024
506f00e
Pick split elements from the largest assignment, pick phase based on …
omriisack Nov 20, 2024
b9e7312
minor
omriisack Nov 20, 2024
654118b
cancel saving each lemma to reduce memory requirement
idan0610 Nov 21, 2024
02259e0
minor
idan0610 Nov 21, 2024
a3b5b24
parse external NAP clauses, if exists
idan0610 Dec 4, 2024
eec5707
Fix for malformed basis factorization + add option for a second NAP e…
idan0610 Dec 8, 2024
f206237
minor
idan0610 Dec 8, 2024
732e164
minor
idan0610 Dec 8, 2024
7e4c7fd
cancel variable elimination + check if external clauses are satisfied…
idan0610 Dec 11, 2024
f0f2d88
minor fix
idan0610 Dec 11, 2024
bcf2566
minor fix
idan0610 Dec 11, 2024
e77e029
run sbt during preprocess + replace the check for satisfied external …
idan0610 Dec 12, 2024
ac132be
minor fix
idan0610 Dec 12, 2024
77abafd
minor
idan0610 Dec 12, 2024
d7bece7
minor
idan0610 Dec 12, 2024
4b40b0b
add brute sbt in preprocess + change order of initialization of boole…
idan0610 Dec 29, 2024
a457558
cancel SBT in preprocess + turn off QuickXplain
idan0610 Jan 2, 2025
348c7c9
Minor
omriisack Jan 14, 2025
091f087
Merge remote-tracking branch 'origin/master'
omriisack Jan 14, 2025
1fe06f7
boolean abstraction in regular order
omriisack Jan 14, 2025
328f146
Merge remote-tracking branch 'refs/remotes/upstream/master'
idan0610 Feb 26, 2025
00600f8
merging CDCL code with updated master Marabou branch + allow using na…
idan0610 Feb 27, 2025
f78c039
fix clang format
idan0610 Feb 27, 2025
a95df01
minor clang fix
idan0610 Feb 27, 2025
dd95a38
minor
idan0610 Feb 27, 2025
4dce77e
Fixed engine initialization
idan0610 Mar 2, 2025
c458ad7
some minor fixes
idan0610 Mar 2, 2025
11c1584
some more small fixes
idan0610 Mar 2, 2025
df0c282
Restore use of UNSATCertificateNode when not solving with CDCL
omriisack Mar 2, 2025
eb44242
Split SmtCore into SearchTreeHandler and CdclCore
idan0610 Mar 3, 2025
d03c0d1
minor
idan0610 Mar 3, 2025
d1660ba
minor
idan0610 Mar 3, 2025
925cd7d
Add support for NAP queries
idan0610 Mar 4, 2025
e0fa4bb
add support for cdcl in maraboupy + minor fix to support proof produc…
idan0610 Mar 4, 2025
f9fada1
several fixes, including error for unsupported constraint in CDCL + c…
idan0610 Mar 5, 2025
c3ade80
minor - error when there are non-linear constraints
idan0610 Mar 5, 2025
0532dd6
super minor
idan0610 Mar 5, 2025
d19ae40
minor - change name fo cadicalVars to cdclVars in PiecewiseLinearCons…
idan0610 Mar 5, 2025
8894ab1
Guarding assertions in CDCL methods in Engine, count number of lemmas…
omriisack Mar 5, 2025
ccce916
add statistics to cb_propagate time measurement
idan0610 Mar 5, 2025
0ea1e03
fix for statistics in cb_propagate
idan0610 Mar 5, 2025
9e5085c
minor
omriisack Mar 6, 2025
b1d99be
adding tests + small fix in initializeCDOs
idan0610 Mar 6, 2025
1d8eb65
Merge remote-tracking branch 'origin/master'
idan0610 Mar 6, 2025
ca6b0b7
minor
idan0610 Mar 6, 2025
56f4730
minor fix
idan0610 Mar 6, 2025
4f16724
Removing code for NAP + adding cmake compilation flag for building Ca…
idan0610 Mar 9, 2025
5f0684e
minor
idan0610 Mar 9, 2025
2032f99
fix clang errors
idan0610 Mar 9, 2025
7a078b6
fix clang errors
idan0610 Mar 9, 2025
ba34c15
minor
idan0610 Mar 9, 2025
cc680e2
minor - remove arrayOfStrings option type
idan0610 Mar 9, 2025
e1ad00c
Disable using CDOs for PLCs when in SNC mode
idan0610 Mar 10, 2025
d8dbdcd
minor fix for proof production in bound manager
idan0610 Mar 10, 2025
2be3459
minor fixes with line separator parsing
idan0610 Mar 10, 2025
086d6f9
minor in run_regression.py
idan0610 Mar 10, 2025
c2baa10
minor
idan0610 Mar 10, 2025
1769b48
Add support for decision-based clauses instead of proof-based, as def…
idan0610 Mar 23, 2025
2e2c4b1
minor
idan0610 Mar 23, 2025
2275172
some fixes - avoid calling explainSimplexFailure when using decision-…
idan0610 Mar 23, 2025
7ae1020
minor
idan0610 Mar 23, 2025
f67e823
minor
idan0610 Mar 23, 2025
a54cea5
AC prep
omriisack Mar 27, 2025
b6ff371
Use pseudoimpact to decide split when using SOI (currently without VS…
omriisack Mar 27, 2025
035006e
Modify cdcl decision based on pseudo-impact to be combined with VSIDS
idan0610 Mar 27, 2025
0d19522
Add support for running gurobi with decision clauses
idan0610 Mar 28, 2025
841c76c
Precision restoration bug fix
idan0610 Apr 6, 2025
63999e6
small compilation bug fix
idan0610 Apr 6, 2025
970fb6b
Proof minimization attempt
OmriIsacHUJI Apr 11, 2025
598c427
Merge remote-tracking branch 'origin/cdcl-new' into cdcl-new
OmriIsacHUJI Apr 11, 2025
751d68f
Minor improvements
OmriIsacHUJI Apr 20, 2025
88d9bc9
convert verification query into a reachability query
idan0610 Apr 27, 2025
eff774c
Merge remote-tracking branch 'origin/cdcl-new' into cdcl-new
idan0610 Apr 27, 2025
432240a
some minor bug fixes + adding configuration for controlling conversio…
idan0610 Apr 27, 2025
ed2e224
Return clause if contians many decisions; remove only phaseFixing lem…
OmriIsacHUJI Apr 28, 2025
465e5ec
Remove saturation in proof analysis minimization
OmriIsacHUJI Apr 28, 2025
427b59d
Optimize proof minizations, throw and catch clauses if they consist o…
omriisack Apr 29, 2025
03edca8
Messy code, that unifies the entries and the clauses analysis for eff…
omriisack May 1, 2025
e716540
Messy code, commented out proof minimization
omriisack May 1, 2025
41cc1a3
Revert "Messy code, commented out proof minimization"
idan0610 May 1, 2025
1dd3325
Revert "Messy code, that unifies the entries and the clauses analysis…
idan0610 May 1, 2025
2e59dcb
Revert "Optimize proof minizations, throw and catch clauses if they c…
idan0610 May 1, 2025
31e7248
Proof minimization flag in GlobalConfiguration ; remove unnecessary q…
omriisack May 1, 2025
6c897e8
Remove redundant aggregation of dependencies
omriisack May 1, 2025
8040a10
Remove redundant aggregation of dependencies
omriisack May 1, 2025
94c0f97
Bugfix delete unused lemmas
omriisack May 3, 2025
a73375a
Debugging attempt
omriisack May 3, 2025
abc5ade
Minor
omriisack May 3, 2025
390b1ac
Proof minimization alternative
omriisack May 4, 2025
6ae1ea4
Minor
omriisack May 4, 2025
54ce023
compute scores based on output UB for each literal, and shorten queri…
idan0610 May 17, 2025
6141f5d
fix small bug of clearing decisionScores on every conflic clause
idan0610 May 18, 2025
86511a6
add shortening clauses for reason clauses
idan0610 May 18, 2025
af44c4f
small improvement in creating decision-based reason clauses
idan0610 May 18, 2025
2aea508
comment deepPoly logs
idan0610 May 19, 2025
277251c
skip bounds in conversion to reachability + use input query bounds in…
idan0610 May 19, 2025
5c1b2ae
fixed convert bounds to equations in reachability conversion
idan0610 May 19, 2025
78374e2
if all clause scores are infinity, reorder clause literals by decisio…
idan0610 May 20, 2025
6f192f2
minor bug fix
idan0610 May 20, 2025
067fc7a
another bug fix
idan0610 May 20, 2025
849f2ec
try to compute score with current bounds, before iterating on decisio…
idan0610 May 20, 2025
39c0d66
Revert "try to compute score with current bounds, before iterating on…
idan0610 May 21, 2025
41ca5ff
reorder clause literals by decision level in reversed order
idan0610 May 21, 2025
bba27a1
skip clause shortening if NLR considers the current context as SAT
idan0610 May 21, 2025
a106c7b
minor improvement and possible bug fix
idan0610 May 21, 2025
98403fa
minor
idan0610 May 21, 2025
c663700
bug fix
idan0610 May 21, 2025
797103a
minor bug fix
idan0610 May 21, 2025
e31e9a7
Revert "minor bug fix"
idan0610 May 22, 2025
92abae5
Revert "bug fix"
idan0610 May 22, 2025
9160569
Revert "minor"
idan0610 May 22, 2025
d64c87a
Revert "minor improvement and possible bug fix"
idan0610 May 22, 2025
908404f
Revert "skip clause shortening if NLR considers the current context a…
idan0610 May 22, 2025
7a515c4
refactor shortening clauses code + add skip option + more efficient w…
idan0610 May 22, 2025
1587e8b
minor
idan0610 May 22, 2025
8f302da
possible bug fix
idan0610 May 22, 2025
0ba640b
Cancel conversion to reachability, and compute the score hard-coded
idan0610 May 25, 2025
7ecbae0
possible bug fix
idan0610 May 25, 2025
c870893
add short clauses with quickXplain
idan0610 May 26, 2025
8da2b7b
minor bug fix in QX
idan0610 May 26, 2025
b2f3d28
change score to sum(-relu(lb-ub))
idan0610 May 26, 2025
e35e4a6
Revert "change score to sum(-relu(lb-ub))"
idan0610 May 27, 2025
b0c3551
add back code for naps
idan0610 May 27, 2025
96986a1
Proof Min Minor
omrigora Jun 1, 2025
77b93da
do basis factorization only if backjumping more than one level
idan0610 Jun 3, 2025
676656b
Merge remote-tracking branch 'origin/cdcl-new' into cdcl-new
idan0610 Jun 3, 2025
d2aea2b
Revert "do basis factorization only if backjumping more than one level"
idan0610 Jun 5, 2025
c939ceb
small bug fix in NLR
idan0610 Jun 8, 2025
9816d14
Minor optimization in proof-based clause learning
OmriIsacHUJI Jun 8, 2025
9a14380
Formatting
OmriIsacHUJI Jun 8, 2025
b7b5b7d
Formatting
OmriIsacHUJI Jun 8, 2025
449bae6
In reason clause learning - use only decision made prior to the lit t…
OmriIsacHUJI Jun 8, 2025
c3f431c
reorder decision literals by number of clauses each literal is part of
idan0610 Jun 9, 2025
2daeb6c
Merge remote-tracking branch 'origin/cdcl-new' into cdcl-new
idan0610 Jun 9, 2025
337f66d
if the order by the number of clauses is not meaningful, reorder by d…
idan0610 Jun 9, 2025
3494742
reorder by variable index
idan0610 Jun 10, 2025
d7855e3
Revert "reorder by variable index"
idan0610 Jun 10, 2025
5db3b2e
Revert "if the order by the number of clauses is not meaningful, reor…
idan0610 Jun 10, 2025
44ac4da
Revert "reorder decision literals by number of clauses each literal i…
idan0610 Jun 10, 2025
a3f0030
Turn QX off
omrigora Jun 11, 2025
edfda05
In setInputBoundsForLiteralInNLR only for one variable at most.
OmriIsacHUJI Jun 12, 2025
97ab2de
Formatting
OmriIsacHUJI Jun 12, 2025
7fdfaad
fix bug with cadical decisions not in decisionLiterals
idan0610 Jun 17, 2025
ec348f6
Merge branch 'master' into cdcl-new
idan0610 Jun 22, 2025
fa1afac
some compilation bug fixes
idan0610 Jun 22, 2025
f821b1b
In CDCL PseudoImpact heuristic, prefer later decision variables in ca…
OmriIsacHUJI Jun 25, 2025
1d1dd56
Formatting
OmriIsacHUJI Jun 25, 2025
997adea
Bugfix for IncrementalLinearization.cpp in case SOI is off
OmriIsacHUJI Jun 25, 2025
ab9f801
Proofmin optimization
OmriIsacHUJI Jul 2, 2025
88385ab
Proofmin debug
OmriIsacHUJI Jul 3, 2025
c6236e0
Debug case of --prove-unsat and CDCL_USE_PROOF_BASED_CLAUSES = false
OmriIsacHUJI Jul 21, 2025
06221a7
Add targetBound to proofmin analysis
OmriIsacHUJI Aug 12, 2025
7a3ae30
Merge branch 'NeuralNetworkVerification:master' into cdcl-new
omriisack Aug 12, 2025
cd13c40
Bugfix for proofmin - add targetBound for proof min as a member of le…
omrigora Aug 13, 2025
db23172
Merge remote-tracking branch 'origin/cdcl-new' into cdcl-new
omrigora Aug 13, 2025
2914f05
Formatting
omrigora Aug 13, 2025
29b4060
Fix test
OmriIsacHUJI Aug 13, 2025
dd223cd
Remove unnecessary routines from precision restoration
OmriIsacHUJI Aug 21, 2025
4a15cc4
Change config name to reflect independence of CDCL
OmriIsacHUJI Aug 31, 2025
999f421
formatting
OmriIsacHUJI Aug 31, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .clang-format
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ ColumnLimit: '100'
CompactNamespaces: 'false'
ConstructorInitializerAllOnOneLineOrOnePerLine: 'false'
ConstructorInitializerIndentWidth: '4'
EmptyLineBeforeAccessModifier: 'Always'
#EmptyLineBeforeAccessModifier: 'Always'
FixNamespaceComments: 'true'
IncludeBlocks: Regroup
IndentCaseLabels: 'false'
Expand Down
1 change: 1 addition & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,3 +47,4 @@ cmake-build-debug/
/build/
/wheelhouse/
.mypy_cache/
/tools/cadical/
1 change: 1 addition & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@
- Implemented forward-backward abstract interpretation, symbolic bound tightening, interval arithmetic and simulations for all activation functions.
- Added the BaBSR heuristic as a new branching strategy for ReLU Splitting
- Support Sub of two variables, "Mul" of two constants, Slice, and ConstantOfShape in the python onnx parser
- Added optional CDCL solving for networks with ReLU activations, using CaDiCaL as the backend SAT solver.

## Version 2.0.0

Expand Down
Loading
Loading